상태 전이를 분석하기
시스템의 현재 상태와 다음 상태 사이의 관계를 논리적으로 표현해 검사한다. Pono는 모델 검사 알고리즘을 구성하고 확장하기 위한 기반을 제공한다. 실제 설계를 다른 표현에서 변환한다면 그 변환이 보존하는 의미도 함께 확인해야 한다.
하드웨어 모델과 연결
Verilog 설계에서 Yosys를 이용해 BTOR2 표현을 생성하는 활용 경로가 있다. 이때 클록, 리셋, 초기 상태와 가정의 처리가 중요하다. 파일 변환에 성공했더라도 원래 설계에서 의도한 환경이 같은 방식으로 표현되었는지는 별개의 점검 대상이다.
백엔드의 차이
사용할 해결기와 분석 알고리즘에 따라 필요한 빌드 구성이 달라진다. 보간을 사용하는 모델 검사에는 추가 해결기가 요구될 수 있다. Pono 본체와 선택한 해결기의 이용 조건도 같다고 가정하지 않고, 재현 기록에 전체 구성을 남긴다.
관련 문서
Smt-Switch / Kind 2 / Bitwuzla / Yices