Formality 原语（Primitive）概念详解

Formality 中的原语（Primitive）概念

在数字 IC 设计流程中，原语（Primitive）通常指语言内置的基本构件。它们代表了底层的逻辑门和基础单元，常用于建模电路的基本功能。比如在 Verilog 的门级建模中，and、or 等关键词就是典型的原语。

Formality 同样存在原语的概念，这主要体现在对门级网表进行建模和等价性检查时。本文将结合实例，详细解释这一机制。

RTL 与网表的对应关系

假设我们有一段参考设计的 RTL 代码（例 1），其中添加了 // synopsys sync_set_reset "reset" 综合指令，告诉 Design Compiler 将其实现为带同步复位端的 D 触发器。对应的综合后网表（例 2）则展示了具体的底层实现，其中 data_out_reg 原语是一个带同步复位端的 D 触发器（FDS2）。

例 1：参考设计 RTL 代码

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：综合后网表

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

Formalty 的原语映射机制

在 Formalty 中完成参考设计、实现设计和库文件的读取后，我们可以观察其内部结构。如果在结构视图中勾选 Primitive，原理图会显示如图 1 和图 2 所示的形态。

文章配图 图 1 参考设计的结构

文章配图 图 2 参考设计的原理图

你会发现，就像 Design Compiler 读取 RTL 后会转化为 GTECH 网表一样（GTECH 本身也可视为一种 Primitive），Formality 读取 RTL 代码后，会直接将其用内部原语实现。此时 data_out_reg 原语表现为一个有同步使能 SL、同步数据输入 SD 和时钟 CLK 的 D 触发器。

对于实现设计，如果我们同时勾选 Primitive 和 Tech Cells，结构视图和原理图会有所不同（如图 3 和图 4）。

文章配图