Formality 中的原语（Primitive）概念
原语（primitive）通常指语言内置的基本构件，代表底层的逻辑门或单元。在 Verilog 门级建模中，我们常用 and、or 等关键词表示基本单元。Formality 同样存在原语的概念，这在对门级网表进行建模和比较时尤为关键。
我们以一个带同步复位端的 D 触发器为例。参考设计（RTL）如下：
// 例 1 module ref( input clk, input reset, input data_in, output reg data_out ); // synopsys sync_set_reset "reset" always @(posedge clk) begin if (reset) begin data_out <= 1'b0; end else begin data_out <= data_in; end end endmodule
综合后的实现设计网表（Gate-level Netlist）则不同，这里 data_out_reg 原语对应的是库中的 FDS2 单元：
// 例 2 ///////////////////////////////////////////////////////////// // Created by: Synopsys DC Expert(TM) in wire load mode // Version : O-2018.06-SP1 // Date : Fri Jun 27 15:52:09 2025 ///////////////////////////////////////////////////////////// module ref ( clk, reset, data_in, data_out ); input clk, reset, data_in; output data_out; wire n1; FDS2 data_out_reg ( .CR(data_in), .D(n1), .CP(clk), .Q(data_out) ); IV U4 ( .A(reset), .Z(n1) ); endmodule
在 Formality 中加载参考设计、实现设计和库文件后，观察参考设计的结构（勾选 Primitive），你会发现它已经被内部原语实现了。就像 Design Compiler 将 RTL 转为 GTECH 网表一样，Formality 读取 RTL 后直接映射为内部原语。此时 data_out_reg 原语表现为一个有同步使能 SL、同步数据输入 SD 和时钟 CLK 的 D 触发器。
再看实现设计的结构（勾选 Primitive 和 Tech Cells），来自标准单元库的 data_out_reg 单元和 U4 单元虽然看起来是黑盒，但它们是可以再分的。U4 由 cell0 原语组成，而 data_out_reg 单元则由包括 *dff.00* 在内的四个原语组成。
查看 data_out_reg 的内部结构，*dff.00* 原语配合 cell2 原语最终实现了一个带同步复位端的 D 触发器。这与参考设计中直接使用的 data_out_reg 原语在功能上是等效的。
总结一下，为了让等价性检查更标准化，Formality 会将 RTL 代码直接用内部原语实现，同时将门级网表中的各个标准单元通过功能等效的方式映射到内部原语，最终对内部原语进行比较。你可以在工艺库列表中查看每个标准单元是如何映射到内部原语的。
这也解释了为什么在进行比较点验证时，会将参考设计中的 data_out_reg 原语和实现设计中的 data_out_reg/*dff.00* 原语进行比较。只有当它们都映射到相同的内部原语层级时，才是真正需要验证是否等价的对象。
