形式验证和符号推理

符号推理，简单调研一下

符号 vs 模拟

形式验证和 UVM 验证方法本质出发点是不同的，一个基于符号逻辑推理，另一个基于模拟器。

比如有组合电路 A 和组合电路 B，要验证他们逻辑功能一致，即真值表一致。

• 基于模拟器：生成所有输入的可能组合，输入仿真器，对比输出结果
• 基于符号：根据描述得到二者的布尔表达式，证明二者等价

模拟器方法可以把待测元件当作黑盒，只需要关注输入和输出，UVM 本质也是用高级方法写 testbench；而形式验证需要把电路当作白盒对待。有点类似人工智能连接主义路线和符号主义路线区别。

如果考虑时序电路，引入状态输入空间用计算遍历不可行，就要人为约束空间了。在 UVM 中是设置测试边界，而形式验证则是 Inductive 描述良构公式（well-formed formula）。

形式验证方法

SystemVerilog 中的 SVA（System Verilog Assertions） 包含大量形式验证的语法，工具链则是 Formality 最为出名，用于描述符号的格式是 CNF（Conjunctive Normal Form），日后可深入研究。

形式验证主要工具有 Binary Decision Diagrams^[1]、 SAT （Satisfiability）Solver^[2] 等。

---

1. 计算所 23 年自动设计 CPU 的方法就使用的 BDD https://arxiv.org/abs/2306.12456 ↩︎

2. https://medium.com/leep3/從-sat-solver-玩-leetcode-37809cb61df ↩︎