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生成的关键。

0
下载
关闭预览

相关内容

一个具体事物,总是有许许多多的性质与关系,我们把一个事物的性质与关系,都叫作事物的属性。 事物与属性是不可分的,事物都是有属性的事物,属性也都是事物的属性。 一个事物与另一个事物的相同或相异,也就是一个事物的属性与另一事物的属性的相同或相异。 由于事物属性的相同或相异,客观世界中就形成了许多不同的事物类。具有相同属性的事物就形成一类,具有不同属性的事物就分别地形成不同的类。
揭示生成式人工智能 / 大型语言模型(LLMs)的军事潜力
专知会员服务
32+阅读 · 2024年9月26日
大型语言模型(LLMs),附Slides与视频
专知会员服务
71+阅读 · 2024年6月30日
《大型语言模型代码生成》综述
专知会员服务
70+阅读 · 2024年6月4日
大模型如何迭代?北大等《大型语言模型自我进化》综述
自然语言处理中的语言模型预训练方法
PaperWeekly
14+阅读 · 2018年10月21日
NLP通用模型诞生?一个模型搞定十大自然语言常见任务
人工智能头条
10+阅读 · 2018年6月29日
NLP中自动生产文摘(auto text summarization)
机器学习研究会
14+阅读 · 2017年10月10日
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
VIP会员
最新内容
综述 | 3D场景图:开放挑战与未来方向
专知会员服务
4+阅读 · 6月22日
21世纪的无人机战争
专知会员服务
4+阅读 · 6月22日
《量子技术的军事任务技术适配与利用》
专知会员服务
5+阅读 · 6月22日
美国从乌克兰无人机战争中学习经验
专知会员服务
7+阅读 · 6月21日
ICML 2026 | 面向视觉语言模型的语义鲁棒性认证
专知会员服务
5+阅读 · 6月21日
相关基金
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员