AI 中文总结
CHARGE是利用CWE层次结构和LLM生成硬件安全SVA的自动化框架，在Hack@DAC系列SoC设计中检测到多个已知与新错误，生成的SVA具备较高有效性。
AI 中文摘要
本文提出了CHARGE，一种利用常见弱点枚举（CWE）和大型语言模型（LLM）为未经验证的寄存器传输级（RTL）模块生成安全属性的自动化框架。其核心特点是利用CWE条目的层次结构进行推理，以提高识别未经验证RTL模块中安全关键资产的准确性。因此，该方法能够从已识别的资产和CWE语义中推断预期的安全行为并生成属性，无需依赖可信的设计规范，减少了人工工程工作量。我们在Hack@DAC18、19和21开源片上系统（SoC）设计上使用OpenAI的GPT-4.1对该框架进行评估。CHARGE在这些设计中检测到42个已知错误中的27个。对于Hack@DAC21 OpenPiton SoC，生成的SystemVerilog断言（SVA）中有89%可在Cadence JasperGold形式化属性验证（FPV）中运行，且92.2%为非空泛化。我们将其与这些设计的开源手动编写属性集进行比较，发现CHARGE为3个手动编写属性不正确的错误正确生成了属性。此外，CHARGE生成的属性还识别出Hack@DAC21 OpenPiton SoC中之前未发现的一个新错误。
英文摘要
This paper presents CHARGE, an automated framework for generating security properties for unverified RTL modules using CWEs and large language models (LLMs). The hallmark is a reasoning process that leverages the hierarchical nature of CWE entries to improve accuracy when identifying security-critical assets in unverified RTL modules. As a result, the approach can infer expected security behaviors and generate properties from identified assets and CWE semantics, avoiding the need for trusted design specifications and reducing manual engineering effort. We evaluate the framework on the Hack@DAC18, 19, and 21 open source SoC designs using OpenAI's GPT-4.1. CHARGE detects 27 of 42 known bugs in these designs. For Hack@DAC21 OpenPiton SoC, 89% of the generated SVAs run in Cadence JasperGold FPV, and 92.2% are non-vacuous. We compare to an open-source, manually written set of properties for these designs and find that CHARGE correctly writes properties for three bugs in which the manually written properties were incorrect. In addition, CHARGE-generated properties identify a new bug in the Hack@DAC21 OpenPiton SoC that was not previously identified.
CommentsThis paper is an extended version of the paper accepted to the IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2026)
