Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Previously working example now fails on newest version #279

Open
fayalalebrun opened this issue Jun 2, 2024 · 3 comments
Open

Previously working example now fails on newest version #279

fayalalebrun opened this issue Jun 2, 2024 · 3 comments

Comments

@fayalalebrun
Copy link

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
Copy link

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
Copy link

Readon commented Jun 3, 2024

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
Copy link

Readon commented Jun 3, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants