formal cover: FIFO를 채운 경로가 데이터 순서를 증명하지는 않는다

형식 검증 도구가 FIFO를 가득 채우는 입력 경로를 찾아냈다. 그렇다면 FIFO가 제대로 동작한다고 볼 수 있을까. 점유율은 맞게 세지만 저장 주소가 잘못되어 데이터를 덮어쓰는 회로도 full 상태에 도달할 수 있다. 목표 상태에 갔다는 사실과 그 이후 모든 동작이 정확하다는 사실은 다르다.

formal cover는 가정과 초기 조건 아래에서 특정 목표에 도달하는 경로를 찾는다. 검증 환경이 필요한 상황을 만들어 낼 수 있는지 확인할 때 유용하지만, correctness assertion을 대신하지 않는다.

도달할 경로 하나를 찾는다

가상의 깊이 4 FIFO가 초기에는 비어 있고, 각 단계에 최대 한 항목을 수락한다고 하자. pop 없이 push를 네 번 수락하면 점유율은 0→1→2→3→4가 된다. 목표 cover(count==4)는 이 경로를 witness로 사용할 수 있다.

표는 설명 모델의 상태 번호다. 실제 도구의 depth와 step 번호는 초기 상태와 속성 샘플링 방식을 확인하여 맞춘다. 목표에 대한 cover가 성공하면 이 모델 안에 해당 상태로 가는 허용 경로가 있음을 알 수 있다.

SBY 문서는 cover 모드를 각 cover 목표에 도달하는 trace 생성으로 정의한다. 초기 상태에서 시작해 해당 식을 참으로 만드는 경로를 찾는다는 점에서, 모든 허용 경로에 대한 safety assertion과 목적이 다르다. YosysHQ SBY, Options section, Formal extensions, cover 설명

찾아낸 경로도 무엇을 검사했는지 확인한다

같은 FIFO에서 쓰기 주소가 항상 0인 오류가 있다고 하자. count는 정상 증가해 full이 되지만 네 데이터는 같은 위치를 덮어쓴다. full cover는 여전히 도달할 수 있다. 그 witness가 pop을 포함하지 않는다면 나중에 잘못 읽는 동작까지 보여 주지도 않는다.

full 상태 자체에 대한 목표와 입력한 데이터를 순서대로 읽는 검사는 별도다. 데이터 순서 assertion을 넣고 필요한 실행 전체를 검증해야 한다. cover가 하나의 올바른 경로를 찾았더라도 다른 입력 경로에서 오류가 없다는 결론은 얻지 못한다.

cover 실행에서 assertion을 함께 검사하는지도 설정을 읽어야 한다. 현재 SBY reference는 cover 모드의 cover_assert 옵션을 정의하고 기본값을 off로 적는다. assertion 검사가 필요한 cover task라면 해당 옵션과 실행 로그를 확인해야 한다. 문서의 일반적인 cover 설명만 보고 모든 실행이 assertion까지 검사한다고 가정하지 않는다. YosysHQ SBY, cover_assert 옵션

다음은 이 목적을 드러내는 options 부분의 예다. 전체 실행에는 별도의 engine, script 및 files 설정도 필요하다.

[options]
mode cover
depth 10
cover_assert on

이 설정도 cover에서 살펴보는 경로에 대한 검사와 전역 safety 증명을 동일하게 만들지는 않는다. 목표에 도달하는 경로에서 assertion이 깨지지 않았다는 사실과, 가능한 모든 경로에서 그 assertion이 유지된다는 사실을 나누어 보고한다.

미도달은 깊이와 가정의 영향을 받는다

초기 상태부터 세 번의 전이만 보면 위의 full 목표는 아직 만들 수 없다. FIFO가 고장 나서가 아니라 한 번에 하나만 넣는 조건에서 네 번이 필요하기 때문이다. 검사 범위 안에서 찾지 못했다는 결과를 영원히 도달 불가능하다는 증명으로 바꾸지 않는다.

SBY의 공식 FIFO 예제도 깊이 100의 FIFO를 기본 cover depth 20으로 채우려 할 때 필요한 사이클 수를 고려하도록 안내한다. 목표와 전송률, reset에 소비하는 단계까지 보고 깊이를 정해야 한다. YosysHQ SBY, Getting started의 Exercise

가정이 목표를 막을 수도 있다. push가 한 번도 수락되지 않는 환경으로 제한했다면 올바른 FIFO도 full에 도달하지 못한다. 반대로 초기 count를 full로 허용하면 실제로 채우는 과정 없이 목표가 만족된다. 이 경우 ‘full 상태가 허용된다’는 witness이지, reset 뒤 정상 입력으로 채웠다는 witness는 아니다.

목표에 reset 해제와 필요한 전송 조건을 포함하거나, 해당 초기 조건과 전이 계약을 별도로 정의해야 한다. 단순히 count가 4라는 값만으로 목표의 의도 전체를 표현한 것인지 점검한다.

결과 목록이 목표 목록과 맞는지 본다

property를 조건부 컴파일하거나 파라미터로 비활성화하면, 기대했던 cover가 최종 모델에 없을 수 있다. 도구의 종료 표시만 읽지 말고 elaboration 뒤의 목표 수와 이름, 각 목표의 도달 결과를 확인한다. 없는 목표를 검사했다고 보고할 수는 없다.

여러 cover를 따로 달성한 경로가 있다고 해서 모든 상황을 한 번의 연속 실행에서 거쳤다는 뜻도 아니다. ‘full을 보았다’와 ‘empty를 보았다’가 별도 witness라면, full 이후 empty까지 정상 drain하는 전체 순서를 확인하려는 목적에는 그 순서를 표현하는 목표가 필요하다.

witness를 시뮬레이션 입력으로 활용할 수는 있지만 가정과 초기화도 함께 옮겨야 한다. 도구가 허용한 초기 register 값이 실제 reset 상태와 다르거나, 외부 신호 관계를 재현하지 않으면 같은 경로가 실행되지 않을 수 있다.

formal cover는 FIFO를 채우는 허용 경로를 보여 준다. 그 경로의 목표와 시작 조건, assertion 검사 설정 및 탐색 깊이를 함께 읽어야 의미가 맞는다. 도달 가능성을 확인한 뒤 데이터 순서 같은 동작 요구는 별도 증명으로 검증해야 full이라는 숫자를 correctness의 결론으로 오해하지 않는다.