bounded model checking: 19번까지 안전해도 20번째는 다르다

초기화 뒤 19번의 상태 변화에서 오류가 없었다. 그렇다면 계속 실행해도 안전할까. 카운터가 특정 값에 도달했을 때만 발생하는 오류라면 다음 상태에서 처음 드러날 수 있다. bounded model checking의 성공을 읽을 때는 검사한 입력 조건과 시간 범위를 함께 읽어야 한다.

이 방법은 정한 깊이까지 가능한 경로에서 속성 위반을 찾는다. 제한된 범위 안의 결과가 그 이후 모든 실행에 대한 보장이 되지는 않는다.

긴 실행을 상태 변화의 식으로 펼친다

설명용으로 초기 상태 x₀=0인 5비트 카운터를 생각하자. 매 단계의 입력 en이 1이면 1을 더하고, 0이면 유지한다. 31 다음은 0이다. 검사할 속성은 ‘카운터가 20이 되는 상태가 없다’다. 이 속성은 의도적으로 잘못된 설계 요구이며 깊이의 효과를 보기 위한 예다.

전이 관계는 xₜ₊₁=(xₜ+enₜ) mod 32다. 초기화 이후 19번의 전이로 도달한 상태는 최대 19이므로 20은 없다. 20번 모두 en=1이면 x₂₀=20이 되어 위반한다.

SMT 기반 BMC는 이런 초기 상태와 전이, 입력 조건을 유한한 길이로 연결하여 위반하는 해가 있는지 묻는다. 선택한 seed의 한 경로만 실행하는 테스트와 달리, 모델과 가정이 허용하는 해당 길이의 경로를 논리식으로 다룬다. solver가 탐색을 정상 완료한 경우에 그 범위의 결과를 판단할 수 있다.

SBY 공식 문서는 mode bmc를 bounded safety 검사로, mode prove를 unbounded safety 검사로 구분한다. depth는 BMC에서 고려할 사이클 수를 지정한다. YosysHQ SBY, Options section

깊이와 실제 실패 시점을 맞춰 읽는다

위의 19와 20은 설명 모델에서 전이 횟수를 명시한 것이다. 도구의 step 번호와 depth 숫자를 곧바로 같은 것으로 보지는 않는다. 초기 상태를 어느 step에 포함하는지, 속성을 edge에서 언제 검사하는지, reset에 몇 step을 사용했는지를 trace에서 확인해야 한다.

특히 clocked immediate assertion은 상태 갱신과 관측 시점의 관계에 따라 위반 보고가 직관보다 뒤에 보일 수 있다. SBY 문서는 clocked assertion이 직전 구간의 상태를 검사하는 차이를 설명한다. counterexample의 마지막 줄만 보지 말고 관련 상태가 언제 만들어졌는지 함께 읽는다. YosysHQ SBY, SystemVerilog Immediate Assertions

예를 들어 검사의 총 깊이 중 앞부분을 reset 상태로 보내면 정상 동작에서 탐색한 기간은 그만큼 짧아진다. 처음 10단계에 속성 검사를 건너뛰는 옵션이 있다면 ‘처음부터 확인했다’고 보고할 수도 없다. 멀리 있는 실패를 찾기 위해 깊이를 늘리는 일과, 이미 건너뛴 구간을 검사하는 일은 다른 문제다.

BMC 성공과 무제한 증명은 다른 결론이다

카운터 예에서 19전이까지 통과한 뒤 ‘영구적으로 20이 되지 않는다’고 쓰면 틀린 보고다. 정확한 표현은 ‘정한 초기 조건에서 19전이 이내에 해당 속성의 반례가 없다’다. 20전이 경로 하나만으로 무제한 주장에 반례를 만들 수 있다.

무제한 safety 증명에는 귀납이나 다른 도달성 분석을 사용하는 prove 흐름이 있다. SBY의 SMTBMC engine에서 prove의 depth는 k-induction 깊이를 뜻하며, BMC처럼 그 이후를 단순히 생략한다는 의미로 읽어서는 안 된다. 다른 prove engine은 그 옵션을 무시할 수도 있으므로 선택한 engine도 기록해야 한다. YosysHQ SBY, depth 및 Engines section

BMC를 깊게 실행했다고 자동으로 귀납 증명으로 바뀌지는 않는다. 반대로 유한 상태 모델의 완전성에 대한 별도 근거가 있다면 제한된 탐색을 더 강하게 해석할 수 있지만, depth가 커 보인다는 이유만으로 그 근거를 가정하지 않는다.

결과 상태도 나누어 읽는다. 반례를 찾은 FAIL과, 계산을 끝내지 못한 timeout이나 UNKNOWN은 다르다. 성공했다고 표시된 task가 무엇을 검사했는지와 어떤 속성이 포함되었는지도 확인한다. 찾지 못한 시간을 논리적인 부재의 증거로 바꿀 수는 없다.

보고 문장에 범위를 남긴다

검사 기록에는 소스와 파라미터, 초기화·환경 가정, 속성 이름, mode와 engine, 깊이 및 종료 상태를 남긴다. 이 정보가 있어야 ‘어떤 입력에서 어느 구간까지’라는 문장이 복원된다. 물리적인 metastability나 모델에 넣지 않은 동작까지 검사한 것으로 확대하지 않는다.

BMC의 장점은 짧은 반례를 구체적인 입력과 상태 흐름으로 보여 줄 수 있다는 점이다. reset 직후나 좁은 프로토콜 코너처럼 비교적 가까운 실패를 찾는 데 유용하다. 다만 긴 지연 뒤의 오류는 필요한 깊이까지 도달하지 못하면 남는다.

19번째까지 카운터가 안전해도 20번째의 상태는 별도 질문이다. bounded model checking의 결과는 그 제한을 정확히 쓸 때 강한 근거가 된다. 실패 없는 깊이와 무제한 보장을 구별하고, trace의 전이 및 관측 기준으로 범위를 확인해야 한다.