Fminit Pass

fminit 是 Yosys 中用于为形式化验证进行初始化的 pass，其详细命令参见

我们以如下命令为例：

fminit -seq rst 0,1,2 -posedge clk

该命令表示对于信号 rst：

在时刻 0，其值应为 0
在时刻 1，其值应为 1
在时刻 2，其值应为 2
在时刻 3+，其值保持为 2

这是通过移位寄存器、锁存器和 assume 实现的，如下图所示：

#0:
           1
           ↓
        +-----+     1      +-----+     0      +-----+     0
  0 --> | FF0 | ---------> | FF1 | ---------> | FF2 | --------->
        +-----+            +-----+            +-----+
           |                 ↓ 0                 ↓ 0
           | 1                                  LATCH
           ↓                                     ↓ 0
        $ASSUME(rst == 0)  $assume(rst == 1)  $assume(rst == 2)

#1:
        +-----+     0      +-----+     1      +-----+     0
  0 --> | FF0 | ---------> | FF1 | ---------> | FF2 | --------->
        +-----+            +-----+            +-----+
           ↓ 0                ↓ 1                ↓ 0
                                               LATCH
                                                 ↓ 0
        $assume(rst == 0)  $ASSUME(rst == 1)  $assume(rst == 2)

#2:
        +-----+     0      +-----+     0      +-----+     1
  0 --> | FF0 | ---------> | FF1 | ---------> | FF2 | --------->
        +-----+            +-----+            +-----+
           ↓ 0                ↓ 0                ↓ 1
                                                LATCH
                                                 ↓ 1
        $assume(rst == 0)  $assume(rst == 1)  $ASSUME(rst == 2)

#2:
        +-----+     0      +-----+     0      +-----+     0
  0 --> | FF0 | ---------> | FF1 | ---------> | FF2 | --------->
        +-----+            +-----+            +-----+
           ↓ 0                ↓ 0                ↓ 0
                                                LATCH
                                                 ↓ 1
        $assume(rst == 0)  $assume(rst == 1)  $ASSUME(rst == 2)

比如有如下的 RTL，最终的效果类似：

module top (input clk, input [1:0] d, output reg [1:0] q);
  always @(posedge clk)
    q <= q + 1;

  // fminit 增加的部分
  reg [1:0] _ctrl_dly_0  = 0;
  reg [1:0] _ctrl_dly_1  = 0;
  reg [1:0] _ctrl_dly_2  = 0;
  wire      _once_active = 0;

  assign _once_active = _once_active | _ctrl_dly_2;

  initial
    _ctrl_dly_0 = 1;

  always @(posedge clk) begin
    _ctrl_dly_1 <= _ctrl_dly_0;
    _ctrl_dly_2 <= _once_active ? 1 : _ctrl_dly_1;
  end

  always @(*) begin
    if (_ctrl_dly_0) assume(rst == 0);
    if (_ctrl_dly_1) assume(rst == 1);
    if (_ctrl_dly_2) assume(rst == 2);
  end
endmodule

或者更抽象的：

module top (input clk, input [1:0] d, output reg [1:0] q);
  always @(posedge clk)
    q <= q + 1;

  // fminit 增加的部分
  reg [1:0] state = 0;
  always @(posedge clk)
    case (state)
      0: begin
        assume(rst == 0);
        state <= 1;
      end;
      1: begin
        assume(rst == 1);
        state <= 2;
      end
      2:
        assume(rst == 2);
endmodule