用大模型+搜索算法自动生成硬件断言，提升验证效率
SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine
- 大模型分三阶段处理规范，自动分析信号与波形
- 基于蒙特卡洛树自我精炼算法生成可靠断言
- 适合芯片验证工程师快速构建自动化测试用例
近期大型语言模型（LLM）在推理领域的进展，为更复杂、自动化的硬件断言生成带来了新可能。本文提出SANGAM框架，利用LLM引导的蒙特卡洛树自我精炼（MCTSr）算法，从工业级规格中自动生成SystemVerilog断言（SVAs）。该框架采用三阶段流程：第一阶段通过信号映射器、规范分析器和波形分析器三个LLM智能体进行多模态规范处理；第二阶段使用MCTSr算法对每个信号进行自动推理；第三阶段将生成的推理轨迹整合，形成每个信号的SVA断言。实验表明，SANGAM能生成稳健的断言集，在评估中优于现有方法。
原文摘要 · Abstract (English)
Recent advancements in the field of reasoning using Large Language Models (LLMs) have created new possibilities for more complex and automatic Hardware Assertion Generation techniques. This paper introduces SANGAM, a SystemVerilog Assertion Generation framework using LLM-guided Monte Carlo Tree Search for the automatic generation of SVAs from industry-level specifications. The proposed framework utilizes a three-stage approach: Stage 1 consists of multi-modal Specification Processing using Signal Mapper, SPEC Analyzer, and Waveform Analyzer LLM Agents. Stage 2 consists of using the Monte Carlo Tree Self-Refine (MCTSr) algorithm for automatic reasoning about SVAs for each signal, and finally, Stage 3 combines the MCTSr-generated reasoning traces to generate SVA assertions for each signal. The results demonstrated that our framework, SANGAM, can generate a robust set of SVAs, performing better in the evaluation process in comparison to the recent methods.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。