명령어의 의미를 적기
명령어가 레지스터와 메모리 상태를 어떻게 바꾸는지 기술한다. 설명용 의사 코드와 비슷한 접근성을 지향하지만 타입과 동작을 더 정밀하게 다룬다. 비트벡터 길이 같은 수치 제약은 SMT 해결기를 이용한 타입 검사에 활용된다.
하나의 모델을 여러 작업에 활용
ISA 명세에서 문서 조각과 실행 모델, 정리 증명기용 정의를 만들 수 있다. 생성한 실행 모델은 순차 코드 테스트의 기준으로 활용할 수 있다. 기호 평가 도구와 연결해 명령어 시퀀스 생성이나 완화된 메모리 행동 분석에도 사용한다.
모델별 지원 범위
Sail 도구의 기능과 개별 ISA 모델의 완성도는 구분해야 한다. 일부 모델은 전체 시스템을 다루지만 다른 모델은 사용자 모드 일부에 한정될 수 있다. 사용할 아키텍처와 출력 백엔드가 실제로 지원되는지 확인한다.
관련 문서
Isla / Lem 의미론 도구 / Z3 / K 프레임워크