AI가 짜낸 $10 million짜리 버그 — 그리고 내가 그것을 없애려 회사를 세운 이유
나는 Veriprajna를 시작하기로 결심한 바로 그 순간을 정확히 기억한다.
영감의 번뜩임이 아니었다. 전화 한 통이었다. 상대방이 자기가 해야 할 말을 어떻게 꺼내야 할지 고민하느라 처음 5초 동안 아무도 말을 하지 않는, 그런 전화였다. 내가 존경하던 사람들, 자기 일에 진정으로 뛰어난 사람들로 이루어진 설계 팀이 방금 파운드리로부터 커스텀 RISC-V 가속기의 첫 실리콘을 돌려받은 참이었다. 칩은 죽어 있었다. "우회책이 필요한" 수준의 죽음이 아니었다. "펌웨어로 패치할 수 있는" 수준의 죽음도 아니었다. 완전히 벽돌이 되었다. 열 스로틀링과 고대역폭 메모리 트래픽이 특정하고 드문 방식으로 맞물리는 조건에서, 중재(arbitration) 모듈이 정의되지 않은 상태에 진입했고 전체 시스템이 데드락에 빠졌다.
근본 원인은 레이스 컨디션이었다. RTL에서 블로킹 할당과 논블로킹 할당 사이의 단 하나의 미묘한 불일치 — 시뮬레이션에서는 완벽하게 동작하고, 린트에서는 아무 경고도 내지 않으며, 던지는 모든 회귀 테스트를 통과하지만, 두 번째 기회가 없는 실리콘에서 당신을 배신하는 그런 종류의 것이었다.
그 5nm 칩의 마스크 세트는 대략 $10 million의 비용이 들었다. 사라졌다. 하지만 진짜 피해는 마스크가 아니었다. 진단하고, 고치고, 재검증하고, 재제작하는 데 필요한 6개월이었다. 제품 세대가 약 18개월 지속되는 AI 가속기 시장에서, 6개월의 지연은 제품 전체 수명 총 매출총이익의 50%를 잠식할 수 있다. $100 million의 매출을 목표로 하는 회사에게, 그 레이스 컨디션은 $10 million의 비용이 아니었다. $50 million의 비용이었다.
그리고 나를 밤새 잠 못 이루게 한 부분은 이것이다: 그것을 야기한 코드는 LLM이 생성한 것이었다.
아무도 의문을 제기하지 않는 골드러시
지금 이 순간, 반도체 산업은 골드러시 한복판에 있다. 모두가 — 정말 모두가 — 대규모 언어 모델(LLM)을 전자 설계 자동화(EDA) 워크플로에 끼워 넣기 위해 경쟁하고 있다. 그 제안은 거부할 수 없다: 예전에는 몇 년씩 걸리던 설계 주기를 몇 달로 압축하라. 칩 설계를 대중화하라. 지루한 레지스터 전송 수준 코딩은 AI에게 맡기고 엔지니어는 아키텍처에 집중하게 하라.
그 매력을 나도 안다. 나 자신도 느껴 봤다. LLM이 자연어 프롬프트로부터 구문적으로 올바른 Verilog 모듈을 생성하는 것을 처음 봤을 때, 나는 생각했다: 이것은 모든 것을 바꾼다.
하지만 그때 나는 소프트웨어가 아니라 하드웨어를 작성할 때 "구문적으로 올바른"이 실제로 무엇을 의미하는지 더 자세히 들여다보기 시작했다. 그리고 나는 이 산업이 모래 위의 기초 위에 세워지고 있음을 깨달았다.
지금 시장에 넘쳐나는 도구들을 나는 "래퍼(Wrapper)"라고 부른다. 그것들은 범용 LLM — GPT-4, Claude, Llama — 을 가져다가 Verilog 풍의 시스템 프롬프트를 얹은 채팅 인터페이스로 감싸서 "칩 설계 코파일럿"으로 판매한다. 그중 일부는 진정으로 인상적인 데모다. 코드는 깔끔해 보인다. 컴파일된다. 심지어 시뮬레이션도 된다.
하지만 이 도구들이 근본적으로 무엇인지는 이렇다: 하드웨어 껍데기를 뒤집어쓴 확률론적 토큰 예측기. 그것들은 회로 토폴로지를 이해하지 못한다. 타이밍 클로저를 이해하지 못한다. 메타스터빌리티(준안정성)를 이해하지 못한다. 그것들은 학습 데이터의 통계적 패턴에 기반해 다음에 올 가능성이 높은 토큰을 예측할 뿐이다.
LLM이 소프트웨어에서 환각을 일으키면, 무선으로 패치할 수 있는 런타임 오류를 얻는다. LLM이 하드웨어에서 환각을 일으키면, $10 million짜리 문진(paperweight)을 얻는다.
그 비대칭성이 Veriprajna가 존재하는 이유의 전부다.
왜 AI는 형편없는 하드웨어 코드를 작성하는가?
이것은 내가 가장 자주 받는 질문이며, 대개 LLM이 완벽하게 작동하는 Python을 작성하는 것을 본 소프트웨어 엔지니어들이 Verilog는 왜 다른지 이해하지 못해 묻는다. 그 답은 "하드웨어가 더 어렵다"보다 더 깊이 들어간다. 그것은 LLM이 사고하는 방식과 하드웨어가 작동하는 방식 사이의 근본적인 불일치다.
LLM은 압도적으로 소프트웨어 — Python, Java, C++, JavaScript — 위에서 학습된다. 이것들은 명령형이고 순차적인 언어다. A행이 실행되고, 그다음 B행이 실행된다. 시스템의 상태는 연산의 순서로 정의된다. LLM은 이 패러다임을 너무나 깊이 내면화해서, 그것은 사실상 그들의 모국어다.
Verilog와 VHDL은 선언적이고 동시적이다. 하드웨어 모듈에서는, 모든 always 블록, 모든 assign 문(statement), 모든 모듈 인스턴스화가 동시에 그리고 연속적으로 실행된다. 소스 코드에서 줄의 순서는 실리콘에서의 실행 순서와 아무런 상관이 없는 경우가 많다.
나는 우리의 초기 실험 중 하나에서 이것이 실시간으로 펼쳐지는 것을 지켜봤다. 우리는 세 개의 서로 다른 프런티어 LLM에게 간단한 3단계 파이프라인 레지스터를 구현하도록 요청했다. 세 모델 모두 블로킹 할당(=)을 사용했다 — 논블로킹 할당(<=)이 아니라. 코드는 C 코드처럼 실눈을 뜨고 보면 완벽하게 합리적으로 보였다. 하지만 하드웨어에서는, 클럭 블록 안의 블로킹 할당은 다음을 의미한다: stage2가 stage1의 값으로 즉시 갱신되고, 그다음 stage3는 새롭게 갱신된 값을 받는다. 그 값의 출처는 바로 stage2다 — 사실상 2사이클 파이프라인을 1사이클로 붕괴시켜 버리는 것이다.
내 엔지니어 중 한 명인 Priya는 1분 동안 출력을 응시하더니 말했다, "이건 세미콜론을 엉뚱한 자리에 찍은 C를 쓰고 있는 거예요." 그녀의 말은 정확했다. 그 LLM은 순차적 편향을 갖고 있었다 — 그것은 실제로는 기술(description) 언어인 Verilog를 프로그래밍 언어처럼 다루고 있었다. 그 구분은 구문적으로는 미묘하고 물리적으로는 파국적이다.
그리고 상황은 더 나빠진다. 하드웨어 설계는 엄격한 인터페이스 프로토콜 — AXI, AHB, PCIe, TileLink — 에 의존하며 복잡한 시간적 규칙을 따른다. "Ready는 Valid를 기다려서는 안 된다." "Grant는 5사이클 이내에 어서트되어야 한다." LLM은 이러한 규칙을 90%의 경우 준수하는 코드를 생성할 수 있는데, 이는 틀리는 10%가 바로 칩을 죽이는 코너 케이스라는 것을 깨닫기 전까지는 훌륭하게 들린다. WVALID를 먼저 어서트하고 그다음 AWREADY를 어서트하는, 특정 하위 조항 위반에 해당하는 AXI 마스터는 구문 오류를 던지지 않는다. 그것은 컴파일되고, 시뮬레이션되며, 그런 다음 실리콘에서 규격을 준수하는 메모리 컨트롤러에 연결되면 멈춰 버린다.
학습 데이터 문제가 모든 것을 가중시킨다. 학습에 사용할 수 있는 고품질의 프로덕션급 Verilog의 양은 여러 자릿수만큼 더 적다 — Python이나 JavaScript보다 말이다. GitHub에 있는 오픈소스 Verilog의 상당수는 학생 프로젝트, 방치된 프로토타입, 테이프아웃 리뷰를 결코 통과하지 못할 장난감 수준의 구현이다. 형편없는 데이터로 학습하면 형편없는 출력을 얻는다 — 전문적으로 보이지만 아마추어적 실수의 DNA를 담고 있는 출력을.
모든 칩 설계자를 괴롭히는 법칙
반도체 설계에는 "10의 법칙"이라 불리는 경험칙이 있는데, 이것을 이해하고 나면 내가 왜 버그를 초기에 잡는 데 그토록 집착하는지 이해하게 된다.
결함을 수정하는 비용은 10배씩 설계 수명주기의 각 후속 단계마다 증가한다. RTL 설계 단계에서 잡힌 버그는 수정하는 데 약 $100이 든다 — 누군가 파일을 편집하고 검사를 다시 돌린다. 같은 버그가 블록 검증 단계에서 잡히면 $1,000이 든다. 시스템 검증에서는 $10,000. 만약 그것이 포스트 실리콘 검증까지 빠져나가면 — 실험실에서 실제 칩을 디버깅하는 시점 — 리스핀에 $10 million 이상을 각오해야 한다. 그리고 만약 그것이 현장의 고객에게 도달한다면? 그건 $100 million의 영역이다. 리콜, 소송, 브랜드 파괴. 인텔에게 펜티엄 FDIV 버그에 대해 물어보라.
래퍼 AI 도구들은 거의 전적으로 RTL 설계 단계에서만 작동한다. 그것들은 엔지니어가 코드를 더 빨리 작성하도록 돕는다. 하지만 "컴파일이 되는가" 이상의 검증 능력이 전혀 없기 때문에, 그것들은 블록 검증과 시스템 검증을 유유히 통과했다가 결국 실리콘에서 터지는 버그를 주입한다.
여기 잔인한 아이러니가 있다: 검증의 엄격함을 높이지 않은 채 코드 생성의 속도만 높임으로써, 이 도구들은 고비용 결함이 파이프라인에 주입되는 것을 가속한다. 당신은 그저 빠르게 움직이며 무언가를 부수고 있는 게 아니다. 당신은 빠르게 움직이며 $10 million짜리 마스크 세트에 버그를 구워 넣고 있는 것이다.
업계 데이터가 이를 뒷받침한다. 설계의 32%만이 첫 실리콘 성공을 달성한다. 나머지 68%는 최소 한 번의 리스핀을 필요로 하며, 그 주된 원인은 로직 및 기능적 결함 — LLM이 프로토콜을 환각하거나 동시성을 오해할 때 생성하는 바로 그런 종류의 오류 — 이다.
나는 언젠가 자금 조달 초기에 한 투자자에게 이것을 설명했다. 그는 참을성 있게 듣더니 말했다: "그냥 더 나은 프롬프트로 GPT-4를 쓰면 되지 않나요?"
나는 파이프라인 레지스터 예제를 띄웠다. 나는 그에게 블로킹 할당 버그를 보여줬다. 나는 그것이 린팅을 통과하고, 시뮬레이션을 통과하고, 래퍼 도구들이 제공하는 모든 자동 검사를 통과했음을 보여줬다. 그런 다음 나는 그것이 실리콘에서 무슨 짓을 할지 보여줬다.
그는 더 나은 프롬프트에 대해 다시는 묻지 않았다.
코드를 그저 테스트하는 대신 올바르다고 증명할 수 있다면 어떨까?
바로 여기서 이야기가 전환된다. LLM 환각 문제에 대한 답은 더 나은 프롬프트도, 더 큰 모델도, 더 많은 학습 데이터도 아니기 때문이다. 그것은 검증에 대한 근본적으로 다른 접근법이다.
전통적인 검증은 시뮬레이션에 의존한다 — 테스트벤치를 작성하고, 수백만 사이클을 돌리며, 설계가 예상대로 동작하는지 확인한다. 이것은 자동차의 브레이크를 블록을 천 번 돌면서 테스트하는 것과 같다. 브레이크가 고장 나지 않으면, 안전하다고 가정한다. 하지만 만약 그것이 비가 올 때, 정확히 시속 62마일로 달릴 때, 그리고 라디오가 특정 주파수에 맞춰져 있을 때만 고장 난다면? 시뮬레이션은 명시적으로 테스트하는 시나리오만 검증할 수 있다. 그 밖의 모든 것은 기도일 뿐이다.
형식 검증(Formal Verification)은 설계를 아예 실행하지 않는다. 그것은 전체 설계를 수학적 공식으로 변환하고 만족성 모듈로 이론(SMT) 솔버 — 마이크로소프트의 Z3 같은 도구 — 를 사용해, 어떤 속성이 다음 조건에서 성립함을 남김없이 증명한다: 가능한 모든 입력 조합과 내부 상태. 하나도 빠짐없이 전부. 표본이 아니다. 통계적 근사가 아니다. 수학적 증명이다.
시뮬레이션은 묻는다: "이것이 내가 테스트한 경우들에서 작동하는가?" 형식 검증은 묻는다: "이것이 실패할 수 있는 경우가 하나라도 존재하는가?" 그 차이는 희망과 증명 사이의 차이다.
솔버가 "UNSAT" — 충족 불가능 — 을 반환하면, 그것은 반례가 존재하지 않는다는 것을 의미한다. 그 속성은 수학적으로 보장된다. 솔버가 "SAT"를 반환하면, 그것은 당신의 설계를 깨뜨리는 입력의 구체적인 시퀀스를, 정확한 클럭 사이클 단위까지 건네준다.
형식 검증은 수십 년 동안 존재해 왔다. 그것이 업계를 장악하지 못한 이유는 형식 속성 — SystemVerilog Assertions, 즉 SVA — 을 작성하는 일이 악명 높게 어렵기 때문이다. 그것은 대부분의 설계 팀이 갖고 있지 않은 전문적인 기술을 요구한다. 어서션은 하드웨어에 대한 "계약"이다: "요청이 하이가 되면, 그랜트는 N 사이클 이내에 뒤따라야 한다." "주소 X에서 읽은 데이터는 주소 X에 마지막으로 쓰인 데이터와 일치해야 한다." "파이프라인은 절대 데드락에 빠져서는 안 된다." 이것들을 올바르게 작성하는 일은 하나의 예술이며, 그 일을 감당할 실무자가 충분하지 않다.
바로 여기서 AI가 유용해진다 — 하드웨어 코드를 작성하기 위해서가 아니라, 증명을 작성하기 위해서.
"포멀 샌드위치" — 우리가 실제로 이것을 어떻게 만들었는가
나는 올바른 아키텍처를 두고 몇 달 동안 팀과 논쟁했다. 그 논쟁은 치열했고, 돌이켜보면 명료해지는 계기였다. 한 진영은 LLM을 파인튜닝해서 기본적으로 올바른 Verilog를 생성하게 만들고 싶어 했다. 다른 진영은 — 내가 결국 손을 들어준 쪽은 — 학습을 통한 정확성이란 환상이라고 주장했다. 환각은 학습으로 없앨 수 없다. 오직 잡아낼 수 있을 뿐이다.
우리는 우리가 이렇게 부르는 것에 도달했다: "포멀 샌드위치" — LLM이 창의적 엔진이고 형식 검증 솔버가 굽히지 않는 비평가인 뉴로-심볼릭 아키텍처다. 어느 쪽도 홀로는 작동하지 않는다. 함께라면, 그들은 어느 쪽도 독립적으로는 할 수 없는 일을 해낸다.
실제로 어떻게 작동하는지 설명하겠다. 설계자가 명세를 제공한다 — "APB-투-AXI 브리지를 설계하라" 또는 심지어 타이밍 다이어그램 스크린샷을. 우리의 Spec Analyzer 에이전트가 이것을 기능 요구사항으로 분해한다. 그런 다음 핵심 혁신이 등장한다: LLM은 코드만 생성하는 대신, 두 개의 산출물을 동시에 생성한다.
산출물 A는 RTL 구현 — Verilog 코드 그 자체 — 이다. 산출물 B는 형식 명세 — 동일한 요구사항으로부터 도출된 SVA 속성들의 집합 — 이다. 명세가 "그랜트는 리퀘스트를 뒤따라야 한다"고 말하면, LLM은 상태 기계를, 그리고 그것이 주장하는 대로 상태 기계가 동작함을 증명하는 어서션을 생성한다.
그런 다음 우리는 솔버를 풀어놓는다. 솔버는 산출물 A를 가져다가 산출물 B를 사용해 그것을 깨뜨리려 시도한다. 먼저, 공허성(vacuity) 검사 — 어서션이 자명하게 참이 아닌지 확인한다 (트리거 조건이 결코 발동하지 않는 "게으른" 생성). 그다음 경계 모델 검사(bounded model checking)로, 깊은 상태 공간 — 50, 100 사이클 깊이 — 을 탐색하며 데드락, 레이스 컨디션, 프로토콜 위반을 사냥한다.
솔버가 버그를 찾으면, 그것은 단지 표시만 하지 않는다. 그것은 다음을 만들어낸다: 반례 트레이스(counter-example trace) — 버그가 정확히 어떻게 나타나는지 보여주는 정밀한 파형이다. 그리고 바로 여기서 루프가 닫힌다: 우리는 그 트레이스를 프롬프트로서 LLM에 다시 넣어 준다. "당신의 설계가 실패했습니다. 여기 트레이스가 있습니다: 사이클 1, 리셋 해제. 사이클 2, 리퀘스트가 하이가 됨. 사이클 10, 그랜트는 여전히 로우. 그랜트가 끝내 도착하지 않았습니다. 상태 기계를 고치세요."
LLM은 트레이스를 분석하고, 누락된 상태 전이를 식별하고, 코드를 다시 작성한다. 솔버가 다시 검사한다. 이 루프는 설계가 올바르다고 증명될 때까지 자동으로 반복된다.
나는 이 아키텍처를 훨씬 더 깊이 있게 다루었다 — 우리 연구의 인터랙티브 버전에서 말이다. 하지만 핵심 통찰은 단순하다: 우리는 AI를 사용해 증명을 작성하고, 수학을 사용해 그 AI를 검사한다. 어느 쪽도 상대를 신뢰하지 않는다. 둘 다 서로를 더 낫게 만든다.
나를 신봉자로 만든 버그들
나는 이론을 통해서가 아니라, 다른 어떤 것으로도 찾지 못했을, 우리가 잡아낸 구체적인 버그들을 통해 이 접근법의 진정한 신봉자가 되었다.
오픈소스 RISC-V 커뮤니티는 진정으로 훌륭한 프로세서 코어들을 만들어냈다 — Ibex(구글의 OpenTitan 보안 칩에 사용됨), 취리히 연방공과대학교(ETH Zurich)의 PULP 플랫폼. 이것들은 진짜 엔지니어링 인재가 뒤를 받치고 있는, 철저히 검토된 설계다. 그럼에도 그것들은 여전히 오직 형식 검증만이 찾을 수 있는 버그를 담고 있다.
형식 검증 컨설팅 회사인 Axiomise는 Ibex 코어에서, 분기 명령 실행 중 특정 사이클에 도착하는 디버그 요청이 코어를 데드락에 빠뜨리거나 잘못된 명령을 실행하게 만들 수 있는 버그를 발견했다. 생각해 보라 — 수십 명의 엔지니어가 검토한 보안이 중요한 코어에서, 형식 도구가 시뮬레이션이 완전히 놓친 버그를 찾아낸 것이다.
PULP 플랫폼에서는, AXI 인터커넥트가 특정 "바쁨(busy)" 패턴 하에서 버스 마스터를 무한정 굶길 수 있는 버그가 발견되었는데, 그 패턴은 AWVALID 와 AWREADY 상호작용의 것이었다. 전형적인 라이브니스(liveness) 실패다 — 시스템이 충돌하는 게 아니라, 그저 진전을 멈춘다. 당신은 그 특정 상호작용 패턴에 대한 지정 테스트를 결코 작성하지 않을 것이다. 열거하기에는 가능한 패턴이 너무 많다.
우리가 Veriprajna를 RISC-V 로드-스토어 유닛(Load-Store Unit)에 겨누면, 그것은 인터페이스 준수("valid가 어서트되면, ready가 될 때까지 하이를 유지해야 한다"), 데이터 무결성("주소 X에서 읽은 데이터는 주소 X에 대한 마지막 쓰기와 일치한다"), 그리고 순방향 진행("유닛은 결국 응답을 반환해야 한다")에 대한 어서션을 자동으로 생성한다. 이것들은 코드에 나중에 덧붙인 부가물이 아니다. 그것들은 코드와 나란히, 동일한 명세로부터 생성되며, 단 한 줄의 RTL도 우리 시스템을 떠나기 전에 강제된다.
우리 방법론과 형식 검증 엔진에 대한 완전한 기술적 분석은 다음을 참고하라: 우리의 상세한 연구 논문.
"하지만 형식 검증은 확장되지 않는다"
사람들은 항상 이 지점에서 반박하는데, 나는 그 이유를 이해한다. 형식 검증은 계산적으로 폭발적이라는 평판을 갖고 있다 — 현대 SoC의 상태 공간은 천문학적으로 크고, 순진한 형식 접근법은 장난감 수준의 설계보다 큰 것이라면 무엇에든 질식한다.
우리는 이것에 상당한 노력을 쏟았다. 우리 시스템은 자동화된 추상화 기법을 사용해 대규모에서도 형식 검증을 다룰 수 있게 만든다. 블랙박싱(Black-boxing)은 RAM이나 복잡한 ALU 같은 큰 서브블록을 정의된 인터페이스를 가진 추상적 개체로 취급하면서 글루 로직을 검증할 수 있게 해준다. 컷포인트(Cut-points)는 valid/ready 핸드셰이크 경로를 끊어, 우리가 데이터 처리와 독립적으로 흐름 제어를 검증할 수 있게 한다. 대칭성 감소(Symmetry reduction)는 멀티포트 라우터의 한 채널에 대해 어떤 속성을 증명한 뒤 그것을 모든 N개 채널로 수학적으로 귀납할 수 있게 해준다.
완전히 해결되었는가? 아니다. 아날로그 물리는 형식 방법이 손댈 수 없는 난제를 언제나 제기할 것이다. 하지만 로직 버그 — 레이스 컨디션, 데드락, 프로토콜 위반 — 는 생성된 코드에서 수학적으로 불가능해진다. 그리고 바로 그것들이 리스핀을 유발하는 버그다.
내가 듣는 또 다른 반론은 속도에 관한 것이다. "형식 솔버를 돌리면 설계 과정이 느려지지 않나요?" 그렇다, 그것은 계산 비용을 더한다. 하지만 나는 언제든지 컴퓨팅 시간을 일정의 확실성과 맞바꾸겠다. 형식 솔버를 한 시간 더 돌리는 것은 6개월의 리스핀보다 무한히 싸다.
"AI가 설계한 칩"에 관한 불편한 진실
업계에서 힘을 얻고 있는 이야기가 하나 있다 — AI가 곧 칩을 처음부터 끝까지 설계할 것이며, 우리가 컴퓨터 지원 설계(Computer-Aided Design)에서 컴퓨터 자동화 설계(Computer-Automated Design)로 옮겨가고 있다는 것이다. 나는 그 이야기가 방향은 맞지만 위험할 정도로 불완전하다고 믿는다.
우리는 자율적 AI 에이전트들이 협업하는 에이전트형(agentic) 워크플로를 향해 구축하고 있다 — 상위 수준 분할을 위한 아키텍트 에이전트, 구현을 위한 RTL 코더, 테스트벤치와 어서션을 작성하는 검증 엔지니어, 그리고 전력·성능·면적 제약에 맞춰 흐름을 조율하는 매니저. 우리는 검색 증강 생성(RAG)을 코드뿐 아니라 지식을 위해서도 사용한다 — 구체적인 프로토콜 규칙, 공정 설계 키트(PDK) 제약, 그리고 내부 코딩 표준을 끌어와, LLM이 환각 없이 규격을 준수하는 코드를 생성하게 한다.
하지만 이 중 어느 것도 작동하지 않는다 — 단 하나도 — 형식 검증이라는 근간 없이는 말이다. AI가 더 자율적일수록, 모든 출력이 하류로 넘어가기 전에 수학적으로 검증되는 것이 더욱 결정적으로 중요해진다. 코드를 더 빨리 생성하는 AI 에이전트는 그 코드가 올바를 때만 가치가 있다. 코드를 더 빨리 생성하면서 동시에 그것이 올바름을 증명하는 AI 에이전트라면? 그것이 미래다.
반도체 산업의 문제는 AI가 하드웨어 코드를 작성하는 데 너무 느리다는 것이 아니다. 문제는 AI가 미묘하게 잘못된 하드웨어 코드를 작성하는 데 너무 빠르다는 것이다.
우리는 코파일럿이 아니다. 우리는 챗봇이 아니다. 우리는 마침 생성형 AI를 프런트엔드로 사용하는 형식 검증 파운드리다. 이 구분이 중요한 이유는 그것이 당신이 무엇을 최적화하고 있는지를 결정하기 때문이다. 코파일럿은 속도를 최적화한다. 우리는 정확성을 최적화한다. 단 하나의 빠져나간 버그가 마스크에 $10 million, 그리고 잃어버린 매출에 $50 million의 비용을 치르게 하는 세상에서, 나는 내가 어느 최적화를 택할지 안다.
선택은 이미 내려졌다
반도체 산업은 더 이상 "생성하고 기도하라(generate and pray)" 접근법을 감당할 수 없다. 10의 법칙은 제안이 아니다 — 그것은 검증되지 않은 실리콘을 출하하는 누구든 벌하려고 공모하는 물리학과 경제학이다. 5nm 이하에서, $20 million에 육박하는 마스크 세트와 함께, 오차의 여유는 0으로 붕괴했다.
매주 나는 LLM이 자신의 생산성을 위해 할 수 있는 일에 흥분하면서도 LLM이 자신의 테이프아웃 일정에 저지를지도 모를 일에 두려워하는 설계 팀들과 이야기한다. 그들이 두 가지를 동시에 느끼는 것은 옳다. 그 기술은 진정으로 변혁적이다. 그것은 또한 안전망 없이는 진정으로 위험하다.
Veriprajna가 바로 그 안전망이다. 우리는 당신에게 수학의 확실성과 함께 AI의 속도를 준다. "아마도 올바른"이 아니다. "회귀 테스트를 통과한"이 아니다. 올바르다고 증명된, 가능한 모든 입력에 걸쳐, 가능한 모든 상태에 걸쳐, 시뮬레이션이 결코 테스트할 생각조차 못할 가능한 모든 코너 케이스에 걸쳐서 말이다.
오늘날 모든 칩 설계자가 마주한 선택은 AI를 쓸지 말지가 아니다. 그 배는 이미 떠났다. 선택은 자신의 작업을 스스로 증명할 수 있는 AI를 쓸 것인가, 아니면 그저 최선을 바라기만 하는 AI를 쓸 것인가이다.
나는 내가 $10 million을 어느 쪽에 걸지 안다.
