Previously working example now fails on newest version

[fayalalebrun]

I recently updated to the newest version of sby and yosys. Now some of the formal proofs generated by SpinalHDL no longer work (SpinalHDL issue). The error is: prep: ERROR: $check cell $cover$anon.sv:56$6 with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic.

If I add multiclock to [options] or clk2fflogic to [script], then I get:

Traceback (most recent call last):
  File "/usr/bin/sby", line 572, in <module>
    taskloop.run()
  File "/usr/bin/../share/yosys/python3/sby_core.py", line 591, in run
    proc.poll()
  File "/usr/bin/../share/yosys/python3/sby_core.py", line 170, in poll
    self.poll(True)
  File "/usr/bin/../share/yosys/python3/sby_core.py", line 211, in poll
    self.read_output()
  File "/usr/bin/../share/yosys/python3/sby_core.py", line 267, in read_output
    self.handle_output(outs)
  File "/usr/bin/../share/yosys/python3/sby_core.py", line 131, in handle_output
    line = self.output_callback(line)
  File "/usr/bin/../share/yosys/python3/sby_engine_smtbmc.py", line 243, in output_callback
    prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
  File "/usr/bin/../share/yosys/python3/sby_design.py", line 146, in find_property_by_cellname
    raise KeyError(f"No such property: {cell_name}")
KeyError: 'No such property: _witness_.cover_cover_anon_sv_56_6'

Here is an example:

[tasks]
bmc
prove
cover

[options]
bmc: mode bmc
prove: mode prove
cover: mode cover
bmc: depth 40
prove: depth 40
cover: depth 40

[engines]
smtbmc --progress yices

[script]
read -formal anon.sv
prep  -top anon

[files]
rtl/anon.sv

module anon (
  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

[slagernate]

I recently got sby working (after seeing similar error message IIRC) for some basic example by using the latest release of oss-cad-suite.

[Readon]

The problem seems to be that in previous yosys, it synthesize $assume(xxxx) to be individual cell. But in latest version it use $check cell widely.

But in $check cell the TRG_WIDTH is not allowed to be set larger than 1, when async2sync command is adopted. This case is widely met when the reset is asynchronous one. In those cases TRG condition have to be clk and reset both, which takes 2 bit width.

So that the multiclock on command is required in sby file to use clk2fflogic but async2sync command in yosys script file, which lead to a fail. I guess it's mainly caused by the concept of these two command where 'clk2fflogic' is targeting at global clock, but async2sync is not.

[Readon]

I recently got sby working (after seeing similar error message IIRC) for some basic example by using the latest release of oss-cad-suite.

I recently got sby working (after seeing similar error message IIRC) for some basic example by using the latest release of oss-cad-suite.

This example is fully a synchronous design, so that it works as usual.