귀납 불변식: reset으로 갈 수 없는 상태가 반례에 나타났다면

reset 이후 두 카운터는 항상 같은 값으로 움직인다. 초기 상태에서 길게 실행한 검사에서는 오류가 없다. 그런데 귀납 단계는 두 값이 서로 다른 상태에서 시작해 오류를 만든다. 이 반례를 실제 입력으로 그대로 재현하려 하면 시작 상태부터 만들 수 없다.

귀납 불변식은 도달 가능한 상태가 유지하는 관계를 명시하여 이런 증명의 간극을 줄인다. 실제 실행의 안전성과, 현재 속성만으로 다음 단계가 안전하다고 추론할 수 있는지는 서로 다른 질문이다.

초기 상태에서의 경로를 먼저 본다

설명용 상태는 4비트 a, b와 1비트 error다. 초기값은 모두 0이다. 매 단계에 입력 en이 1이면 a와 b에 똑같이 1을 더하고 16에서 wrap하며, en이 0이면 둘 다 유지한다. 다음 error는 현재 a와 b가 서로 다른지로 정한다.

a_next     = (a + en) mod 16
b_next     = (b + en) mod 16
error_next = (a != b)

초기 a=b=0에서 같은 입력을 적용하므로 이후에도 a=b다. 따라서 error는 계속 0이다. 검사할 주 속성 P는 error==0이다.

초기 상태를 기준으로 각 입력을 따라가면 P가 유지된다. 그러나 한 단계 귀납은 보통 ‘현재 P가 참인 상태에서 다음에도 P가 참인가’를 묻는다. 이 전제에 초기화에서 도달했다는 정보가 모두 들어 있는 것은 아니다.

주 속성만으로는 관계를 보존하지 못한다

상태 (a=0, b=1, error=0)을 보자. P는 참이다. 하지만 다음 단계 error는 1이므로 P가 깨진다. 이 상태는 초기 a=b=0에서 같은 증가를 반복하여 도달할 수 없지만, P만 보아서는 제외되지 않는다.

따라서 이 한 단계 귀납 실패는 곧바로 실제 reset 경로의 DUT 오류를 증명하지 않는다. 초기 조건을 포함한 base case에서 나온 반례인지, 귀납 단계에서 나온 반례인지 나누어 읽어야 한다.

SBY 문서는 prove 모드에서 induction 단계가 실패하여 UNKNOWN이 나올 수 있음을 설명한다. 또 SMTBMC engine의 prove depth를 k-induction의 깊이로 정의한다. 그 결과는 초기 경로에서의 구체적인 assertion 실패와 구별해야 한다. YosysHQ SBY, assertion 설명, SBY, depth 및 smtbmc engine

보조 관계도 처음부터 증명한다

이 예에 필요한 보조 불변식 I는 a==b다. 이를 P와 함께 확인하면 귀납 전제가 실제 상태의 중요한 관계를 담게 된다.

초기에는 a=b=0이므로 I가 참이고 error=0이므로 P도 참이다. 현재 a=b라면 같은 en을 더한 뒤에도 두 값은 같으므로 I가 유지된다. 현재 a=b이므로 다음 error도 0이어서 P가 유지된다. 이 두 단계를 확인하면 (a=b) && (error=0)은 초기에서 성립하고 각 전이 뒤에도 성립한다.

중요한 점은 a=b를 근거 없이 assume하는 것으로 끝내지 않는다는 것이다. DUT 내부의 보조 관계가 초기에서 참이며 계속 유지되는지도 assertion으로 검증해야 한다. 그렇지 않으면 실제로 두 값을 다르게 만드는 회로 오류까지 검색 공간에서 지워 버릴 수 있다.

예를 들어 b만 특정 조건에서 두 번 증가하는 오류가 있다면 a=b를 검사하는 속성은 그 차이를 드러내야 한다. a=b를 무조건 가정하면 같은 버그를 숨길 수 있다. 증명을 돕는 정보와 DUT를 대신 옳다고 선언하는 정보는 다르다.

깊이 증가와 보조 관계는 서로 다른 도구다

이 작은 예는 귀납 전제의 연속 상태를 늘려도 해결될 수 있다. error가 0인 상태가 연이어 유지되었다는 조건은 앞 단계의 a=b 관계를 간접적으로 제한한다. 따라서 언제나 명시적인 불변식을 추가해야만 증명할 수 있다는 뜻은 아니다.

하지만 큰 설계에서는 깊이를 늘릴수록 계산이 무거워지고, 필요한 상태 관계가 멀리 떨어져 있을 수 있다. FIFO의 점유율과 포인터 관계, outstanding 요청 수와 큐 상태처럼 의미 있는 보조 관계를 적으면 증명해야 할 이유도 읽기 쉬워진다.

너무 강한 후보 불변식은 실제 도달 상태에서 깨질 수 있다. wrap된 포인터를 일반 정수의 대소 관계처럼 비교하는 것이 한 예다. 후보를 적기 전에 정상 실행의 경계와 초기 조건을 확인하고, base case와 전이 보존을 모두 검증해야 한다.

또 초기화 가정이 잘못되었다면 ‘도달 불가능’이라는 판단도 바뀐다. a와 b가 실제 reset에서 모두 0이 되는지, 일부 상태가 임의 값으로 시작하는지에 따라 허용 상태 집합이 달라진다. 귀납 반례가 낯설다는 이유만으로 도구의 가짜 반례라고 단정하지 않는다.

귀납 불변식은 안전한 실행이 왜 계속 안전한지를 표현한다. error=0만으로 설명이 부족했던 예에서는 a=b라는 관계가 다음 상태의 안전성을 연결한다. 반례가 초기 실행에서 온 것인지 확인하고, 필요한 관계를 독립적으로 증명하면 도달 불가능한 상태와 실제 설계 오류를 구별할 수 있다.