정형 검증기는 "증명됨"이라고 했다. 그런데 칩은 여전히 망가져 있었다.
우리 자체 도구 중 하나가 처음으로 내게 거짓말을 했을 때, 그것은 정중하게 그렇게 했다. 정형 엔진은 녹색 체크 표시를 반환했다. 우리가 증명을 요청했던 모든 속성이 증명됨 상태로 되돌아왔다. 어설션 라이브러리는 완전해 보였다. 서류상으로는 설계가 검증되어 있었다.
그 인증서가 무가치하다는 것을, 그리고 내가 반도체 AI 검증에 대해 가정했던 모든 것이 우리를 엉뚱한 실패로부터 지켜 주고 있었다는 것을 깨닫는 데 이틀이 걸렸다.
그 속성들은 우리가 정형 엔진을 감싸서 만든 대규모 언어 모델이 생성한 것이었다 — 정확히 모두가 만들고 있던 그 매끈한 에이전트형 칩 설계 데모 같은 것이었다. 그리고 엔진은 그것들을 밀리초 만에 증명했는데, 그것이야말로 신호였어야 했다. 그것들이 증명된 것은 그것들을 시험할 조건이 결코 발동하지 않았기 때문이었다. '모든 요청은 결국 승인을 받는다'고 말하는 속성은, 그 요청이 결코 일어날 수 없다면 자명하게 참이다. 솔버가 틀린 게 아니었다. 그것은 우리가 실수로 던진 질문에 답했고, 그 질문은 공허했다. 바로 그 순간 나는 이 AI 검증 파이프라인이 실제로 무엇을 방어해야 하는지 — 그리고 왜 그것을 파는 사람들 거의 아무도 옳은 대상을 방어하고 있지 않았는지 — 를 이해했다.
우리가 무엇을 발견했는지 말하고 싶다. 현대 칩을 죽이는 버그 부류는 업계가 잡을 수 있다고 광고하는 그것이 아니기 때문이다. 우리는 팹리스 칩 팀을 위한 맞춤형 검증 파이프라인을 만든다 — 팀이 이미 보유한 정형 엔진을 감싼, 파인튜닝된 오픈 웨이트 모델로, 전적으로 그들 자신의 하드웨어에서 돌아간다 — 그리고 이 접근 전체는 먼저 이것을 잘못한 데서 나왔다. 그 형태는 여기서 볼 수 있다: veriprajna.com/solutions/semiconductor-ai-verification. 하지만 이 접근은 '통과한' 설계가 실패하는 것을 직접 본 뒤에야 비로소 이해가 된다.
모든 팹리스 CFO를 겁먹게 해야 할 숫자 하나
통계 하나가 문제 전체를 규정한다. 업계에서 가장 오래 이어져 온 벤치마크인 2024년 Wilson Research Group / Siemens EDA 기능 검증 연구는 초도 실리콘 성공률을 14%로 잡았다. 20년간 추적해 온 이래 가장 낮은 수치다. 2020년에 그 숫자는 약 32%였다. 4년 만에 절반 넘게 떨어진 것이다.
이것은 엔지니어들이 게을러졌다는 이야기가 아니다. 복잡성이 도구를 앞질렀다는 이야기이자, 사양이 그것을 뒤쫓는 테스트벤치보다 더 빠르게 변형된다는 이야기다. 같은 연구는 대략 리스핀의 70%가 사양 변경과 관련된 오류로 인해 발생한다는 것을 발견했다 — 순수한 논리 버그가 아니라.
초도 실리콘 성공률이 떨어진 것은 칩 팀이 나빠져서가 아니다. 이제 사양이, 검증이 그것을 마무리할 수 있는 속도보다 더 빠르게 움직이기 때문에 떨어진 것이다.
나는 그 70%라는 숫자를 오랫동안 곱씹었다. 그것이 수많은 '칩 설계용 AI' 세일즈를 조용히 고발하기 때문이다. 대부분의 리스핀이 사양 표류에서 온다면, 논리 버그만 잡는 도구는 문제의 한 조각을 다루면서 그것을 파이 전체라고 부르는 셈이다.
그리고 틀렸을 때의 비용은, 소프트웨어를 하는 사람들이 과소평가하는 방식으로 잔혹하다. 5nm 마스크 세트는 $10–20M이 든다. 3nm에서는 $40M에 육박하며, EUV 레이어 20개 이상을 포함해 마스크 레이어가 70개가 넘는다. 완전한 2nm 테이프아웃은 이제 $725M 규모의 총비용이 든다. 무언가가 빠져나가면, 리스핀은 마스크 비용에 더해 3~6개월의 일정 지연을 의미한다. 18개월짜리 제품 창에서 6개월의 지연은 칩 생애 매출의 절반을 지워 버릴 수 있다. CFO는 검증을 비용 센터로 보지 않는다. 그들은 그것을 단 한 번의 여덟 자리 숫자짜리 실수에 대비하는 보험으로 본다.
LLM은 하드웨어에서 실제로 어떻게 환각하는가?
당신의 팀은 이미 Verilog에 LLM을 쓰고 있다. 나는 아닌 척하지 않을 것이고, 당신에게 파는 누구도 그래서는 안 된다. 이 연구 분야는 이제 실재한다 — LLM이 Verilog를 작성하는 것에 관한 논문은 2020년 한 편에서 2025년 64편으로 늘었다. VerilogEval 벤치마크의 더 어려운 문제들에서, GPT-4급 모델은 약 43%의 기능적 정확도에 이른다. 유용하다. 하지만 믿을 만하지는 않다.
흥미로운 질문은 모델이 도움이 되느냐가 아니다. 그것은 바로 그것들이 어떻게 실패하는가이다 — 그 실패 양상이 소프트웨어 엔지니어가 두려워하도록 훈련받은 실패와 닮지 않았기 때문이다. '올바르게 보이는' RTL이 왜 잘못됐는지 밤늦도록 들여다본 끝에, 나는 그 실패들을 다섯 가지 부류로 분류하기 시작했다.
첫 번째는 무해한 것이다. 구문적 환각 — 그냥 컴파일되지 않는 코드다. Verilator나 합성 프런트엔드가 몇 초 만에 잡는다. 다들 이미 이것을 다룰 줄 알며, 사람들이 문제가 해결됐다고 주장하고 싶을 때 가리키는 부류가 바로 이것이다.
두 번째는 아프기 시작하는 지점이다. 의미적 환각이며, 교과서적 사례는 블로킹 대 논블로킹 할당이다. 파이썬과 C로 훈련된 모델은 Verilog를 문장이 위에서 아래로 실행되는 것처럼 읽는다. 그래서 모델은 블로킹 할당 — 평범한 = 를 — 클록 구동 always_ff 블록 안에 작성한다, 그 언어가 논블로킹 <= 를 요구하는데도 말이다. 설계자는 2사이클 파이프라인을 원했다. 블로킹 할당을 쓰면 두 번째 스테이지는 첫 번째 단의 새로운 값을 읽는다 — 옛 값이 아니라. 그래서 실리콘은 2사이클이 아니라 1사이클 바이패스를 내보낸다. 일부 시뮬레이터는 이 경쟁 상태를 완전히 감추는 순서로 이벤트를 스케줄한다. 시뮬레이션은 멀쩡히 돈다. 하지만 합성 결과는 엉뚱한 기계가 된다.
세 번째 부류는 내게 AMBA 사양을 보조 모니터에 항상 띄워 두도록 가르친 것이다. 프로토콜 환각. 코드는 컴파일되고, 지정 테스트의 90퍼센트를 통과한 뒤, 슬레이브가 주소를 받을 준비가 되기도 전에 write-data-valid 신호를 어서트한다 — AXI 핸드셰이크 위반이다. 또는 valid 신호를 높게 유지한 채 그 아래 데이터를 뒤바꾼다. 또는 어떤 인간도 외우지 못한, 버스 사양 84페이지에 묻힌 하위 조항을 건드린다. 그 칩은 내부 테스트 하네스에서는 완벽하게 동작하다가, 서드파티 메모리 컨트롤러에 연결되는 순간 멈춰 버린다. 이것은 시뮬레이션 사이클을 더 돌린다고 무차별로 해결할 수 없다. 각 프로토콜에 대해 작성된 사전 검증 어설션 라이브러리로 잡아낸다.
네 번째 부류는 우리를 속인 바로 그것이며, 위험한 것이다.
왜 '증명됨'이 검증 보고서에서 가장 위험한 단어인가?
공허성 환각. 모델이 SystemVerilog 어설션을 생성한다. 정형 엔진이 그것을 증명한다. 당신은 출하한다. 그런데 그 속성은, 그 전제 — 'if' 부분 — 가 애초에 참이 된 적이 없었기 때문에 자명하게 참이었을 뿐이다.
중재기(arbiter) 속성을 떠올려 보라: 요청이 올라오면, 몇 사이클 안에 반드시 승인이 뒤따라야 한다. 이제 같은 모델이 도움이 되려고 request 신호를 강제로 낮게 만드는 가정(assumption)까지 작성했다고 하자. 정형 엔진은 그 승인 속성을 밀리초 만에 충실히 증명하는데, 그것을 위반할 요청 자체가 존재하지 않기 때문이다. 그 아래 실제 중재기는 완전히 망가져 있을 수도 있다. 인증서에는 '증명됨'이라고 적혀 있다. 그것은 무가치하다.
밀리초 만에 끝나는 정형 증명은 빠른 것이 아니다. 그것은 의심스러운 것이다. 엔진이 아무것도 증명하지 않았을 수도 있다.
이것은 변방의 위험이 아니다. Siemens는 2017년부터 공허한 증명에 대한 경고를 발표해 왔지만, 이 분야는 여전히 자동 공허성 검사가 없는 플로우를 출하한다. 공허성 탐지가 없는 정형 검증 플로우가 더 나쁘다 — 정형 검증이 전혀 없는 것보다 말이다 — 고 하면 사람들은 내가 과장한다고 여긴다. 그렇지 않다. 검증이 없으면 당신은 적절히 겁먹은 상태가 된다. 공허한 '증명됨'은 당신을 확신에 차 있으면서도 틀리게 만들고, 사인오프된 블록이 테이프아웃으로 향하게 한다. 그것이 우리 초기 프로토타입에서 하마터면 출하될 뻔한 실패였고, 우리가 만드는 것을 영구히 바꿔 놓았다.
다섯 번째 부류는 시뮬레이션이 구조적으로 볼 수 없는 것이다. 클록 도메인 교차(CDC) 사각지대. LLM은 신호 이름을 읽을 뿐, 클록 도메인을 인지하지 못한다. 그래서 2 GHz CPU 도메인의 신호를 400 MHz 주변장치 도메인 플롭에 곧바로 연결하면서, 준안정성을 막아 주는 더블 플롭 동기화기를 건너뛴다. RTL 시뮬레이션은 준안정성을 모델링하지 않는다 — 그래서 회귀 테스트는 매번 통과하고, 실리콘은 현장에서 교착에 빠진다. 이것이 CDC 버그가 마스크 세트를 잡아먹는 이유다. 또한 이것이 Accellera가 2024년에 CDC/RDC 상호운용 표준을 시작한 이유다: 상용 CDC 도구들 간의 파편화가 사인오프를 깨뜨릴 만큼 심각해졌던 것이다.
두 번째부터 다섯 번째까지의 부류는 한 가지 무서운 속성을 공유한다: 이들은 시뮬레이션을 통과한다. 이들은 오직 실리콘에서만 드러난다. 그것이 여전히 테이프아웃을 날려 버리는 버그 부분집합이며, 정확히 '논리 버그를 잡는다'는 세일즈가 손대지 않고 남겨 두는 부분집합이다.
칩 팀이 실제로 마주 서 있는 벤더의 벽
테이프아웃에 대해 진정으로 독립적인 도움을 찾아 나섰을 때, 나는 몇 년 전보다 더 적은 선택지밖에 얻지 못했다 — 그리고 이것은 향수가 아니라 시장 구조다. 설계검증 리드가 실제로 고를 수 있는 세 EDA 벤더 — Synopsys, Cadence, Siemens — 는 10년 전 시장의 75% 미만에서 오늘날 85% 이상으로 올라섰다. 여기에 Synopsys의 $35B 규모의 Ansys 인수를 더하면 상위 4개사가 약 90%를 지배한다. 팹리스 스타트업이 쇼핑하는 시장은, 문제가 어려워진 바로 그 시점에 넓어진 것이 아니라 좁아졌다.
그리고 기존 강자들도 AI에서 가만히 있지 않는다. Synopsys는 AgentEngineer를 2026년 3월에 출시했는데, 생산성 2~5배를 주장하는 에이전트형 검증 워크플로우로, VC Formal 위에서 동작한다 — 내가 평가해 본 것 중 가장 신뢰할 만한 벤더 에이전트 스택이다. Cadence는 ChipStack AI Super Agent를 2026년 2월에 발표했고, 강화학습 기반 구현을 위한 Cerebrus AI Studio를 운영하며, JasperGold는 나머지 모두가 견주어지는 표준(gold-standard) 정형 엔진으로 남아 있다. 나는 에두르지 않고 말한다: JasperGold와 VC Formal은 정말로 뛰어나다. 이들을 헐뜯으며 세일즈를 시작하는 사람은 자신이 실제 테이프아웃을 한 번도 마무리해 본 적 없음을 스스로 말한 셈이다.
함정은 가격과 태세다. JasperGold의 과거 기준가는 약 $225K에 좌석당 $45K 수준이었다 — 대형 팹리스 회사에는 괜찮지만, 가장 흥미로운 작업을 하는 초기 단계 RISC-V 및 AI 가속기 스타트업에는 손이 닿지 않는다. 게다가 기존 강자들의 최신 AI 기능은 클라우드 우선이어서, 이 고객들이 결코 양보하지 않을 단 하나의 요구사항과 정면으로 충돌한다. 이에 대해서는 곧 더 다루겠다.
그다음은 스타트업의 물결인데, 그 소음이 요란하다. 지난 DAC와 DVCon에서, 내가 함께 일하는 한 DV 리드는 한 분기 만에 서로 다른 '칩 설계용 에이전트형 AI' 회사 여덟 곳으로부터 세일즈를 받았다. ChipAgents는 2026년 초 기준 $74M을 조달했고 설계·검증 생산성 10배를 주장한다. Normal Computing는 삼성의 Catalyst Fund가 주도하여 $50M을 조달했고, 자동 정형화(auto-formalization) — 엔지니어의 의도를 정형 속성으로 직접 변환하여 증명하는 LLM — 를 구축하고 있으며, 세계 10대 반도체 설계 회사의 절반이 이를 사용하고 있다고 말한다. 더 있다: 전체 테스트벤치를 생성하는 MooresLabAI, 회귀 분석의 Bronco, 전력-성능-면적 예측의 Silimate.
이들 중 일부는 진짜다. 하지만 어느 것도 고객의 실제 문제를 해결하지 못하는데, 그 문제란 이제 이런 포인트 도구를 세 개나 사 놓고도 이미 신뢰하는 사인오프 플로우 안에서 그것들을 어떻게 함께 작동시킬지 전혀 모른다는 것이다.
아무도 대놓고 말하고 싶어 하지 않는 강화학습 배치(placement) 이야기
검증 너머 칩 설계에는 나란한 유혹이 하나 있다: 물리적 플로어플래닝 — 큰 블록들을 다이 위 어디에 앉힐지 결정하는 일 — 을 강화학습으로 하는 것이다. 매혹적이지만, 가장 많이 인용되는 그 결과는 대부분의 세일즈가 편의상 건너뛰는 방식으로 논란에 싸여 있다.
2020년 Google의 Nature 논문은 매크로 배치에서 RL이 모의 담금질(simulated annealing)을 능가한다고 주장했고, 실제 실리콘에도 쓰였다 — 여러 세대의 TPU가 이를 탑재해 출하됐다. 그러나 2023년, 방법론적 우려가 제기된 뒤 Nature는 편집자 주를 덧붙였다. 현재 Synopsys에 있는 Igor Markov는 한 줄 한 줄 짚는 비판을 발표했는데, 그 대표 비교는 한번 보면 잊기 어렵다: RL 방식은 32.31시간이 걸렸고, 튜닝된 모의 담금질 기준선은 12.5시간이 걸렸으며, 상용 Cadence 도구는 같은 작업을 0.05시간만에 끝냈다. DeepMind는 'That Chip Has Sailed'라는 제목의 논문으로 반격했다. 몇 년이 지났지만, 어떤 독립적인 외부 재현도 원래 주장을 확증하지 못했고, 비판과 반박 모두 여전히 유효하다.
내가 이 이야기를 꺼내는 것은, 컨설턴트가 진짜 정형 팀에게 RL 배치를 제안하면서 그 논란이 존재하지 않는 척할 때 벌어지는 일 때문이다. 그들은 10분 안에 낌새를 알아차리고, 당신은 그 방을 잃는다. 정직한 입장은 진정한 틈새가 존재한다는 것이다 — 칩렛과 3D-IC 열 인식 플로어플래닝, 아날로그 레이아웃, 오픈 툴링에서의 RISC-V IP 최적화 — 하이브리드 접근이 제값을 하는 곳 말이다. 기존 강자들의 배치 엔진에 대한 정면 공격은 그렇지 못하다. 그 차이를 알고, 그것을 대놓고 말하는 것이 일의 전부다.
우리 도구가 우리를 속인 뒤 무엇이 바뀌었나
그래서 공허한 증명이라는 참사가 우리를 데려간 곳은 이렇다. 우리는 Verilog를 작성하는 더 나은 AI를 만들려는 시도를 멈췄다. 그것은 자금 지원을 받은 주자가 여덟이나 되는 붐비는 경주이기 때문이다. 그리고 그들 중 누구도 팔지 않는 것을 만들기 시작했다: 벤더 중립적 통합 계층으로, 팀이 이미 쓰는 도구를 신뢰할 수 있게 만들어 주는 것이다.
구체적으로 이는 몇 가지 결정을 뜻하며, 각각은 우리가 목격한 실패가 강제한 것이다. 우리는 오픈 웨이트 모델 — Qwen Coder, Llama 등 맞는 것 무엇이든 — 을 고객 자신의 RTL 코퍼스, 그들의 사양, 그들의 과거 버그 이력에 대해 파인튜닝한다. 당신의 하우스 스타일을 본 적 없는 모델은 그에 어긋나는 환각을 일으키기 때문이다. 우리는 그것을 팀이 이미 보유한 어떤 정형 엔진에도 감싼다: JasperGold, VC Formal, Questa Formal, 또는 오픈소스 SymbiYosys. 우리는 그들에게 이미 신뢰하는 표준 도구를 뜯어내라고 결코 요구하지 않는다. 그리고 모델이 제안하는 모든 속성은 공허성 및 커버리지 검사를 통과한다 — 그러기 전에는 누구도 '증명됨'이라는 단어를 읽을 수 없다. 방비 없는 증명은 연극에 불과하다는 것을 우리는 비싼 대가를 치르고 배웠기 때문이다.
사전 검증된 어설션 라이브러리는 모델만큼이나 중요하다. RISC-V 코어의 경우, 정형 하네스에는 AXI4, AHB, TileLink 준수 검사, 파이프라인 해저드 어설션, 로드-스토어 스코어보딩, 디버그 유닛 정확성 속성이 함께 딸려 온다 — 실리콘이 잡기 전에 프로토콜 및 의미적 환각을 잡아내는 것들이다. 이것은 추측이 아니다. 정형 컨설팅 회사 Axiomise는 Ibex에서 65개 이상의 버그를 발견했다. Ibex는 Google OpenTitan 안에 들어 있는 오픈 RISC-V 코어로, 여기에는 오직 정형만이 잡아낼 수 있었던 디버그 유닛의 분기 명령 버그도 포함된다. 정형은 RISC-V에서 작동한다. 희소한 것은 방법이 아니라, 그것을 다룰 줄 아는 팀이다.
여기서 진짜 기회는 결코 더 똑똑한 Verilog 모델이 아니었다. 그것은 팀이 이미 신뢰하는 값비싼 도구를 감싼 정직한 하네스였다.
왜 그냥 클라우드에서 돌리지 않는가?
사람들은 이것을 끊임없이 묻고, 그 답은 모든 클라우드 우선 EDA-AI 스타트업이 내가 신경 쓰는 고객들에게 도착하자마자 죽는 이유와 같다: RTL은 왕관의 보석이며, 건물 밖으로 나가지 않는다.
팹리스 회사의 레지스터 전송 수준(RTL) 코드가 곧 그 회사 자체다. 방위 및 항공우주 고객은 그것을 에어갭 상태로, 때로는 보안 시설 안에 두어야 한다. 상용 팹리스 팀은 최소한 온프레미스, 가상 사설 클라우드를 원한다. 그래서 우리는 모든 것을 고객 자신의 하드웨어에서 돌린다 — 그들의 기존 H100 또는 H200 클러스터에서 vLLM이나 유사한 추론, 그들 자신의 코퍼스에 대한 로컬 검색, 그리고 RTL이 네트워크 경계를 넘는 일은 결코 없다. 기존 강자들의 최신 에이전트 기능은 클라우드 우선이다. 그것은 그들에게는 기능이지만 IP에 민감한 칩 팀에게는 시작조차 불가능한 조건이다. 내가 보는 가장 큰 기회는 알고리즘 문제가 전혀 아니다. 그것은 최고의 알고리즘을 가진 사람들이 풀지 않기로 결정한 배포·통합 문제다.
또 다른 질문은 자동차 팀에서 나오며, 그들에게는 모든 것을 결정짓는 질문이다. ASIL C 또는 D로 칩을 자동차에 실어 보내라 — ISO 26262가 정형 검증을 단지 권고하기를 멈추고 의무화하기 시작하는 안전 무결성 수준이다 — 그러면 도구 자체가 TCL2 또는 TCL3 인증 패키지를 갖추어야 한다. 기존 강자들의 핵심 엔진은 그 제3자 인증을 갖고 있지만, 갓 나온 AI 도구는 그렇지 않다. 나는 정말로 더 나은 도구가 바로 이 이유로 자동차 프로그램에서 벤치 신세가 되는 것을 지켜봤다: 인증 패키지 없음, 사인오프 플로우에 자리 없음, 대화 끝. 그래서 우리는 되려고 하지 않는다 — 그 인증된 도구가. 우리는 팀이 인증된 기존 엔진 곁에서 AI 보조를 인증 사슬을 깨뜨리지 않고 운영하도록 돕는다 — 자동차 분야에서 감사를 견디지 못하는 기술적으로 우월한 도구는 아무 가치가 없기 때문이다.
인증서는 칩이 아니다
나는 아무 의미도 없는 녹색 체크 표시를 믿으며 보낸 그 이틀로 자꾸 돌아가게 된다. 교훈은 'LLM이 Verilog에 서툴다'가 아니었다. 그것들은 분기마다 나아지고 있다. 교훈은, 하드웨어에서는 검증된 것처럼 보이는 것과 실제로 검증된 것 사이의 간극이 여덟 자리 숫자의 마스크 세트와 6개월의 일정 지연으로 측정된다는 것이었다 — 그리고 이 영역으로 몰려드는 도구들은 대부분 '검증된 것처럼 보이는' 부분을 더 빠르게 만드는 데만 경쟁하고 있다.
$10M짜리 마스크 세트에서, 비공허 증명으로 추적할 수 있고, 당신이 통제하는 하드웨어에서 돌아가며, 사양 84페이지를 읽은 누군가가 작성한 어설션에 대해 검증된 그런 '증명됨'이 아니라면 — 그것은 검증이 아니다. 그것은 제작 완성도만 그럴싸한 희망일 뿐이다. 우리가 그 차이를 어떻게 구별하는지 보고 싶다면, 모든 것이 여기에 정리되어 있다: veriprajna.com/solutions/semiconductor-ai-verification.
칩은 보고서가 뭐라고 말하든 신경 쓰지 않는다. 칩은 오직 실리콘이 실제로 하도록 만들어진 것만 한다. 검증이란 그 두 가지를 같게 만드는 규율이다 — 그리고 AI가 밀리초 만에 둘이 같다고 말하는 그 순간이야말로, 당신이 사양서를 집어 들어야 할 바로 그때다.
