대규모 언어 모델은 칩 설계 검증에서 가장 번거로운 작업 중 하나인 자연어로 작성된 사양을 RTL 구현의 정확성을 판단하는 데 사용할 수 있는 공식 속성 집합으로 변환하는 단계에 가까워지고 있다. Semiconductor Engineering에서 Brian Bailey가 진행한 인터뷰에 따르면, 현재 도구는 유용한 초기 초안을 만들 수 있지만, 집중적인 엔지니어링 검토 없이 승인할 수 있는 완전한 집합을 생성하는 단계에는 아직 이르지 못했다.
이 발전이 중요한 이유는 속성 작성이 수년 동안 공식 검증의 병목이었기 때문이다. 검증 환경에 삽입될 때 assertions라고 불리는 SystemVerilog 속성은 신호 간의 논리적·시간적 관계를 설명한다. 예를 들어 리셋 동작, 핸드셰이크, one-hot 조건, 기본 안전성 검사를 표현할 수 있다. 이러한 속성이 완전하고 정확하다면 설계 구축 방식과 무관하게 RTL 구현의 동작을 사양과 비교하는 데 사용할 수 있다.
오늘날 도구가 할 수 있는 일
대규모 언어 모델 기반 도구는 사양 문서, 프로토콜 표준 또는 RTL 내부의 주석을 읽은 뒤 SVA 속성 초안을 제안할 수 있다. Axiomise의 CEO인 Ashish Darbari는 사양이 크게 변하지 않는 안정적인 표준에 기반할 때 이러한 활용이 더 실용적이라고 말한다. 이 경우 도구는 검증 전체를 담당하기보다는 초기 코드 작성의 반복적인 부분을 줄여 준다.
일부 접근 방식은 knowledge graph, 즉 엔터티와 그 관계를 저장하는 지식 그래프를 구축해 모델의 정확도를 높이려고 한다. 노드에는 신호, 모듈, 요구사항 또는 포트가 포함될 수 있으며, 엣지는 ‘구동한다’, ‘리셋한다’, ‘응답한다’와 같은 관계를 설명한다. 요청과 관련 있어 보이는 텍스트 조각을 검색하는 대신 시스템이 구체적인 사실과 연결을 참조할 수 있으므로, 신호 이름을 지어내거나 설계 구성요소 간 관계를 잘못 이해할 가능성을 줄일 수 있다. 소식통은 이와 관련해 Cohen과 Chibani의 RAG-SVA in the Landscape of LLM-Based Assertion Generation이라는 연구를 언급한다.
문제는 AI보다 먼저 시작된다
도구는 처음부터 작성되거나 확정되지 않은 내용을 추출할 수 없다. Synopsys의 애플리케이션 엔지니어링 디렉터인 Ravindra Aneja는 지난 30년 동안 이상적인 사양이 현실적으로 존재하지 않았다고 말한다. 문서화가 완성되기 전에 개발이 시작되는 경우가 많고, 일부 프로젝트, 특히 파생 설계나 작업 중 요구사항이 변경되는 경우에는 완전한 사양이 없을 수도 있다.
이 문제는 단순히 표현 방식에 관한 것이 아니라 변경 관리에 관한 것이기도 하다. 마케팅팀이 새로운 기능을 추가하거나 기존 요구사항을 수정할 수 있으며, 설계팀과 검증팀은 그 변경의 영향을 판단해야 한다. Siemens EDA의 수석 부사장 겸 총괄 관리자인 Abhi Kolpekwa는 사양을 속성으로 변환하려면 매번 새로운 텍스트를 생성하는 에이전트가 아니라 변경 이력과 맥락을 추적하는 ‘맥락 지능’이 필요하다고 본다.
잘못된 신뢰의 위험
현재 접근 방식의 가장 큰 한계는 속성이 문법적으로는 올바를 수 있다는 점이다. 즉 속성이 번역되고 검증 도구가 이를 증명하는 데 성공하더라도, 실제로 의도된 동작을 테스트하지 않을 수 있다. Darbari는 취약하거나 vacuous한 속성이 많은 동작을 허용하거나, 잘못된 신호를 사용하거나, 누락되었거나 지나치게 제한적인 선행 조건을 포함하기 때문에 쉽게 성공할 수 있다고 경고한다. 따라서 ‘녹색 증명’이 설계에 오류가 없다는 뜻은 아니다. 증명은 증명된 속성보다 강할 수 없다.
소식통은 또한 모델이 아키텍처 의도와 규칙의 존재 이유를 이해하는 것보다 구조적·문법적 커버리지에서 더 나은 성능을 보이는 경향이 있다고 설명한다. 따라서 모델이 사양을 부정확하게 해석하면 형식적이고 엄격해 보이는 결과물이 만들어질 수 있지만, 그 안에 요구사항의 공백이 숨겨질 수 있다. 이러한 공백이 FMEDA, 안전성 파일 또는 ISO 26262와 ISO 21434에 연계된 인증 근거와 같은 작업으로 이어지면 그 영향은 원래의 검증 프로젝트를 넘어설 수 있다.
설계와 검증을 분리하는 문제도 부각된다. Normal Computing의 제품 설계 리더인 Kaye Mao는 에이전트가 프로젝트 자료에 접근할 수 있는 범위를 제한해야 한다고 지적한다. 에이전트가 설계 자체를 사용해 테스트 케이스를 생성하도록 허용하면 검증 프로세스의 독립성이 훼손될 수 있기 때문이다.
실무적으로 무엇이 달라지는가?
Darbari에 따르면 AI는 첫 번째 초안 작성 시간을 며칠에서 몇 분으로 줄일 수 있지만, 이후 작업량을 두 배로 늘릴 수도 있다. 생성된 각 속성은 사양과 대조하고, 커버리지를 분석하며, vacuity를 검사하고, 설계 신호와의 관계를 검토해야 하며, 실패한 경우에는 파형 분석이 필요할 수 있다. 속성 수가 10배로 늘어나고 각각에 요구되는 검토 수준이 그대로라면, 검토 부담이 빠른 생성으로 얻는 이익을 넘어설 수 있다.
certi.news의 관점에서 진정한 변화는 검증 엔지니어를 대체하는 것이 아니라 속성 작성에서 속성 평가와 출처 추적 쪽으로 중심을 옮기는 것이다. Darbari는 생성된 속성을 승인된 결과물이 아니라 초안으로 취급하고, 이를 regression suite에 추가하기 전에 검토 관문을 마련할 것을 권고한다. 또한 각 속성의 출처, 즉 해당 속성을 생성한 사양의 문단, 요구사항 또는 RTL 요소를 기록해야 엔지니어가 일치 여부를 확인할 수 있다.
Normal Computing의 검증 솔루션 엔지니어인 Yaron Ilani는 이러한 접근 방식이 formal verification을 사용하려는 검증 엔지니어들의 진입 장벽을 낮출 수 있다고 말한다. 그러나 이것이 투자수익률에 관한 질문을 해결하지는 않는다. Kaye Mao는 에이전트의 출력물을 검증하는 데 걸리는 시간도 비용에 포함해야 한다고 본다. 한편 Normal Computing의 솔루션 수석 엔지니어인 Arvind Srinivasan은 확장성이 계산 능력에만 달린 것이 아니라 데이터의 완전성과 인간 검토 비용에도 달려 있다고 지적한다.
결론적으로 대규모 언어 모델은 속성 작성의 자동화되고 반복적인 부분을 가속할 수 있게 되었지만, 사양의 완전성과 설계 의도 이해라는 두 문제를 아직 해결하지 못했다. 이러한 도구의 가치는 모델이 생성할 수 있는 속성의 수가 아니라, 설계를 이해하는 엔지니어의 존재와 커버리지를 독립적으로 측정하고 공허하거나 부적절한 속성을 찾아내는 메커니즘에 달려 있을 것이다.