블록 두 개를 증명해도 연결된 데이터는 틀릴 수 있다

생산 모듈과 소비 모듈을 각각 검증했는데, 둘을 연결하자 데이터가 달라진다. 두 증명 중 하나가 틀렸을까? 그럴 수도 있지만, 먼저 각 증명이 보장한 관계에 연결부의 의미가 포함됐는지 봐야 한다. assume-guarantee는 큰 회로를 나눠 검증하는 방법이면서, 모듈 경계에서 남은 책임을 드러내는 방법이기도 하다.

가정의 공급자를 적어 두기

모듈을 독립적으로 검증할 때 입력의 모든 조합을 허용하면 현실에 없는 프로토콜 위반까지 검사하게 될 수 있다. 그래서 환경이 지킬 조건을 가정하고, 그 조건 아래에서 모듈이 지킬 동작을 증명한다. 이를 간단히 쓰면 환경 가정 A → 모듈 보장 G다. SymbiYosys에서 assume은 허용하는 동작을 제한하고 assert는 그 동작에 대해 확인할 조건을 지정한다. SymbiYosys의 assume·assert 의미

중요한 것은 A를 누가 실제로 만족시키느냐다. 소비 모듈이 “입력 데이터는 대기 중 바뀌지 않는다”고 가정했다면, 상위 회로나 생산 모듈이 그 조건을 보장해야 한다. 소비 모듈의 로컬 증명에 그 문장이 등장했다는 사실만으로 연결된 시스템의 입력이 그렇게 행동하는 것은 아니다.

포트 형식도 보장의 증거가 되지는 않는다. Chisel의 공식 설명은 DecoupledIO 자체에는 valid·ready의 철회나 bits의 안정성에 대한 보장이 없다고 명시한다. IrrevocableIO에는 더 강한 관례가 있지만 인터페이스가 이를 자동으로 검사하거나 assertion을 생성하지는 않는다. 같은 ready-valid 선 세트를 사용해도 실제 계약은 달라질 수 있다. Chisel의 ready-valid 인터페이스 정의

따라서 연결도 옆에는 신호 이름뿐 아니라 가정과 보장도 있어야 한다. 대기 중 데이터 유지, 전송이 성립하는 에지, 리셋으로 취소되는 요청, 데이터의 비트 의미를 구체적으로 적는다. 그중 상대 모듈이 보장하는 조건과 외부 환경이 책임지는 조건을 구분하면, 증명 사이에 비어 있는 부분이 보인다.

두 로컬 증명을 모두 통과하는 잘못된 연결

8비트 값을 그대로 전달하는 가상 경로를 만들자. 생산 모듈 P는 받아들인 값을 순서대로 내보내며, valid=1이고 ready=0인 동안 데이터와 valid를 유지한다고 보장한다. 소비 모듈 C는 그런 안정된 입력을 가정하고, 실제로 받은 값을 변경 없이 기록한다고 보장한다. 여기서는 같은 클록을 쓰고, 설명할 전송 사이에 리셋이 없다고 정한다.

P와 C 사이에 데이터의 상위 4비트와 하위 4비트를 바꾸는 잘못된 어댑터를 끼워 보자. valid와 ready는 정상 연결돼 있다. P가 0x12를 보내면 C에는 0x21이 들어간다. P가 대기 중 0x12를 유지하면 어댑터의 출력도 대기 중 0x21로 유지된다. C의 안정성 가정은 충족되고, C는 자신이 받은 0x21을 정확히 기록한다.

P의 출력이 입력과 같다는 검사도, C가 받은 값을 그대로 기록한다는 검사도 이 상황에서 성립한다. 하지만 시스템의 입력과 최종 기록이 같다는 요구는 깨진다. 두 로컬 명세에는 P의 출력값과 C의 입력값이 동일한 뜻으로 연결돼야 한다는 관계가 빠져 있었다.

이는 드문 숫자 하나에만 생기는 오류도 아니다. 8비트 입력 256개 중 두 4비트 조각이 같은 값은 0x00, 0x11부터 0xFF까지 16개다. 나머지 240개는 조각을 바꾸면 값이 달라진다. 우연히 0xAA만 확인한 연결 테스트는 통과할 수 있지만, 비트 매핑을 전수 비교하면 숨은 책임을 쉽게 드러낼 수 있다. 이 숫자는 가상 어댑터의 경우의 수이며 실제 제품 검증 결과는 아니다.

보장들을 연결하려면 연결 자체도 증명해야 한다

이 예에서 필요한 추가 조건은 간단하다. 전송되는 데이터에 대해 C 입력과 P 출력의 대응을 확인하고, 제어 신호가 같은 전송을 가리키는지도 확인한다. 그 연결 관계가 성립해야 P의 데이터 보존 보장과 C의 데이터 보존 보장을 이어 붙여 시스템의 데이터 보존을 결론낼 수 있다. OpenTitan은 시스템 수준 연결을 별도로 지정하고 형식 검증하는 connectivity 테스트 흐름을 제공한다. OpenTitan의 연결 검증 설명

상태가 있는 어댑터라면 한 에지의 선 비교로 끝나지 않는다. 어느 입력 전송이 어느 출력 전송에 대응하는지, 버퍼에 남은 데이터가 리셋에서 어떻게 처리되는지까지 관계를 잡아야 한다. 비트가 같아도 서로 다른 요청을 연결했다면 데이터 보존 명세는 틀릴 수 있다.

가정이 서로를 근거로 빙빙 도는 경우도 주의해야 한다. P가 C의 올바른 동작을 가정한 상태에서만 보장하고, C도 P의 올바른 동작을 가정해야만 보장한다면, 두 개의 로컬 PASS만으로 두 가정이 시스템에서 성립한다고 결론낼 수 없다. 시작 상태와 연결 조건을 포함한 정당한 구성 규칙이나 별도의 통합 증명이 필요하다. 가정들이 충돌해 가능한 실행이 사라졌는지도 대표 동작의 도달성으로 살펴볼 수 있다.

블록을 나눈 효과는 증명을 작게 만드는 데 있다. 다만 작은 증명의 경계는 문서에도 남아야 한다. 각 가정의 공급자, 전송 데이터의 대응, 리셋과 초기 상태의 연결을 확인하면 로컬 결과가 시스템의 결론으로 이어진다. “둘 다 검증했다”에서 한 걸음 더 나아가, 두 보장을 연결하는 관계까지 검증했다고 말할 수 있어야 한다.