符号推理，简单调研一下

符号 vs 模拟

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

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

⚠️以下内容有猜测部分，待调研工具具体实现补充

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

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

如果考虑时序电路，引入状态输入空间用计算遍历不可行，就要人为约束状态空间了。

形式验证方法

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

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