먼저 엔진과 초기 상태를 확인합니다
SBY의 smtbmc 엔진으로 prove를 수행하면 base case와 귀납 단계를 구분합니다. 초기 조건에서 정해진 깊이까지 오류가 없다고 해서 무한한 실행까지 증명한 것은 아닙니다. prove의 모든 엔진이 같은 귀납 방식을 쓰는 것도 아닙니다.
SBY는 reset이라는 이름을 특별하게 취급하지 않습니다. 필요한 초기화와 리셋 순서를 모델에 명시해야 합니다. 귀납 반례는 임의의 비리셋 상태에서 시작할 수 있으므로 실제 초기 상태에서 도달 가능한지도 확인합니다.
출력만 같아도 내부 상태는 다를 수 있습니다
ZipCPU의 2018년 예시는 초기값·리셋·입력·enable이 같은 두 시프트 레지스터를 비교합니다. 출력 비트의 동등성만으로는 귀납 단계의 다른 내부 비트를 제한하지 못합니다. 레지스터 전체가 같다는 보조 불변식은 더 강한 증명 대상입니다.
축소한 3비트 예시를 생각하면 010과 000은 최상위 출력이 모두 0입니다. enable 상태에서 같은 0을 넣어 왼쪽으로 한 번 이동하면 100과 000이 됩니다. 그러나 두 레지스터를 같은 값으로 초기화하고 매번 같은 전이를 적용했다면 이 서로 다른 상태 쌍에 도달할 수 없습니다.
가정으로 오류를 지우지 않습니다
환경의 실제 계약은 assume으로 모델링할 수 있지만, 내부 동등성은 초기 조건과 전이로부터 증명할 assertion으로 둡니다. 귀납 단계의 실패를 실제 오류나 성공으로 단정하지 말고 base case, 보조 불변식, 환경 제약을 따로 점검합니다.
SBY·Yosys·엔진·솔버 버전과 설정, 전체 결과를 함께 기록합니다. 여기의 3비트 설명은 상태 전이 예시이며, 새 SBY 실행이나 실제 FPGA 검증 결과를 주장하지 않습니다. 2018년의 솔버 조합과 종료 코드를 현재 설치 환경에 그대로 대입하지 않습니다.
- 초기 조건
어디서 실행이 시작되는가
- 상태 전이
어떤 관계가 유지되는가
- 검증 결과
어느 증명 의무가 해결됐는가