FSM pass equivalence bug

[joonho3020]

Version

Yosys 0.46+11 (git sha1 0200a76, clang++ 14.0.0-1ubuntu1.1 -fPIC -O3)

On which OS did this happen?

Linux

Reproduction Steps

• We have a given verilog file PointerChasing.sv

// Generated by CIRCT firtool-1.62.0
// VCS coverage exclude_file
module mem_8x4(
  input  [2:0] R0_addr,
  input        R0_en,
  input        R0_clk,
  output [3:0] R0_data,
  input  [2:0] W0_addr,
  input        W0_en,
  input        W0_clk,
  input  [3:0] W0_data
);

  reg [3:0] Memory[0:7];
  reg       _R0_en_d0;
  reg [2:0] _R0_addr_d0;
  always @(posedge R0_clk) begin
    _R0_en_d0 <= R0_en;
    _R0_addr_d0 <= R0_addr;
  end // always @(posedge)
  always @(posedge W0_clk) begin
    if (W0_en & 1'h1)
      Memory[W0_addr] <= W0_data;
  end // always @(posedge)
  assign R0_data = _R0_en_d0 ? Memory[_R0_addr_d0] : 4'bx;
endmodule

module SRAM(
  input        clock,
  input        io_wr_en,
  input  [2:0] io_wr_addr,
  input  [3:0] io_wr_data,
  input  [2:0] io_rd_addr,
  output [3:0] io_rd_data
);

  mem_8x4 mem_ext (
    .R0_addr (io_rd_addr),
    .R0_en   (1'h1),
    .R0_clk  (clock),
    .R0_data (io_rd_data),
    .W0_addr (io_wr_addr),
    .W0_en   (io_wr_en),
    .W0_clk  (clock),
    .W0_data (io_wr_data)
  );
endmodule

module Chaser(
  input        clock,
  input        reset,
  input        io_start,
  output       io_done,
  output [1:0] io_sram_rd_addr,
  input  [3:0] io_sram_rd_data,
  output [3:0] io_final_addr
);

  reg  [1:0] state;
  reg  [3:0] currentAddr;
  reg  [2:0] step;
  wire       _GEN = state == 2'h0;
  wire       _GEN_0 = state == 2'h1;
  wire       _GEN_1 = _GEN_0 & ~(step[2]);
  always @(posedge clock) begin
    if (reset) begin
      state <= 2'h0;
      step <= 3'h0;
    end
    else if (_GEN) begin
      if (io_start) begin
        state <= 2'h1;
        step <= 3'h0;
      end
    end
    else begin
      if (_GEN_0 & step[2])
        state <= 2'h2;
      if (_GEN_1)
        step <= step + 3'h1;
    end
    if (_GEN) begin
      if (io_start)
        currentAddr <= 4'h0;
    end
    else if (_GEN_1)
      currentAddr <= io_sram_rd_data;
  end // always @(posedge)
  assign io_done = state == 2'h2;
  assign io_sram_rd_addr = _GEN | ~_GEN_1 ? 2'h0 : currentAddr[1:0];
  assign io_final_addr = currentAddr;
endmodule

module PointerChasing(
  input        clock,
  input        reset,
  input        io_start,
  output       io_done,
  output [3:0] io_final_addr
);

  reg        initDone;
  wire [1:0] _chaser_io_sram_rd_addr;
  wire [3:0] _sram_io_rd_data;
  reg  [3:0] initCntr;
  wire [3:0] _initCntr_T = initCntr + 4'h1;
  always @(posedge clock) begin
    if (reset) begin
      initDone <= 1'h0;
      initCntr <= 4'h0;
    end
    else begin
      initDone <= ~initDone & initCntr == 4'h7 | initDone;
      if (initDone) begin
      end
      else
        initCntr <= _initCntr_T;
    end
  end // always @(posedge)
  SRAM sram (
    .clock      (clock),
    .io_wr_en   (~initDone),
    .io_wr_addr (initCntr[2:0]),
    .io_wr_data (_initCntr_T),
    .io_rd_addr ({1'h0, _chaser_io_sram_rd_addr}),
    .io_rd_data (_sram_io_rd_data)
  );
  Chaser chaser (
    .clock           (clock),
    .reset           (reset),
    .io_start        (io_start & initDone),
    .io_done         (io_done),
    .io_sram_rd_addr (_chaser_io_sram_rd_addr),
    .io_sram_rd_data (_sram_io_rd_data),
    .io_final_addr   (io_final_addr)
  );
endmodule

• Use yosys to generate a blif file for the above Verilog file. Here we won't use the fsm pass:

read_verilog PointerChasing.sv
hierarchy -check -top PointerChasing
proc; memory; techmap;
async2sync;
dffunmap;
flatten -wb
abc -fast -lut 3
opt -nodffe -nosdff;
write_verilog PointerChasingNoFSM.sv

• Similarly, generate a blif file, but with the fsm pass:

read_verilog PointerChasing.sv
hierarchy -check -top PointerChasing
proc; memory; fsm; techmap;
async2sync;
dffunmap;
flatten -wb
abc -fast -lut 3
opt -nodffe -nosdff;
write_verilog PointerChasingFSM.sv

• Modify the top level module names so that they are different:

sed -i 's/PointerChasing/PointerChasingFSM/g' PointerChasingFSM.sv
sed -i 's/PointerChasing/PointerChasingNoFSM/g' PointerChasingNoFSM.sv

• Run equivalence checking using the following yosys script:

read_verilog PointerChasingFSM.sv
proc
memory

read_verilog PointerChasingNoFSM.sv
proc
memory

equiv_make PointerChasingFSM PointerChasingNoFSM equiv
equiv_simple
equiv_status

Expected Behavior

The equivalence checking should be able to prove that these two circuits are equal.

Actual Behavior

It shows me that it cannot prove equivalence for many of its internal nodes:

Specifically, the combinational logic driving the chaser.state[0] LUT is incorrect when the fsm pass is included.
In the attached parsed.pdf the chaser.state[0] Latch should be initialized to 0 when reset is 1. However, it is getting initialized to 1. Furthermore, the LUT table of $abc$836$flatten... should contain a entry [0, 0, 1] so that chaser.state[0] can be updated when the $abc$836$new_n116 LUT has a value of 1 (the table is order is [reset, chaser.state[0], $abc$836$new...]).

parsed.pdf

[akashlevy]

fsm_recode is a sub-step of fsm which optimizes the internal encoding. If you want logic equivalence for those internal nodes, you might want to try fsm -norecode?

[joonho3020]

I think the problem that I'm having is more severe because the optimized circuit has a completely different functionality compared to the original one (when running simulations, they exhibit different behaviors). I'll still try fsm -norecode :)

[povik]

With FSM state recoding I don't think equiv_make/equiv_simple will be able to prove the circuits equivalent. Also note equiv_simple is severely limited in its power, EQY is the more appropriate tool for general equivalence checking.

the optimized circuit has a completely different functionality compared to the original one (when running simulations, they exhibit different behaviors)

That on the other hand is a serious bug, if you can give more details please adapt the report or open a new ticket.