sva-gen

name	sva-gen
description	在 YAML 中编写 SVA 属性检测代码

SVA 断言编写工作流

本技能指导如何将 .formal_records.yaml 中的 sva_body 占位符翻译为完整的 SVA 断言代码。

SVA 编码规范参见 Guide_Doc/sva_property.md

核心原则：数据驱动同步

VeriAgent 采用 YAML 作为唯一事实来源 (SSOT) 的架构。

1. 禁止直接修改 .sv 文件：checker.sv 和 wrapper.sv 是由系统自动根据 YAML 渲染生成的只读产物。
2. 通过 YAML 更新代码：使用 update_sva_body.py 技能脚本更新检测点的实现代码。
3. 自动同步：当你调用 Check 工具进行验证时，系统会自动将 YAML 中的代码渲染到 .sv 文件中。

步骤

1. 逐条编写 SVA 代码

针对 .formal_records.yaml 中标记为 [LLM-TODO] 的 sva_body 字段，构思对应的 SVA 逻辑。

确认注释中标注的 Style（Assume / Seq / Comb / Cover），选择 Guide_Doc/sva_property.md 中对应的代码模板。

2. 使用工具更新 YAML

使用 update_sva_body.py 脚本将代码注入 YAML。

python3 .veriagent/skills/formal/sva-gen/scripts/update_sva_body.py <CK-ID> "<SVA_CODE_BODY>"

示例：

python3 .veriagent/skills/formal/sva-gen/scripts/update_sva_body.py CK-ADD-CORE-EQUATION "##0 ({cout, sum} == a + b + cin);"

3. 调用 Check 工具验证

调用 veriagent.checkers.formal.PropertyStructureChecker。

• 如果仍有检测点未填写，Checker 会报错并列出缺失项。
• 如果全部填写完成，Checker 会自动渲染生成最新的 checker.sv 和 wrapper.sv 供后续 EDA 工具使用。

核心规则

1. 禁止直接编辑 SV 文件：任何手动对 checker.sv 的修改都会在下次 Check 时被覆盖。
2. 属性语法：只需提供 property 内部的逻辑体，外层的 property ... endproperty 和标签实例化由模板自动生成。
3. 禁止 |-> 1'b1 占位符断言：必须实现真实逻辑。
4. 每个逻辑行以 ; 结尾。
5. 白盒信号处理：如果需要引用内部信号，请先确保这些信号在 RTL 解析阶段已正确识别或在模板中已处理。