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