跳转至

文章背景与核心概要

硬件功能验证在暴露设计缺陷以及确保寄存器传输级（RTL）设计信心方面，高度依赖高质量的断言（Assertions）。然而，传统断言挖掘方法往往表现不佳，因为随机或有限的执行追踪无法触及深层、难以访问的行为，且一站式生成技术缺乏识别验证盲区的反馈机制。

为了克服这些局限性，作者引入了 NeuroAssertion，这是一个新颖的覆盖率驱动断言生成框架，它将形式化追踪生成、语法制导综合（SyGuS）以及智能体驱动的细化过程有机结合。实验评估表明，与传统的断言挖掘技术相比，NeuroAssertion 能够产生大约 2 倍的断言，并实现大约 2 倍高的变异覆盖率。

Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

Authors: Zhiyuan Yan, Ziyue Zheng, Hongce Zhang
Primary Subject: Hardware Architecture (cs.AR)
Secondary Subject: Artificial Intelligence (cs.AI)
Identifiers: arXiv: 2608.18482 | DOI: 10.48550/arXiv.2608.18482
Status: Accepted at MLCAD 2026
Submitted: August 19, 2026

Authors: Zhiyuan Yan, Ziyue Zheng, Hongce Zhang
Primary Subject: Hardware Architecture (cs.AR)
Secondary Subject: Artificial Intelligence (cs.AI)
Identifiers: arXiv: 2608.18482 | DOI: 10.48550/arXiv.2608.18482
Status: Accepted at MLCAD 2026
Submitted: August 19, 2026

Summary

硬件功能验证 heavily 依赖于高质量的断言来暴露设计缺陷并确保对寄存器传输级（RTL）设计的信心。然而，传统断言挖掘方法往往效果欠佳，因为随机或有限的执行追踪无法触及深层、难以访问的行为，并且一站式生成技术缺乏用于识别验证盲区的反馈机制。

Hardware functional verification heavily relies on high-quality assertions to expose design bugs and ensure confidence in Register Transfer Level (RTL) designs. However, traditional assertion mining methods often fall short because random or limited execution traces fail to reach deep, hard-to-access behaviors, and one-stop generation techniques lack feedback mechanisms to identify verification gaps.

为了克服这些局限性，作者推出了 NeuroAssertion，这是一个新颖的覆盖率驱动断言生成框架，它统一了形式化追踪生成、语法制导综合（SyGuS）以及智能体驱动的细化过程。

To overcome these limitations, the authors introduce NeuroAssertion, a novel coverage-driven assertion generation framework that unifies formal trace generation, syntax-guided synthesis (SyGuS), and an agent-driven refinement process.

Key Methodology

  1. 形式化可达性目标： 将难以触及的控制流条件转换为形式化目标。
  2. 行为多样的追踪生成： 利用模型检测生成多样化的执行追踪。
  3. 语法制导综合（SyGuS）： 从生成的追踪中挖掘初始断言。
  4. 受智能体启发的神经符号细化： 采用双大模型（Dual-LLM）反馈循环：
  5. LLM 1 为未覆盖区域提出候选断言。
  6. LLM 2（如果候选断言未通过形式化检查）生成修复语法，在神经符号修复过程中引导受约束的符号综合。

Key Methodology

  1. Formal Reachability Objectives: Converts hard-to-reach control-flow conditions into formal objectives.
  2. Behaviorally Diverse Trace Generation: Leverages model checking to generate diverse execution traces.
  3. Syntax-Guided Synthesis (SyGuS): Mines initial assertions from the generated traces.
  4. Agent-Inspired Neuro-Symbolic Refinement: Employs a dual-LLM feedback loop:
  5. LLM 1 proposes candidate assertions for uncovered regions.
  6. LLM 2 (if a candidate fails formal checking) generates a repair grammar to steer constrained symbolic synthesis in a neuro-symbolic repair procedure.

Results

实验评估表明，与传统的断言挖掘技术相比，NeuroAssertion 能够产生大约 2 倍的断言，并实现大约 2 倍高的变异覆盖率。

Results

Experimental evaluations demonstrate that NeuroAssertion yields approximately 2× more assertions and achieves roughly 2× higher mutation coverage compared to traditional assertion mining techniques.

附加资源与链接

许可证信息：知识共享署名 4.0 国际许可协议

License Information: Creative Commons Attribution 4.0 International