Closed Readon closed 3 weeks ago
Yosys 0.41+111
Linux, Windows
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.
The formal verification passes.
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.
async2sync
As far as I can tell this is duplicate of #4231
Yes, it is
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
Failed while upgrading to latest version, but works in Yosys 0.33.
The scripts used for yosys is
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
However, after upgrading the RTLIL become
In this case, the TRG_WIDTH become 2, which is not permit while runing
async2sync
command.