Functional verification remains a dominant cost in modern IC development, and SystemVerilog Assertions (SVAs) are critical for simulation-based monitoring and formal property checking. However, writing SVAs by hand is time-consuming and error-prone. Directly prompting general-purpose large language models (LLMs) is also unreliable: the generated properties are often syntactically invalid or semantically incorrect, and the problem is exacerbated by scarce, high-quality domain training data. We present SVA Generator, a data-centric framework that translates natural-language SVA Descriptions (SVADs) into executable SVAs. It uses AST-grounded constraint injection and an automated supervision pipeline that enforces structural consistency and reduces hallucinations via de-duplication and constraint checks. To enable rigorous evaluation, we introduce a benchmark suite stratified by AST depth and use formal property equivalence checking to quantify semantic correctness separately from syntax validity, by checking mutual implication between the generated and reference properties under the same clocking and environment assumptions. Across all difficulty tiers, SVA Generator achieves comparable Syntax Pass Rate (SPR) to strong general LLM baselines, while delivering substantially higher Semantic Equivalence Rate (SER) on deeper tiers: +24.5 pp on D2, +26.0 pp on D3, and +17.5 pp on D4 relative to the best-performing general LLM, corresponding to a +22.7 pp SER improvement on average over D2--D4. These results highlight that high-fidelity data construction and depth-stratified benchmarking are key to reliable, semantics-preserving SVA generation.
翻译:功能验证仍是现代集成电路开发中的主要成本,而SystemVerilog断言(SVA)对于基于仿真的监测和形式化属性检查至关重要。然而,手动编写SVA耗时且易出错。直接提示通用大语言模型(LLM)也并不可靠:生成的属性常存在语法无效或语义错误问题,且高质量领域训练数据的稀缺加剧了这一挑战。我们提出SVA Generator,一种以数据为中心的框架,可将自然语言SVA描述(SVAD)转化为可执行的SVA。它采用基于抽象语法树的约束注入和自动化监督流水线,通过去重与约束检查强制结构一致性并减少幻觉。为支持严格评估,我们引入按AST深度分层的基准测试套件,并利用形式化属性等价性检查,在相同时钟与环境假设下,通过验证生成属性与参考属性间的互蕴含关系,将语义正确性与语法有效性分离评估。在所有难度层级上,SVA Generator的语法通过率(SPR)与强通用LLM基线相当,同时在深层级上实现显著更高的语义等价率(SER):相比最优通用LLM,D2、D3、D4层级分别提升24.5、26.0、17.5个百分点,对应D2-D4层级平均SER提升22.7个百分点。这些结果表明,高保真数据构建与深度分层基准测试是实现可靠、语义保持的SVA生成的关键。