第4章 设计读入与网表整合：核心概念、原理机制、实战要点

本章聚焦 JasperGold 形式化验证作业流中的第一道关键工序：设计读入与网表整合。只有正确完成该阶段，后续的断言证明、覆盖率分析和反例调试才有可靠基础。

4.1 问题背景：为什么读入阶段如此关键？

形式化验证工具不会直接对源代码做“解释执行”，而是将设计编译为内部验证模型。JasperGold 的设计读入与网表整合环节决定了：
  • 完备性：设计是否被完整建模，缺失部分将成为黑盒。
  • 性能：整合后的网表规模直接影响证明引擎的复杂度。
  • 可调试性：读入阶段的错误处理方式决定你能否快速定位问题。

实际项目中，RTL设计、综合网表、SDC约束和SVA断言往往混合存在。JasperGold 需要同时处理这些不同类型的信息，构建统一的验证模型。

4.2 核心概念

  • 设计读入（Design Read）：将 HDL 文件解析为 JasperGold 内部数据结构的过程。
  • Elaboration（整合）：展开顶层模块的所有例化层级、参数传递、generate 语句，生成扁平化逻辑模型。
  • 网表整合（Netlist Integration）：将门级网表、RTL 模块和约束统一映射到验证模型。
  • 黑盒（Black Box）：未建模的子模块，其输入被当作自由变量，输出为未知。
  • 标准单元库模型：门级网表中的库单元（如 DFF、AND2、MUX2）需要库模型才能完成逻辑映射。

下图给出了设计读入与网表整合的完整路径：

RTL / 网表输入 .v / .sv / .vg 约束文件输入 SDC / SVA JasperGold 读入 解析 + 编译 网表整合 Elaboration 验证模型就绪 可执行形式化验证

4.3 原理机制：从 HDL 源代码到验证模型

JasperGold 将设计源码转换为可求解的模型，需要经历三步流水线：

  1. 词法与语法解析：读取 .v / .sv / .vg 文件，生成抽象语法树（AST）。
  2. 中间表示生成：将 AST 转化为 JasperGold 的中间表示 IR。
  3. Elaboration：解析例化关系、参数传递与 generate，将层级设计展开为扁平化网表。

门级网表整合的特殊性在于：综合网表通常只包含门级互连和库单元实例。JasperGold 必须将每个标准单元（如 SDFF_X1）映射到内部逻辑元操作（寄存器、与门、选择器等）。若找不到库模型，则默认将其视为黑盒并产生警告。

4.4 实战流程：读入与整合五步走

  1. 准备文件清单：编写 filelist，包含所有 RTL、网表、SVA、SDC。
  2. 编写读入脚本：使用 read_file 命令按类型分组建入。
  3. 启动编译：运行 JasperGold，执行脚本，观察日志输出。
  4. 执行 Elaborate：使用 -top 指定顶层模块，完成整合。
  5. 检查报告：确认没有 unknown module 和未连接端口。

典型读入脚本示例：

set PROJ aes_formal

read_file -format sverilog {
  rtl/aes_top.sv
  rtl/aes_sbox.sv
  rtl/aes_keyexp.sv
}

read_file -format sva {
  cons/aes_properties.sva
}

read_file -format sdc {
  cons/aes_constraints.sdc
}

elaborate -top aes_top

report_design -detail

# 保存整合后的模型，便于后续调试
write_design -to out/aes_elab

4.5 案例说明：综合网表缺失标准单元库怎么办？

场景：读入综合网表 aes_netlist.vg 后，elaborate 报告大量 unknown module: SDFF_X1 错误。

根因：综合网表中的标准单元库未被读入，JasperGold 无法识别 SDFF_X1 的行为。

解决方案：

  1. 读入库模型：将标准单元库的 RTL 模型或 liberty 文件加入文件清单。
  2. 声明为黑盒：将 SDFF_X1 设置为黑盒，只关注可见逻辑。
  3. 自定义行为模型：为 SDFF_X1 编写功能等价的 RTL 模型，精度更高。

4.6 表格总结：输入类型与处理方式

输入类型文件扩展名关键命令处理要点
RTL 设计.v / .svread_file -format sverilog保证 module 例化完整
综合网表.vg / .vread_file -format verilog需要标准单元库模型
SVA 断言.svaread_file -format sva与设计版本对齐
SDC 约束.sdcread_file -format sdc时钟、复位等约束

4.7 误区提醒

误区1：读入 RTL 后不看 elaborate 日志，直接开始写 prove 脚本。这会导致黑盒、断线未被发现，最终证明目标无效。
误区2：把门级网表当作普通 RTL 读入。门级网表必须配套标准单元库模型，否则所有门单元变为黑盒。
误区3：忽略 SVA 与设计版本的对应关系。断言与 RTL 来自不同版本时，读入阶段可能不报错，但语义已错位。
提示：读入整合完成后，使用 write_design 保存当前阶段模型。后续调试可以快速重新加载，避免重复 elaborate。

4.8 实践清单

  1. 建立完整的文件清单 filelist，确保 RTL / 门级网表 / SVA / SDC 无缺漏。
  2. 在脚本中显式设置顶层模块：elaborate -top <top>。
  3. 读入后检查日志中的 warning、error、unknown 关键字。
  4. 使用 report_design 查看顶层、模块层次、信号计数和黑盒数量。
  5. 对于缺失的标准单元库，优先补全库模型而非直接黑盒。
  6. 保存 elaborate 后的 journal / 日志，作为回归基线。
← 上一章 📖 返回目录 下一章 →