原语（primitive）的概念
原语一般指的是语言内置的基本构件，它们代表了基本的逻辑门和构件，通常用于建模电路的基本功能。例如 Verilog 中的门级建模会使用 and、or 等关键词表示单元门。Formality 也存在原语的概念，这一般出现在对门级网表进行建模时。
假设以例 1 所示的 RTL 代码作为参考设计（可以看出添加了// synopsys sync_set_reset 综合指令让 Design Compiler 将其实现为带同步复位端的 D 触发器），例 2 所示的综合后网表作为实现设计，其中 data_out_reg 原语是一个带同步复位端的 D 触发器 (FDS2)。
// 例 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
// 例 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 中完成了参考设计、实现设计和库文件的读取后，参考设计的结构如图 1 所示（注意勾选 Primitive），原理图如图 2 所示。
图 1 参考设计的结构
图 2 参考设计的原理图
可以看出，就像 Design Compiler 读取 RTL 代码后会将其转化为 GTECH 网表那样（其实 GTECH 也可以被认为是一种 primitive），Formality 读取 RTL 代码后直接将其用内部原语实现了，其中 data_out_reg 原语是一个有同步使能 SL，同步数据输入 SD 和时钟 CLK 的 D 触发器。
实现设计的结构如图 3 所示（注意勾选 Primitive 和 Tech Cells），原理图如图 4 所示。
图 3 实现设计的结构
图 4 实现设计的原理图
从图 3 所示的结构，我们可以看到来自标准单元库的 data_out_reg 单元（注意，这与参考设计中的 data_out_reg 原语不是一个概念）和 U4 单元，但是可以看出它们是可以再分的，U4 单元由 cell0 原语组成，data_out_reg 单元则由包括 dff.00 在内的四个原语组成。
data_out_reg 单元的内部结构如图 5 所示。
图 5 data_out_reg 单元的内部结构
dff.00 原语就像参考设计中的 data_out_reg 原语那样是一个有同步使能 SL，同步数据输入 SD 和时钟 CLK 的 D 触发器，但此时搭配 cell2 原语实现了一个带同步复位端的 D 触发器。
总结一下就是，为了让等价性检查更标准化，Formality 将直接用内部原语实现 RTL 代码，而用功能等效的方式用内部原语实现门级网表中的各个标准单元，并最终对内部原语进行比较。在工艺库列表中，可以查看各个标准单元是如何映射到内部原语的，如图 6 所示。
图 6 查看标准单元库中每个标准单元原语映射方式
这也解释了为什么在进行比较点验证时，会将参考设计中的 data_out_reg 原语和实现设计中的 data_out_reg/dff.00 原语进行比较了，此时它们才应该是比较是否等价的对象，如图 7 所示。
图 7 比较点的验证