The $check cell could not support TRG_WIDTH > 1 lead to old design verification failed with async2sync command.

[Readon]

Version

Yosys 0.41+111

On which OS did this happen?

Linux, Windows

Reproduction Steps

As it is states in YosysHQ/sby#279 the design

module unamed(
  input  wire          a_valid,
  output reg           a_ready,
  input  wire [0:0]    a_payload,
  output wire          r_valid,
  input  wire          r_ready,
  output wire [0:0]    r_payload,
  input  wire          clk,
  input  wire          reset
);

  wire                a_m2sPipe_valid;
  wire                a_m2sPipe_ready;
  wire       [0:0]    a_m2sPipe_payload;
  reg                 a_rValid;
  reg        [0:0]    a_rData;
  wire                when_Stream_l372;
  wire                a_fire;
  wire                r_fire;
  reg                 formal_with_past;
  reg                 _zz_1;
  reg                 _zz_2;

  initial begin
    formal_with_past = 1'b0;
  end

  always @(*) begin
    a_ready = a_m2sPipe_ready;
    if(when_Stream_l372) begin
      a_ready = 1'b1;
    end
  end

  assign when_Stream_l372 = (! a_m2sPipe_valid);
  assign a_m2sPipe_valid = a_rValid;
  assign a_m2sPipe_payload = a_rData;
  assign r_valid = a_m2sPipe_valid;
  assign a_m2sPipe_ready = r_ready;
  assign r_payload = a_m2sPipe_payload;
  assign a_fire = (a_valid && a_ready);
  assign r_fire = (r_valid && r_ready);
  always @(posedge clk or posedge reset) begin
    if(reset) begin
      a_rValid <= 1'b0;
    end else begin
      if(a_ready) begin
        a_rValid <= a_valid;
      end
      cover(((a_fire && r_fire) && _zz_2)); // FormalTest.scala:L119
    end
  end

  always @(posedge clk) begin
    if(a_ready) begin
      a_rData <= a_payload;
    end
    formal_with_past <= 1'b1;
    _zz_1 <= ((a_fire && r_fire) && formal_with_past);
    _zz_2 <= ((a_fire && r_fire) && _zz_1);
  end


endmodule

Failed while upgrading to latest version, but works in Yosys 0.33.

The scripts used for yosys is

# running in unamed_cover/src/
read -formal unamed.sv
prep  -top unamed

hierarchy -smtcheck
rename -witness
write_jny -no-connections ../model/design.json
write_rtlil ../model/design.il

# running in unamed_cover/model/
read_ilang design.il
scc -select; simplemap; select -clear
memory_nordff
async2sync
chformal -assume -early
opt_clean
formalff -setundef -clk2ff -ff2anyinit -hierarchy
chformal -live -fair -remove
opt_clean
check
setundef -undriven -anyseq
opt -fast
rename -witness
opt_clean
write_rtlil ../model/design_prep.il

at this stage it report error.

Expected Behavior

The formal verification passes.

Actual Behavior

It reports that "ERROR: $check cell $cover$anon.sv:56$6 with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic."

I have traced on the generated RTLIL.
Previously, it would be

  attribute \src "unamed.sv:55.10-56.43"
  cell $cover $cover$unamed.sv:55$16
    connect \A $auto$rtlil.cc:2496:Mux$65
    connect \EN $auto$rtlil.cc:2496:Mux$49
  end

However, after upgrading the RTLIL become

  attribute \hdlname "_witness_ check_cover_unamed_sv_56_6"
  attribute \src "unamed.sv:56.7-56.43"
  cell $check \_witness_.check_cover_unamed_sv_56_6
    parameter \ARGS_WIDTH 0
    parameter \FLAVOR "cover"
    parameter \FORMAT ""
    parameter \PRIORITY 32'11111111111111111111111111111111
    parameter \TRG_ENABLE 1
    parameter \TRG_POLARITY 2'11
    parameter \TRG_WIDTH 2
    connect \A $logic_and$unamed.sv:56$8_Y
    connect \ARGS { }
    connect \EN 1'1
    connect \TRG { \reset \clk }
  end

In this case, the TRG_WIDTH become 2, which is not permit while runing async2sync command.

[povik]

As far as I can tell this is duplicate of #4231

[Readon]

As far as I can tell this is duplicate of #4231

Yes, it is