Functional verification has become the most time-consuming phase in IC development, and Assertion-Based Verification (ABV) is key to reducing debugging time. However, existing LLM-based assertion generation methods typically pursue indiscriminate verification, aiming for maximal coverage without considering signal criticality, whereas industrial practice demands maximizing coverage with minimal verification cost. Consequently, identifying signals that have the greatest impact on design functionality and error propagation-enabling a shift from indiscriminate to targeted verification-remains a key challenge. To address this, we propose AgileAssert, a key signal-driven assertion generation framework that constructs RTL semantic graphs and identifies the top-K critical signals via a hybrid scoring and selection mechanism, followed by structure-aware RTL slicing to provide the LLM with precise targets and contextual information, thereby guiding LLMs to generate tightly constrained targeted assertions for efficient verification. Evaluated on block- and CPU-level designs, with an average 66.68% reduction in assertions, our approach outperforms three existing SOTA methods, and significantly improving coverage metrics while reducing input token consumption by 64%. In mutation testing, when our approach surpasses existing methods in error detection rate, the average number of assertions used decreases by 72.74%.
翻译:功能验证已成为集成电路开发中最耗时的阶段,而基于断言的验证(ABV)是缩短调试时间的关键。然而,现有基于大语言模型(LLM)的断言生成方法通常追求无差别验证,旨在最大化覆盖率而不考虑信号关键性,而工程实践则要求以最小的验证成本实现最大的覆盖率。因此,识别对设计功能和错误传播影响最大的信号,实现从无差别验证到目标驱动验证的转变,仍然是一项关键挑战。针对这一问题,我们提出AgileAssert——一种关键信号驱动的断言生成框架。该框架通过构建RTL语义图并采用混合评分与选择机制识别前K个关键信号,随后进行结构感知的RTL切片,为LLM提供精准的目标与上下文信息,引导LLM生成紧密约束的目标驱动型断言,实现高效验证。在模块级和CPU级设计上的评估显示,我们的方法在断言数量平均减少66.68%的同时,在覆盖率指标上显著优于三种现有最先进方法,且输入令牌消耗降低64%。在变异测试中,当我们的方法在错误检测率上超越现有方法时,所使用的断言数量平均减少了72.74%。