overconstraint: ready를 항상 1로 두면 stall 오류가 사라진다

형식 검증이 통과했는데 실제 회로는 ready가 꺼진 순간 데이터를 받아들인다. 검증 환경은 ready를 항상 1이라고 가정했다. stalled 입력은 한 번도 검색하지 않았으므로 그 상황의 오류도 존재할 수 없었다. 통과한 것은 전체 인터페이스가 아니라 좁혀 놓은 환경에서의 주장이다.

overconstraint는 가정이 합법적인 동작까지 제외하여 검사 범위를 과도하게 줄이는 문제다. 강한 가정은 계산을 쉽게 만들지만 그만큼 결론의 조건도 강해진다.

assume은 정답을 검사하는 문장이 아니다

SBY 문서는 assume이 도구가 살펴볼 가능성을 제한한다고 설명한다. 생성된 trace에서 가정은 참이어야 한다. assert는 그 조건 안에서 거짓이 되는 경로를 찾는 검사다. 따라서 assume에 넣은 동작이 DUT에서 정말 성립하는지는 같은 문장으로 검증한 것이 아니다. YosysHQ SBY, SystemVerilog Immediate Assertions

가상의 인터페이스에서 전송은 valid와 ready가 모두 1인 edge에만 성립한다. DUT의 내부 수락 신호 take는 이 조건과 같아야 한다. 그런데 구현 오류로 take=valid가 되었다고 하자.

네 조합 중 valid=1, ready=0에서만 다르다. 그런데 환경에 assume(ready)를 넣으면 이 행이 사라진다. 나머지 가능한 두 행에서는 구현이 맞으므로 assert(take == (valid && ready))는 그 가정 아래에서 통과할 수 있다.

이 결과는 solver가 틀렸다는 뜻이 아니다. 질문에 넣지 않은 입력을 solver가 임의로 되살려 검사하지 않는다는 뜻이다. stall을 허용하는 명세라면 ready=0을 검색 공간에 남겨야 한다.

환경의 의무와 회로의 보장을 나눈다

예를 들어 valid를 제시한 sender가 수락 전까지 payload를 유지해야 한다는 규칙은 입력 환경의 의무일 수 있다. 이를 가정하면 DUT가 합법 입력을 만났을 때의 동작을 검증한다. 반면 DUT 자신의 take가 정확하다는 것을 assume으로 넣으면 검사해야 할 결론을 먼저 사실로 만든다.

내부 FIFO가 overflow하지 않는다고 가정하고 overflow 방지를 증명하는 경우도 같은 위험이 있다. 내부 상태에 대한 가정이 항상 금지된 것은 아니지만, 추상화 경계에서 따로 검증한 보장인지 근거가 있어야 한다. 편의를 위해 임의로 넣은 내부 조건은 DUT의 실제 실패 경로를 제거할 수 있다.

위 ready 가정도 모든 상황에서 틀린 것은 아니다. 대상의 계약이 실제로 항상 준비된 sink만 연결하도록 제한한다면 그 조건의 검증은 의미가 있다. 다만 stall을 지원한다는 더 넓은 주장으로 확대해서는 안 된다. 결과를 사용할 시스템에서 이 환경 가정이 충족되는지 확인해야 한다.

cover로 사라진 상황을 찾아본다

검증 환경에 stall 상황을 목표로 하는 cover(valid && !ready)를 추가하면 가정이 그 상황을 허용하는지 확인할 수 있다. ready=1 가정 아래에서는 그 목표가 도달할 수 없다. 가정을 제거하면 valid=1, ready=0인 입력이 목표의 witness가 된다.

이 cover는 DUT가 stall을 옳게 처리한다는 증명은 아니다. 검사할 환경이 그 상황을 검색할 수 있다는 확인이다. 실제 수락의 정확성은 앞의 assertion처럼 별도로 검사한다. 목표를 찾은 하나의 경로와 오류가 없는 모든 경로는 다른 결론이다. YosysHQ SBY, cover 및 assertion 설명

reset 해제, 요청 수락, FIFO full, stalled 응답 등 명세에서 중요한 경계를 cover로 확인하면 가정의 영향을 살펴보기 좋다. 단, 몇 개의 대표 목표가 도달했다고 모든 합법 입력이 열려 있다는 보장은 없다. 긴 stall이나 특정 데이터 조합은 여전히 별도의 가정 때문에 빠질 수 있다.

서로 충돌하는 가정도 조심한다

가정이 너무 강한 데서 더 나아가 서로 모순될 수도 있다. 같은 시점의 ready에 1과 0을 동시에 요구하면 허용되는 실행이 없다. 이런 환경에서 위반 경로가 없다는 논리적 사실은 회로의 정확성에 대한 쓸 만한 근거가 아니다.

도구는 가정의 충돌을 점검하는 기능을 제공할 수 있다. SBY의 SMTBMC engine 문서는 assumptions가 모순되지 않는지 확인하는 presat 질의를 설명한다. 그러나 도구의 자동 점검 여부만으로 의미적인 overconstraint를 모두 잡는다고 생각해서는 안 된다. ready=1처럼 일관되지만 과도한 가정은 여전히 가능하다. YosysHQ SBY, smtbmc engine

가정을 줄이거나 하나씩 바꾸어 주요 목표의 도달 여부가 달라지는지도 살펴본다. 단순히 모든 가정을 삭제하면 불법 입력 때문에 무의미한 반례가 생길 수 있으므로, 각 조건이 명세의 어느 의무에서 왔는지 적어 둔다.

ready를 항상 1로 두면 검증은 쉬워지지만 stall에 대한 답은 얻지 못한다. overconstraint를 피하려면 입력 계약만 적절히 제한하고 DUT의 의무는 검사 대상으로 남겨야 한다. 중요한 경계가 검색 가능한지 확인하고 가정과 함께 결과를 보고해야 통과의 의미가 실제 사용 환경과 맞아진다.