합성 AI 생성 SVA를 위한 테이프아웃 사인오프 거버넌스

고정된 합성 보드에서 8/8 PROVEN은 감사 후 5/8 TRUSTWORTHY로 전환됩니다.

Proof Firewall은 합성 PROVEN SystemVerilog 어설션이 사인오프 파일에 들어가기 전에 공허성, 어설션 강도, 영향 콘을 다시 감사(re-audit)합니다. 고정된 보드에서 8/8 베어 플로우 증명을 5개의 인증된 TRUSTWORTHY 결과로 전환하고 나머지는 이유와 함께 사람 검토로 라우팅합니다. 에이전트는 조언하고, 코드가 결정합니다.

8/8에서 5/8로

PROVEN에서 TRUSTWORTHY로

방화벽 감사 후의 고정 합성 8개 프로퍼티 보드

0/6

PIPE3 변이 킬

주요 합성 약한 파이프라인 사례

18/18

라벨링된 합성 벤치마크 일치도

로컬 데모 벤치마크이며, 오픈월드 정확도 주장이 아닙니다

이것은 픽스처로 작성된 합성 전이 시스템 설계와 프로퍼티를 사용하는 실행 가능하고 재현 가능한 데모입니다. 기본 경로에서 고객 RTL, 클라우드 솔버 또는 실시간 LLM 호출을 사용하지 않습니다.

사인오프 실패는 그린 결과 안에 숨겨져 있습니다

2024년 Wilson Research Group 및 Siemens EDA 연구에서 최초 실리콘 성공률은 14%로 보고되었습니다. 어설션이 AI에 의해 작성되었을 수 있는 경우 정형 결과는 더 면밀한 검토가 필요합니다. 전건(antecedent)이 결코 발생하지 않거나 후건(consequent)이 유용한 제약을 전혀 가하지 않기 때문에 함의문이 PROVEN으로 판정될 수 있습니다.

Proof Firewall은 그 결정을 위한 결정론적 증명 후 거버넌스 게이트입니다. 정형 엔진이 틀렸다고 선언하는 것이 아닙니다. 증명이 사람의 테이프아웃 사인오프를 위해 제출할 만큼 충분히 방어 가능한지 묻고, 인증하거나 보류하는 모든 결과에 대해 구체적인 이유를 남깁니다.

거버넌스 게이트의 작동 방식

핵심 기준은 증명 품질입니다. 각각의 결정론적 검사는 그린 증명이 제출될 만큼 충분한 실질적 내용을 가지고 있는지 테스트합니다.

신뢰를 부여하기 전 도달 가능성 검증

명시적 상태 모델 체커(explicit-state model checker)는 합성 전이 시스템 IR에서 함의문의 전건이 발생할 수 있는지 테스트합니다. 도달할 수 없는 전건은 증거로 제출되는 대신 VACUOUS로 라우팅됩니다.

강도 검증을 위한 변이 킬 테스트

관련 단일 지점 설계 변이(mutation)를 통해 어설션이 결함이 있는 변형을 거부하는지 테스트합니다. 이러한 변이에서 살아남은 프로퍼티는 그린 솔버 결과의 신뢰도를 차용하도록 허용되지 않고 WEAK로 라우팅됩니다.

COI 및 정책 라우팅

게이트는 영향 콘(COI)을 계산하고 TRUSTWORTHY, BOUNDED-PROVEN, VACUOUS, WEAK, DEAD 또는 VIOLATED를 할당합니다. 오직 TRUSTWORTHY만이 서명된 시연 인증서를 받습니다.

데모의 순수 Python 명시적 상태 체커는 유한 모델에서 도달 가능성과 반례 트레이스를 찾습니다. 유계 깊이 폴백(bounded-depth fallback)은 무조건적인 증명으로 재구성되지 않고 유계(bounded)로 라벨링됩니다.

합성 보드에서의 상세 증명 검토

모든 이미지는 실행 중인 합성 데모의 스크린샷입니다. 보드는 8개의 PROVEN 베어 플로우 결과로 시작하며, 감사를 통해 보류된 증거를 시각화합니다.

감사는 3개의 그린 결과를 뒤집습니다

테이프아웃 사인오프 보드는 베어 플로우 뷰에서 처음에 8/8 PROVEN을 표시합니다. 방화벽 감사 후 5/8가 TRUSTWORTHY로 인증되며, 나머지 3개는 1개의 VACUOUS 및 2개의 WEAK 프로퍼티입니다. 이것은 고정된 합성 픽스처이며 고객 설계나 상용 엔진 결과가 아닙니다.

8개의 합성 프로퍼티 중 5개가 TRUSTWORTHY로 표시되고 1개의 VACUOUS 및 2개의 WEAK 결과가 검토를 위해 보류된 것을 보여주는 Proof Firewall 테이프아웃 사인오프 보드. — 감사된 합성 보드: 방화벽이 8/8 PROVEN 뷰를 5개의 TRUSTWORTHY 인증서와 3개의 이유가 명시된 보류로 변환합니다.

ARB3는 트리거가 발생하지 않으므로 아무것도 증명하지 못합니다

합성 ARB3 어설션인 assert (g0 && g1) |-> (turn == 0)은(는) 합성 아비터에서 전건에 도달할 수 없으므로 VACUOUS입니다. 이 결과는 증명된 함의문이라도 여전히 아무것도 인증하지 못할 수 있는 이유를 보여줍니다.

g0 및 g1 전건에 도달할 수 없어 VACUOUS로 분류된 ARB3를 보여주는 합성 아비터의 파형. — ARB3: 도달 불가능한 전건이 그린 함의문을 VACUOUS 결과로 바꿉니다.

PIPE3는 잡아내야 할 변이에서 살아남습니다

합성 PIPE3 어설션인 assert v2 |-> (s2 == s2)은(는) WEAK입니다. 동어반복적인 후건이 주입된 관련 변이에서 살아남으며, 주요 파이프라인 사례에서 0/6 변이 킬을 기록합니다.

6개 중 0개의 변이 킬을 기록한 후 WEAK로 분류된 동어반복적 프로퍼티 PIPE3를 보여주는 합성 파이프라인의 파형. — PIPE3: 동어반복적 후건이 0/6 변이 킬 테스트 후 WEAK 결과를 얻습니다.

더 강력한 CDC 프로퍼티는 자체 반례를 보여줄 수 있습니다

합성 약한 CDC2 프로퍼티는 WEAK입니다. 이를 다음과 같이 강화하면 assert (req && !ack) |-> ##1 req 합성 CDC 픽스처에서 VIOLATED가 되며 구체적인 반례 파형을 생성합니다. 이는 실제 칩에 대한 주장이 아니라 트랜잭션 유실 CDC 결함 클래스를 보여줍니다.

픽스처에서 VIOLATED로 분류된 강화된 합성 CDC 프로퍼티의 구체적인 반례 파형. — 강화된 합성 CDC 프로퍼티는 VIOLATED이며, 검토자가 검사할 수 있는 반례가 포함되어 있습니다.

검토는 구조화된 영수증을 남깁니다

서명된 시연 인증서는 각 프로퍼티의 판정, 도달 가능성, 변이 결과, COI, 해당 시 반례 기록 및 SHA-256 필드를 기록합니다. 검토자가 상태 변경 이유를 추론할 필요 없이 감사를 검토할 수 있도록 합니다.

프로퍼티별 판정, 도달 가능성, 변이 결과, 영향 콘, 반례 기록 및 SHA-256 필드를 보여주는 Proof Firewall 서명된 시연 인증서. — 서명된 시연 인증서는 인증 또는 사람 검토 뒤에 있는 증거를 보존합니다.

대체 솔버가 아닌, 엔진 독립적인 프로덕션 방향

Proof Firewall은 증명 증거를 둘러싼 게이트를 시연합니다. 아래 범위는 데모가 수행하는 작업과 연기된 작업을 구분합니다.

항목	Proof Firewall 데모	프로덕션 방향
증명 입력	픽스처 작성 합성 전이 시스템 IR 및 SVA	고객의 기존 정형 플로우를 둘러싼 게이트
시연된 검사 항목	공허성, 변이 킬 테스트, COI, 정책 라우팅, 인증서 내보내기	제공된 증명 증거에 적용되는 동일한 거버넌스 질문
정형 엔진	실제 엔진 어댑터 없음	엔진 독립적 방향이며, 통합에 대한 주장이 아님
결과 처리	TRUSTWORTHY 인증서 및 이유가 설명된 보류	구조화된 증거 기록을 통한 사람 사인오프 검토

이 데모가 하지 않는 것

✓ Verilog 또는 SystemVerilog RTL을 파싱하지 않으며, 고객 RTL, GDSII 또는 실제 칩 설계에서 작동하지 않습니다. V1은 합성 전이 시스템 IR 픽스처를 사용합니다.
✓ JasperGold, VC Formal, Questa Formal, SymbiYosys 또는 기타 정형 엔진을 대체하지 않습니다. 실제 엔진 어댑터는 연기되었습니다.
✓ 기본적으로 실시간 LLM을 사용하지 않습니다. 프로퍼티는 픽스처로 작성된 LLM 생성 SVA이며, 기본 기록 경로는 결정론적입니다.
✓ 테이프아웃 준비성, 안전 인증, 재스핀 제로, 고객 성과, 배포, ROI 또는 규제 자격을 주장하지 않습니다.
✓ 5/8, 18/18, 0/6 또는 7/7을 프로덕션 또는 업계 전반의 성능으로 제시하지 않습니다. 이는 고정된 로컬 합성 픽스처 및 테스트의 결과입니다.

검증 책임자들이 묻는 질문

우리는 이미 정형 검증을 실행하고 있습니다. 왜 PROVEN 결과 뒤에 또 다른 게이트를 두어야 하나요?

PROVEN 결과라 하더라도 도달할 수 없는 전건이나 관련 설계 동작이 손상되었을 때 실패하지 않는 프로퍼티에 기반하고 있을 수 있습니다. Proof Firewall은 이러한 질문에 대한 결정론적 증명 후 게이트(도달 가능성, 변이 킬 테스트, 영향 콘 및 정책 라우팅)를 시연합니다. 정형 엔진을 대체하지 않으며, 프로덕션 방향은 기존 정형 플로우를 감싸는 엔진 독립적 게이트입니다.

Proof Firewall은 현재 JasperGold, VC Formal, Questa Formal 또는 SymbiYosys에 연결되나요?

아니요. 본 데모에서는 실제 엔진 어댑터가 연기되었으므로 JasperGold, VC Formal, Questa Formal, SymbiYosys 또는 기타 정형 엔진의 대체품으로 해석해서는 안 됩니다. 시연된 프로덕션 방향은 고객의 기존 정형 워크플로우를 둘러싼 엔진 독립적 거버넌스 게이트입니다.

이 결과들은 고객 RTL이나 실시간 AI 어설션 생성기에서 나온 것인가요?

아니요. 보드, SystemVerilog 어설션, 설계, 벤치마크 및 반례는 합성된 것입니다. 기본 기록 경로는 고객 RTL이나 실시간 LLM 호출이 아닌, 픽스처 작성 LLM 생성 SVA 프로퍼티와 합성 전이 시스템 IR을 사용합니다.

8/8에서 5/8 결과는 실제로 무엇을 측정한 것인가요?

고정된 합성 8개 프로퍼티 보드입니다. 베어 플로우 기준선은 8/8 PROVEN을 표시하지만, 방화벽 감사 후 5개는 TRUSTWORTHY로 인증되고 1개는 VACUOUS, 2개는 WEAK로 분류됩니다. 이는 프로덕션 RTL 비율이나 고객 결과, 또는 합성 AI 생성 어설션에 대한 일반적인 결과가 아닙니다.

데모는 어설션이 공허하거나 약하다고 어떻게 결정하나요?

거버넌스 게이트는 전건이 도달 가능한지 확인하고, 관련 단일 지점 설계 변이를 실행하며, 각 프로퍼티의 영향 콘을 계산합니다. ARB3는 합성 아비터에서 전건에 도달할 수 없기 때문에 VACUOUS입니다. PIPE3는 동어반복적인 후건이 주입된 관련 변이에서 살아남아 주요 파이프라인 사례에서 0/6 변이 킬 결과를 기록하기 때문에 WEAK입니다.

검토자는 이 데모에서 어떤 증거를 가져갈 수 있나요?

UI는 프로퍼티별 판정, 도달 가능성, 변이 결과, 영향 콘, 해당 시 반례 기록 및 SHA-256 필드가 포함된 signoff_certificate.json을 내보냅니다. 오직 TRUSTWORTHY만이 서명된 시연 인증서를 받으며, BOUNDED-PROVEN, VACUOUS, WEAK, DEAD, VIOLATED 결과는 이유와 함께 사람 검토를 위해 보류됩니다.

기술 연구

이 데모의 배경 연구 — 아키텍처, 검증 설계 및 엔터프라이즈 청사진.

전체 솔루션

반도체 AI 검증 및 실리콘 정확성 솔루션 살펴보기 →

사인오프 논의에 증명 품질 거버넌스 도입하기

고위험 AI 지원 엔지니어링 워크플로우를 위한 결정론적 증거 경로에 대해 검증 리더 여러분과의 논의를 환영합니다.

다음으로 유용한 논의는 팀이 검사해야 하는 증명 아티팩트, 검토자가 방어할 수 있는 정책 경계, 그리고 엔진 독립적 프로덕션 방향에 필요한 사항에 관한 것입니다.

증명 거버넌스 평가

✓ 현재 증명 검토 경로 매핑
✓ 공허성 및 강도 증거 식별
✓ 사인오프 정책 상태 정의
✓ 검토 가능한 인증서 기록 명세

거버넌스 경로 설계

✓ 엔진 독립적 증거 게이트 설계
✓ 결정론적 정책 라우팅 구축
✓ 감사 및 예외 워크플로우 모델링
✓ 사람 사인오프 핸드오프 계획

WhatsApp으로 연결하기 저희 팀에 이메일 보내기