Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

당신이 디지털 레고 브릭으로 거대하고 정교한 성을 쌓고 있다고 상상해 보세요. 이것이 바로 엔지니어들이 컴퓨터 칩을 설계할 때 하는 일입니다. 그들은 트랜지스터가 어떻게 행동해야 하는지 알려주는 RTL(Register Transfer Level)이라는 코드를 작성합니다. 하지만 여기에는 함정이 있습니다. 만약 단 하나의 브릭이라도 잘못된 위치에 놓인다면, 전원이 켜졌을 때 성 전체가 무너질 수 있습니다. 이러한 실수를 찾아내는 것은 이 작업에서 가장 어려운 부분이며, 종종 전체 시간의 절반 이상을 차지하기도 합니다. 전통적으로 엔지니어들은 자신의 작업을 확인하기 위해 두 가지 주요 방법을 사용해 왔습니다. 첫 번째는 "시운전"과 같은 것으로, 칩이 고장 나는지 확인하기 위해 몇 가지 특정 시나리오를 실행해 보는 것입니다. 두 번째는 "형식 검증(formal verification)"으로, 이는 단순히 테스트한 상황뿐만 아니라 모든 가능한 조건에서도 성이 견딜 수 있음을 보장하는 초수학적인 증명과 같습니다. 하지만 이 초수학적 증명 방법은 대기업만이 감당할 수 있는 비싸고 폐쇄적인 소프트웨어를 필요로 하는 경우가 많습니다.

여기에 새로운 강자가 등장했습니다. 바로 대규모 언어 모델(LLM)입니다. 당신도 이들이 이야기를 쓰거나 코드를 작성할 수 있는 AI 챗봇이라는 것을 알고 있을 것입니다. 최근 사람들은 이렇게 묻기 시작했습니다. "AI가 우리의 고장 난 디지털 성을 고치는 설계자가 될 수 있을까?" 핵심 질문은, AI가 단순히 실수만 찾아내는 것이 아니라, 값비싼 소프트웨어 라이선스를 구매하지 않고도 수학적으로 완벽함이 증명된 방식으로 오류를 수정할 수 있는지 여부입니다. 이 논문은 AI의 창의성과 형식 수학의 엄격하고 변함없는 논리 사이의 가교를 놓으려 노력하며, 오직 무료 오픈 소스 도구만을 사용하여 이 질문에 깊이 파고듭니다.

AI 탐정과 오픈 소스 도구 상자

이 연구에서 연구원 하 퉁 트란(Ha Trung Tran)은 고장 난 칩 설계를 수리하는 역할을 할 영리한 AI 에이전트 팀을 구축했습니다. 이것은 마치 고도의 기술을 갖춘 탐정 부대가 루프(loop) 안에서 작동하는 것과 같습니다. 한 명의 AI가 모든 것을 한꺼번에 처리하는 대신, 팀은 역할이 나뉩러져 있습니다. 한 에이전트는 설계도를 읽고, 다른 에이전트는 칩이 해야 할 규칙을 작성하며, 세 번째 에이전트는 작업 내용을 점검하고, 네 번째 에이전트는 실제로 코드를 수정합니다.

여기서 비결은 실수에 대한 확인 방식에 있습니다. 대부분의 AI 수리 도구는 칩이 제대로 작동하는지 보기 위해 몇 번의 시운전(시뮬레이션)을 실행할 뿐입니다. 하지만 이 팀은 "형식 백엔드(formal backend)"를 사용합니다. 이는 Yosys, SymbiYosys, Z3라고 불리는 도구들로 구성된 무료 오픈 소스 수학 엔진입니다. 이 엔진은 단순히 추측하는 것이 아니라, 칩이 올바르다는 것을 수학적으로 증명하려고 시도합니다. 만약 칩이 실패한다면, 엔진은 단순히 "고장 났다"라고 말하는 데 그치지 않습니다. 대신 엔진은 AI에게 성이 정확히 어떻게 무너졌는지 보여주는 영상 재생과 같은 구체적인 "반례(counterexample)"를 전달합니다. 그러면 AI는 이 영상을 보고 무엇이 잘못되었는지 파악한 뒤 코드를 수정하려고 시도합니다. 그들은 수학이 칩이 완벽하다고 증명하거나 시도 횟수를 다 쓸 때까지 이 과정—확인, 충돌 발견, 수정, 재확인—을 반복합니다.

좋은 소식: 효과가 있다 (때로는)

연구진은 이 시스템을 단순한 계산기 부품(ALU)부터 더 복잡한 트래픽 컨트롤러 및 메모리 유닛에 이르기까지 여섯 가지 유형의 디지털 설계에 대해 테스트했습니다. 결과는 승리와 명확한 한계가 섞여 있었습니다.

이 극의 주인공은 칩의 계산기 뇌와 같은 역할을 하는 ALU(산술 논리 장치)였습니다. 연구진은 의도적으로 "AND" 연산을 "OR" 연산으로 바꿔서 이를 고장 냈습니다. AI 팀은 즉시 오류를 찾아냈습니다. 단 두 번의 확인과 수정 과정을 거쳐 코드를 수리했습니다. 더 중요한 것은, 오픈 소스 수학 엔진이 칩이 처리할 수 있는 모든 숫자에 대해 수정이 올바르다는 것을 100% 확실하게 증명했다는 점입니다. 이 과정은 다섯 번의 테스트 실행 모두에서 발생했으며, 평균 단 16.5초가 걸렸습니다. 이는 아이디어가 작동함을 입증했습니다. 즉, 오픈 소스 수학 도구의 안내를 받는 AI가 수학적 보증과 함께 실제 버그를 찾아내고 수정할 수 있다는 것입니다.

나쁜 소식: AI가 막힌 곳

하지만 이야기가 모두 승리로 끝난 것은 아닙니다. 연구진이 동일한 과정을 다른 다섯 가지 설계에 적용했을 때, AI 팀은 벽에 부딪혔습니다. 그들은 이 설계들을 안정적으로 고칠 수 없었습니다. 논문은 AI를 함정에 빠뜨리는 네 가지 뚜렷한 "실패 모드(failure modes)"를 식별하며 왜 실패했는지를 면밀히 분석합니다.

1. "너무 깊은" 함정 (유계 커버리티 공백, Bounded-Cover Vacuity): 한 사례(카운터)에서, 수학 엔진은 수정이 실제로 올바름에도 불구하고 "FAIL"이라고 판정했습니다. 왜일까요? 설계가 특정 상태에 도달하기 위해 256 사이클을 실행해야 했지만, 도구가 256 사이클까지만 살펴보았기 때문입니다. 이는 마치 자동차가 나라를 가로질러 운전할 수 있는지 증명하기 위해 딱 1마일만 운전해 보는 것과 같았습니다. 도구가 목적지를 보지 못했기 때문에 포기한 것입니다. 논문은 이것이 AI의 한계가 아니라 도구의 한계라고 지적합니다.
2. "혼란스러운 지침" 함정 (명세 모호성, Specification Ambiguity): 또 다른 설계(아비터)의 경우, AI는 작성된 규칙을 따르려고 노력했지만, 그 규칙은 (시계 없이 작동하는 신호등처럼) 불가능한 것을 요구했습니다. AI는 충실하게 불가능한 지침을 따랐고, 결국 막다른 길에 다다랐습니다.
3. "시간 여행" 함정 (시계열 논리 버그, Temporal Logic Bugs): 두 가지 사례(UART 송신기 및 FIFO 메모리)에서 버그는 여러 타임 스텝에 걸쳐 발생하는 이벤트와 관련되었습니다. AI는 단일 단계의 논리(계산기처럼)를 고치는 데는 뛰어났지만, 시간에 따라 발생하는 이벤트의 순서를 추론하는 데는 어려움을 겪었습니다.
4. "너무 많은 규칙" 함정 (다중 속성 압박, Multi-Property Pressure): 마지막 사례(AXI Lite 슬레이브)에서는 칩이 동시에 준수해야 하는 규칙이 너무 많아서, 하나의 규칙을 고치면 다른 규칙이 깨지는 현상이 발생했습니다. AI는 모든 조건을 만족하는 해결책을 찾지 못한 채 루프에 빠졌습니다.

도구 상자의 숨겨진 결함

도구 자체에 대해서도 놀라운 발견이 있었습니다. 연구진은 코드를 처리하는 데 도움을 주는 Yosys 도구에 숨겨진 특이점이 있다는 것을 발견했습니다. 만약 "bind"라는 특정 방식을 사용하여 설계에 안전 점검(assertion)을 부착하려고 하면, 도구가 이를 조용히 무시합니다. 이는 방에 보안 카메라를 설치했지만 카메라 전원이 뽑혀 있는 것과 같습니다. 시스템은 카메라를 전혀 보지 못하기 때문에 모든 것이 정상이라고 생각하게 됩니다. 연구진은 수학 엔진이 실제로 점검 내용을 볼 수 있도록 체크를 코드에 직접 "주입(inject)"하는 방식으로 방법을 변경해야 했습니다. 이는 이 무료 도구들을 사용하는 다른 모든 이들에게 도움이 될 팁입니다.

결론

이 논문은 "타당성 조사(feasibility study)"입니다. 이는 "우리가 시도해 보았고, 정확히 어디에서 작동하며 어디에서 깨지는지"를 밝히는 학술적인 표현입니다. 주요 결과는 AI를 사용하여 수학적 정당성이 증명된 칩 설계를 수정하는 것이 가능하다는 것이지만, 이는 오픈 소스 도구를 사용하고 문제가 너무 복잡하지 않을 때에만 해당됩니다.

저자는 한계를 솔직하게 인정합니다. 이 시스템은 단순하고 즉각적인 논리 오류(계산기 등)를 고치는 데는 훌륭하지만, 현재로서는 복잡한 타이밍 문제, 깊은 메모리 상태, 또는 충돌하는 규칙이 있는 설계에는 어려움을 겪습니다. 저자는 칩 수리의 문제를 해결했다고 주장하는 대신, AI가 작동하는 "안전 구역"과 길을 잃는 "위험 구역"을 보여주는 명확한 지도를 그렸습니다. 오직 무료 도구만을 사용함으로써, 저자는 이 분야의 연구 진입 장벽을 낮추고, 신뢰할 수 있는 하드웨어 설계를 구축하는 미래를 만드는 데 수백만 달러의 예산이 필요하지 않다는 것을 증명하고자 합니다.