SystemVerilog 어설션을 감사했을 때 8개의 녹색 정형 증명 중 제출 가능한 것은 5개뿐이었다
합성 정형 보드가 8/8 PROVEN을 보고하는 것을 본 뒤, 자체 감사가 단 5/8만을 TRUSTWORTHY로 인증하는 것을 지켜보았다. 이러한 반전은 AI가 생성한 SystemVerilog 어설션(SVA) 거버넌스의 실행 가능한 데모인 Proof Firewall의 전제이며, 테이프아웃 사인오프 검토에 도달하기 전에 녹색 증명이 충족해야 할 기준에 대한 나의 생각을 바꾸어 놓았다.
불편한 사례일수록 눈에 보여야 하기에, 나는 합성 아비터, 2단계 파이프라인, CDC 크로싱에 픽스처로 작성된 “LLM 작성” 속성을 포함하여 보드를 구축했다. 어설션은 속성 원장에서 완벽히 그럴듯해 보일 수 있다. 정형 엔진은 녹색 결과를 반환할 수 있다. 하지만 함의(implication)가 아무런 실제 검증 작업을 수행하지 않았을 수도 있고, 관련된 설계 동작이 망가진 후에도 계속 통과할 수도 있다. 나는 그동안 PROVEN이라는 단어를 하나의 종착점으로 여겨왔다. 이 데모를 구축하면서 나는 이를 증거 검토의 시작점으로 다루지 않을 수 없게 되었다.
Proof Firewall 데모는 정형 엔진을 대체하거나, 실제 RTL을 수집하거나, 기본 경로에서 라이브 LLM을 호출하지 않는다. 이 데모는 의도적으로 더 작고 검사하기 쉽게 만들어졌다. 순수 Python 명시적 상태 모델 체커가 합성 전이 시스템 IR을 평가한 다음, 거버넌스 게이트가 전건 도달 가능성, 뮤테이션 킬, 영향 영역(COI)을 검사한다. 그 출력은 서명된 시연 인증서를 제출할 근거가 되거나, 사람이 검토하도록 결과를 보류할 근거가 된다.
잘못된 종류의 녹색에서 시작했다
보드의 첫 번째 버전이 매우 깔끔했기에 안도감을 주었던 기억이 난다. 8개의 속성, 8개의 녹색 배지, 그리고 작업이 완료된 것처럼 보이게 만드는 베어 플로우 뷰가 있었다. 나의 초기 본능은 데모가 그 깔끔한 결과를 더 잘 설명하도록 만드는 것이었다. 나는 엔지니어링 과제가 프레젠테이션에 있다고 생각했다. 즉 증명을 표면에 드러내고, 어설션을 보여주며, 대시보드를 더 신뢰하기 쉽게 만드는 일 말이다. 녹색 결과는 진짜였다, 하지만 그것은 검토자가 물어야 할 질문보다 더 협소한 질문에 답하고 있었다.
그런 다음 나는 동일한 8개 속성을 실제 사인오프 제출 논의에서 요구하는 검사들에 통과시켜 보았다. 전건이 참이 된 적이 있는가? 설계의 관련 부분이 변경되면 어설션이 이의를 제기(object)하는가? 의미 있는 COI를 제약하고 있는가? 이러한 질문들은 솔버가 단순히 무엇을 반환했는지가 아니라 증명이 무엇을 입증해 냈는지를 묻기 때문에, 녹색 배지보다 덜 호의적이다.
나는 초기 구축 프레임워크를 포기해야 했다. 8/8 PROVEN을 보여주는 화면은 베어 플로우 기준선의 정확한 모습이었지만, 사인오프 스토리로서는 불완전했다. 방화벽 감사를 거친 후, 동일한 고정 합성 보드는 5개의 TRUSTWORTHY 결과, 1개의 VACUOUS 결과, 그리고 2개의 WEAK 결과를 갖게 된다. 나머지 3개는 성공으로 재라벨링되지 않는다. 그 이유를 설명하는 증거와 함께 보류된다. 증명 라벨과 제출 결정은 서로 다른 결과물이다.
나는 여기서 “거버넌스”라는 단어를 신중하게 선택했다. 데모의 결정론적 검사는 제출 결정을 검토 가능하게 만든다. 선택적 SVA 작성기가 어설션을 제안할 수는 있지만, 평결을 내리는 것은 모델 체커와 정책 게이트다. 에이전트는 조언하고, 코드가 결정한다. 나는 부정적인 결과가 단순한 당혹감에 그치지 않고 유용하게 쓰일 수 있도록 게이트를 충분히 판독 가능하게 만들고자 했다. 보류된 결과에는 검증 엔지니어가 검사하고 재현하며 이의를 제기할 수 있는 이유가 필요하다.
ARB3는 문제를 도저히 무시할 수 없게 만들었다
가장 명확한 실패는 ARB3, 즉 합성 아비터 속성인 assert (g0 && g1) |-> (turn == 0)에서 발견되었다. 베어 플로우에서 이 속성은 녹색이다. 파형과 도달 가능성 증거를 열어보았을 때, 전건 g0 && g1은 해당 합성 아비터에서 도달 불가능했다. 이 함의는 자신이 기술한 상태에 대해 답하도록 강제된 적이 없다는 지극히 좁은 의미에서만 증명되었던 것이다. 전건은 결코 발동하지 않는다.
이러한 차이는 말하기는 쉽지만 검증 대시보드가 온통 녹색으로 가득 차 있을 때는 명심하기 어렵다. 나는 처음에 이 함의를 중재 동작에 관한 주장으로 읽었다. 도달 가능성 결과는 내가 보고 있던 대상의 의미를 바꾸어 놓았다. 그것은 트리거 조건이 결코 발생하지 않은 주장이었다. 이를 VACUOUS로 명명하는 것은 녹색 라벨을 유지하는 것보다 훨씬 유용하다. 검토자의 시선을 증명을 공허하게 만든 가정이나 자극(stimulus)으로 이끌어 주기 때문이다.
정책 라벨을 작업하는 동안 나는 계속해서 이 패널로 되돌아왔다. 그 대안을 고려하기 전까지는 VACUOUS라는 결과가 가혹하게 들릴 수 있다. 만약 사인오프 기록이 전건이 결코 발동하지 않는다는 사실을 기록하지 않은 채 증명을 유지한다면, 검토는 그 증명에 의미를 부여하는 조건이 빠진 결론만을 전달받은 셈이다. 더 나은 기록은 한계를 명시적으로 드러내어 사람이 구체적으로 질문하고 따져볼 수 있는 거리를 남겨주는 기록이다. 그러한 도달 가능성 기록은 평결 바로 옆에 위치해야 한다.
나는 또한 공허성(vacuity)을 단순한 형식적 경고로 취급하려는 유혹을 떨쳐내야 했다. 속성이 중재 조건을 제약하기 위한 것이라면, 도달 불가능한 트리거 동작은 해당 속성이 의도된 동작을 실제로 실행했는지 여부를 보여주는 핵심 증거다. 대시보드는 검토자에게 녹색 결과로부터 이를 알아서 추론하라고 요구해서는 안 된다. 대시보드는 도달 가능성 결과를 보존하고, 해당 결과를 인증서 발급 경로에서 제외하며, 다음 검토 조치를 명확히 제시해야 한다.
업계의 현실은 내게 문제의 중대성을 더욱 절감하게 했다. 데모 사양에서 인용한 2024 Wilson Research Group / Siemens EDA 연구 보고서에 따르면 초도 실리콘 성공률은 14%에 불과하다. 이는 Veriprajna의 측정치가 아니며, 이 합성 보드가 그 수치를 설명한다고 주장하는 것도 아니다. 다만 보기 좋은 대시보드 상태 그 자체를 증거로 취급하지 않도록 경각심을 준다.
파이프라인 속성은 잡아내리라 기대했던 결함을 잡지 못하고 살아남았다
두 번째 실패는 합성 2단계 파이프라인 속성인 PIPE3, 즉 assert v2 |-> (s2 == s2)를 테스트하는 도중에 맞닥뜨렸다. 나는 피상적인 검토를 무사히 통과할 만큼 그럴듯하게 읽히는 간결한 어설션 예시를 원했다. 후건(consequent)은 항진명제(tautology)다. 즉 s2가 자신과 같다고 말할 뿐이다. 후건은 아무것도 제약하지 않는다.
이 데모에서 중요한 조치는 줄글 속에서 항진명제를 단순히 눈으로 찾아내는 것에 그치지 않는다. 거버넌스 게이트는 관련된 단일 지점 설계 뮤테이션을 주입하고, 속성이 이를 제거(kill)하는지 묻는다. 주요 취약 파이프라인 사례의 경우, PIPE3은 0/6 뮤테이션 킬 결과를 기록한다. 이 속성은 결함이 있는 관련 변형체들 속에서도 살아남는다. 이것이 바로 정책이 WEAK를 부여하고, 아무런 검증을 거치지 않은 PROVEN 결과가 제출 증거로 인정받지 못하게 막는 이유다. 뮤테이션 결과는 유용한 민감도를 검증한다.
이 예제를 덜 뻔하게 느껴지도록 만들려 시도하면서 나는 한 가지 불편한 사실을 깨달았다. 사람은 s2 == s2를 읽고 빠르게 지나칠 수 있다. 많은 결함은 이처럼 명백하게 드러나지 않는다. 그렇기 때문에 나는 데모가 운영자가 의심스러운 문자열을 직접 발견하는 것에 의존하기를 원치 않았다. 진정으로 유용한 결과물은 바로 절차다. 즉 도달 가능성, 관련된 뮤테이션 킬 테스트, COI, 그리고 그 이유를 기록하는 정책 결정이다.
나는 뮤테이션 검사를 증명을 지나치게 안이하게 해석하는 태도를 거부하는 체계적인 방법으로 보게 되었다. 그 목표는 극적인 실패를 억지로 만들어내는 것이 아니다. 속성이 자신이 제약해야 할 동작의 국소적인 관련 변화를 감지할 수 있는지 묻는 것이다. 그렇지 못할 때, 그 결과는 검토자에게 실행 가능한 정보를 제공한다. 즉 이 어설션이 사인오프 기록을 뒷받침하기 전에 이를 강화하거나 다른 검토 경로를 거쳐야 한다는 점이다.
이것이 바로 데모의 벤치마크를 엄밀하게 한정하여 설명해야 하는 이유이기도 하다. 로컬에서 실행되는 python -m backend.bench 실행은 고정된 라벨이 부착된 합성 어설션 세트에 대해 18/18 점을 기록하며, 게이트가 없는 데모 자체의 기준선이었다면 무비판적으로 승인했을 6개의 증명을 식별해 낸다. 이 수치들은 이 데모의 라벨링된 픽스처에 대한 재현성 검증일 뿐이다. 이는 상용 환경에서의 성공률이나 AI가 작성한 어설션 전반에 대한 주장이 아니며, 상용 정형 도구와의 비교도 아니다.
게이트를 관대하게 보이도록 만들려는 시도를 멈추었다
첫 번째 감사 결과가 나온 후 내게는 설계상의 선택지가 있었다. 보드가 더 낙관적으로 느껴지도록 보류 평결을 완화할 것인가, 아니면 방어할 수 없는 것에 대해서는 보드가 인증을 거부하도록 둘 것인가. 나는 후자를 택했다. 실제 사인오프 검토에서는 완전한 증명과 바운디드(bounded) 증명을 구별하고, 도달 불가능한 전건과 의미 있는 속성을 가려내며, 취약한 검사와 관련된 결함 동작에 반응하는 검사를 분별할 수 있는 능력이 필요하기 때문이다. 보류는 검토의 한 가지 결과이지, 막다른 골목이 아니다.
그러한 선택은 정책 용어 체계에 잘 드러나 있다. TRUSTWORTHY는 서명된 시연 인증서를 획득한다. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD, 그리고 VIOLATED는 해당 인증서를 보류하거나 결과를 에스컬레이션하는 서로 다른 이유들을 보존한다. 예를 들어 CDC 픽스처에서 더 엄격한 속성인 assert (req && !ack) |-> ##1 req는 VIOLATED 상태가 되며 구체적인 합성 반례 파형을 생성한다. 이는 트랜잭션 유실이나 CDC 실패 유형을 보여준다. 고객의 칩에 대해서는 아무것도 말해주지 않는다.
나는 이것을 검증 팀의 기존 엔진을 대체하라는 제안으로 보지 않는다. 상용화 방향은 엔진에 구애받지 않는(engine-agnostic) 방식이다. 즉 기존 정형 워크플로 주위에 게이트를 배치하고 그 수용 기준을 검사할 수 있게 만드는 것이다. 실제 엔진 어댑터와 RTL 수집은 이 데모에서는 뒤로 미루어 두었다. 시연된 범위는 의도적으로 좁게 설정되었다. 그러한 경계는 주장의 수준을 실제로 실행되는 범위에 비례하도록 유지해 주기 때문에 중요하다.
이제 나는 평결 옆에 영수증이 놓이기를 원한다
어설션 작성자가 AI의 도움을 받을 때 사인오프 회의에 필요한 결과물이 무엇인지 계속 생각하게 된다. 그것은 작성자의 신뢰도 점수가 아니다. 어떤 검사가 실행되었는지, 도달 가능성 결과가 어떠했는지, 어떤 뮤테이션이 제거되었는지, COI에 무엇이 포함되었는지, 그리고 왜 정책이 인증을 허용하거나 보류했는지를 명시하는 기록이다. 검토에는 다시 열어 검증할 수 있는 증거가 필요하다.
이것이 바로 데모가 signoff_certificate.json 파일로 내보내는 내용이다. 즉 속성별 평결, 도달 가능성, 뮤테이션 결과, COI, 해당되는 경우의 반례 기록, 그리고 SHA-256 필드다. 검토자가 맹목적으로 녹색 배지를 신뢰하지 않고도 결정을 재구성할 수 있어야 하기에, 나는 이 인증서를 시연용 기록으로 구축했다. 인증서는 평결에 이르는 경로를 보존해야 한다.
그리고 내가 설명하는 글을 읽기보다 직접 눈으로 보고 싶다면, 여기 전체 과정이 처음부터 끝까지 실행되는 모습을 확인할 수 있다.
8/8에서 5/8로의 반전을 단순한 구호로 반복하는 대신 직접 검사해 볼 수 있도록 나는 이 데모를 직접 실행할 수 있게 만들었다. 이를 통해 내가 얻은 결론은 소박하지만 확고하다. 제출할 가치가 있는 증명은 무엇을 제약했는지, 어떤 결함에서 살아남았는지, 그리고 왜 이를 신뢰할 수 있는지에 대한 증거를 수반한다는 점이다. 녹색 표시는 여전히 유용하다. 다만 다음 검토자가 그것이 더 멀리 나아갈 자격이 있는지 판단할 수 있게 해주는 기록이 필요할 뿐이다.
