AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs
Hongqin Lyu, Yonghao Wang, Jiaxin Zhou, Zhiteng Chao, Tiancheng Wang and Huawei Li
基于断言的验证(ABV)是检查逻辑设计是否符合其架构规范的关键方法。 基于设计规范的现有断言生成方法通常只产生顶级断言,忽略了微架构级别模块中实现细节的验证需求,其中设计错误更频繁地发生。 为了解决这一限制,我们介绍了AssertMiner,一个模块级断言生成框架,利用从抽象语法树(AST)生成的静态信息来帮助LLM进行挖掘断言。 具体来说,它执行基于AST的结构提取来派生模块调用图,I/O表和数据流图,引导LLM生成模块级规范和矿模块级断言。 我们的评估表明,AssertMiner在为模块生成高质量断言方面优于AssertLLM和Spec2Assertion等现有方法。 当与这些方法集成时,AssertMiner可以提高结构覆盖范围并显着提高错误检测能力,从而实现更全面、更高效的验证过程。
Assertion-based verification (ABV) is a key approach to checking whether a logic design complies with its architectural specifications. Existing assertion generation methods based on design specifications typically produce only top-level assertions, overlooking verification needs on the implementation details in the modules at the micro-architectural level, where design errors occur more frequently. To address this limitation, we present AssertMiner, a module-level assertion generation framework...