Formality 原语概念详解

原语 (Primitive) 的概念

原语 (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 实现设计的结构