SAT mini example question.

[Kmanfi]

Steps to reproduce the issue

design -reset; 
read_verilog test_sat.v
hierarchy -top sat_test

proc; flatten 

rename sat_test gold
write_ilang gold.il

###
design -reset; 
read_verilog test_sat.v
hierarchy -top sat_test

proc; flatten; memory; opt

hierarchy -top sat_test
rename sat_test gate
write_ilang gate.il

###
design -reset
read_ilang gold.il
read_ilang gate.il

equiv_make gold gate equiv
hierarchy -top equiv
clean -purge; 
equiv_simple -seq 1
#equiv_induct
#equiv_simple
#equiv_status -assert
###

module sat_test (A, Y, clk, rst);
  input [1:0] A;
  input clk;
  input rst;
  output [1:0] Y;

  reg [1:0] i_d;

  always @(posedge clk) begin
    if ( rst ) begin
      i_d <= 2'b0;
    end
    else begin
      i_d <= A;
    end
  end

assign Y = i_d;
endmodule

Expected behavior

Proof for two designs are functionally equal.

Actual behavior

Question is how to check two sequential designs are functionally equal.
Due to above script I could only find mismatches between gold and gate designs.

[povik]

With the fixes from #3971, the example you have will get proven once you extend -seq from 1 to 2. You need to consider two time steps to see the circuits equivalent.