어느 클록에서 전송을 수락했는가
검증 대상의 계약이 i_wr=1, busy=0라면 그 조건이 참인 클록의 데이터와 설정을 기준으로 프레임을 추적합니다. 요청만 들어온 시점이나 나중에 바뀐 입력을 기준값으로 삼지 않습니다. 8N1 예시를 가변 길이·패리티·다중 stop bit 설계에 그대로 적용하지 않습니다.
2019년 ZipCPU UART 사례는 가변 baud 간격을 긴 반복식으로 표현할 때 증명 상태가 커지는 문제와, 별도의 모니터 상태를 두는 대안을 보여 줍니다. 마지막 stop 구간의 busy 해제 경계도 수락 시점과 맞춰야 합니다. 원문의 특정 도구 한계를 모든 현재 버전에 일반화하지 않습니다.
모니터가 DUT의 실수를 따라 하지 않게 합니다
검증용 모니터는 수락한 데이터에서 예상 start·data·stop 값을 만들고, 약속된 tick마다 출력과 대조합니다. DUT의 비트 번호나 다음 상태를 그대로 복사하면 동일한 오류를 따라갈 수 있습니다. 모니터 자체도 작은 정상·오류 trace로 확인하되, 그 시험을 DUT 증명 성공으로 표시하지 않습니다.
리셋 중 어느 assertion을 적용할지와 리셋 뒤 처음 유효한 history를 명시합니다. YosysHQ 문서는 첫 클록의 $past 값이 정의되지 않는다는 점을 설명합니다. 출력 위반을 숨기려고 DUT 내부 상태를 assume하지 말고, 실제 환경 계약과 설계가 지켜야 할 assertion을 구분합니다.
구문 지원과 증명 결과를 별도로 기록합니다
SBY의 front end와 엔진에 따라 지원 구문이 달라집니다. 현재 Verific 문서는 repetition과 checker·bind 등을 설명하지만 여러 클록을 한 property에 섞는 것은 지원하지 않는다고 명시합니다. 이 지원표만으로 로컬 설치·라이선스·선택한 엔진의 지원 여부가 확인되지는 않습니다.
결과에는 RTL·모니터 버전, 설정, 클록·리셋 모델, 엔진과 증명 모드를 함께 남깁니다. cover 도달, 제한된 깊이의 무반례, 귀납 증명 완료를 구분합니다. 여기서는 검증 구조를 설명하며 UART RTL 실행이나 형식 증명 완료를 주장하지 않습니다.
- 수락
데이터와 설정을 고정
- 시간 모델
tick·리셋·history 정의
- 비교
출력과 예상 프레임 대조