짧은 형식 반례를 재현하려면 첫 원인부터 복원해야 한다

형식 검증이 찾아낸 반례는 짧을 때가 많다. 리셋 뒤 몇 번의 입력만으로 FIFO가 잘못된 값을 내보냈다면, 그 순서를 회귀 테스트에 넣어 오래 남겨 두고 싶어진다. 그러나 파형에 보이는 입력값만 옮겼는데 같은 실패가 나오지 않을 수 있다. counterexample 재현은 숫자의 복사가 아니라, 실패를 만든 상태와 시간 조건의 복원이다.

반례 파일에는 입력 이상의 맥락이 있다

SymbiYosys의 FIFO 시작 예제는 실패 경로를 VCD, Verilog 테스트벤치, SMT 제약 파일로 출력하는 SMTBMC 실행 로그를 보여 준다. 이 예제의 trace는 실제로 상태가 어디서 어긋났는지 찾는 데 사용된다. 다만 모든 엔진과 모든 실패 종류가 동일한 파일을 만든다고 일반화해서는 안 된다. 사용한 엔진과 작업의 로그에서 생성된 파일을 확인해야 한다. SymbiYosys의 FIFO 반례 예제

파형에는 클록, 리셋, 입력과 출력 외에도 모델이 선택한 초기 상태나 내부 상태가 들어갈 수 있다. 입력을 구체적인 값으로 골랐다는 사실과, 그 상태를 정상 리셋으로 만들 수 있다는 사실은 별개다. 초기화하지 않은 메모리의 내용도 반례에 영향을 줄 수 있다. 시뮬레이션 환경이 모두 0으로 채우면 같은 경로가 사라질 수 있다.

먼저 반례가 어떤 검사에서 나왔는지 구분해야 한다. 정해진 초기 상태에서 시작하는 base case의 실패라면 그 초기 조건에서 실패까지의 경로를 살펴볼 수 있다. induction 단계의 실패 후보는 실제 초기 상태에서 도달하지 않는 상태를 출발점으로 삼을 수 있다. 그런 후보를 리셋부터 재현하려고 해도 실패가 나오지 않는 것이 자연스럽다. SymbiYosys의 초기 조건과 induction 설명

빈 FIFO 읽기에서 시작하는 네 번의 자극

깊이가 2인 가상 FIFO를 생각하자. 빈 상태에서 읽기를 요청하면 요청을 받아들이지 않고 포인터도 유지하는 계약이다. 정상 읽기는 먼저 저장한 데이터를 먼저 내보낸다. 리셋은 count, 읽기 포인터와 쓰기 포인터를 모두 0으로 만든다.

버그가 있는 회로는 count가 0일 때도 읽기 요청만 들어오면 읽기 포인터를 바꾼다. count는 그대로 0이라서 바로 출력만 보면 오류를 놓칠 수 있다. 다음 순서에서 처음 저장한 두 값이 뒤집힌다. A=0x35, B=0xC2로 잡고, 쓰기와 읽기는 아래에서 각각 다른 에지에 요청한다.

이 표는 명시한 가상 버그의 상태 전이를 계산한 것이다. 공식 예제의 FIFO가 반드시 같은 거부 정책을 사용한다는 주장도, 실제 solver가 이 숫자를 찾았다는 주장도 아니다. 공식 예제는 빈 읽기에서 두 주소를 함께 이동시키는 방식도 다룬다. 테스트로 옮길 때는 자신이 검증한 FIFO 계약을 기준으로 기대 동작을 써야 한다.

이 가상 회로에서는 첫 빈 읽기가 원인을 만들고, 마지막 읽기가 데이터 오류를 관측하게 한다. 마지막 두 쓰기와 읽기만 남기면 두 포인터가 정상 위치에서 시작하므로 B 대신 A가 나올 수 있다. 짧게 만들겠다고 최초 원인 자극을 지워 버리면 더 이상 같은 버그의 재현이 아니다.

클록 경계까지 같은 실험으로 만들기

실제 회귀 테스트에서는 입력을 DUT가 샘플링하기 전에 안정시켜야 한다. 상승 에지와 동시에 입력을 바꾸는 드라이버는 시뮬레이터의 실행 순서에 따라 서로 다른 자극을 만들 수 있다. 출력 검사도 해당 인터페이스의 유효 시점을 따라야 한다. 등록된 읽기 출력이라면 에지에서 읽기 요청이 수락됐는지 기록하고, 출력이 갱신된 뒤 올바른 값과 비교한다.

실패 속성의 샘플링 시점도 함께 읽는다. clocked immediate assertion은 그 에지의 비차단 대입이 반영되기 전 상태를 검사할 수 있다. 파형의 마지막 구간만 보고 “이 에지에서 이 값이 쓰였으니 즉시 비교해야 한다”고 옮기면 한 사이클 차이의 새 테스트를 만들 수 있다. $past를 사용했다면 과거 값의 이력과 첫 유효 검사 시점도 보존해야 한다.

재현 결과를 판단할 때는 동일한 숫자의 실패 메시지보다 처음 어긋난 상태를 비교하는 편이 유용하다. 위 예에서는 빈 읽기 뒤 읽기 포인터가 1이 되는지, 두 쓰기 후 count가 2인지, 마지막 수락에서 B가 관측되는지를 순서대로 확인한다. 전제가 같지 않은 실패라면 비슷한 증상을 만들었을 뿐 원래 반례를 재현한 것이 아닐 수 있다.

회귀 테스트에는 사용한 RTL 버전, 파라미터, 초기화·리셋 순서, 입력을 넣고 결과를 읽는 시점, 형식 환경의 주요 가정을 남긴다. 임의 초기 상태가 핵심이라면 시뮬레이션에서 그 상태를 어떻게 구체화했는지도 기록한다. 내부 값을 강제로 맞춘 테스트를 리셋에서 자연스럽게 도달한 증거로 해석해서는 안 된다.

반례가 재현됐다고 해서 다른 모든 입력에서 회로가 옳다는 증명이 되는 것은 아니다. 그래도 발견한 오류가 수정 뒤 다시 나타나지 않도록 지키는 작고 구체적인 테스트를 얻는다. 최초 원인부터 첫 불일치까지 같은 상태 전이를 복원하면, 짧은 형식 반례는 누구나 다시 실행하고 이해할 수 있는 버그의 설명으로 남는다.