단순한 연산으로 회로 표현
논리 회로를 AND 연산과 신호 반전의 연결로 나타내면 도구 사이에서 공통으로 다룰 수 있다. AIGER는 이러한 그래프를 파일로 저장하고 처리하는 기반을 제공한다. 회로를 어떤 형식으로 표현하는지와 어떤 속성을 검사하는지는 다른 층위의 문제다.
검증 도구 사이의 연결
모델 검사 벤치마크와 변환 도구에서 AIGER를 사용할 수 있다. 배포 유틸리티에는 다른 회로 표현을 변환하거나 시뮬레이션하는 도구가 포함된다. 단순한 안전성 문제를 시간 단계별로 펼치는 한정 모델 검사 활용도 있다.
형식과 지원 범위
AIGER의 형식 버전은 표현할 수 있는 속성과 정보를 구분하는 기준이다. 도구가 파일을 읽는다는 사실만으로 모든 기능을 동일하게 처리한다고 가정하지 않는다. 초기 상태와 출력의 의미, 속성의 종류가 변환 과정에서 유지되는지 확인한다.