chipsalliance / synlig

SystemVerilog support for Yosys
Apache License 2.0
144 stars 20 forks source link

Crash on reading file with assertions #2410

Open jjjt-git opened 2 months ago

jjjt-git commented 2 months ago

When reading the following file, yosys crashes.

`timescale 1ns/1ns
`default_nettype none

module mre (
    i_clk,
    i_w, o_w
);
    input wire i_clk, i_w;
    output reg o_w;

    reg f_past_valid;

    initial f_past_valid = 0;
    always @(posedge i_clk) begin
        o_w <= i_w;
        f_past_valid <= 1;
    end

    always @(posedge i_clk)
    if (f_past_valid & $past(i_w))
        assert(o_w);
endmodule

Removing the f_past_valid or $past(i_w) from the line with if (f_past_valid & $past(i_w)) will prevent the crash. The crash is also prevented, when swapping

always @(posedge i_clk)
if (f_past_valid & $past(i_w))
    assert(o_w);

with

assert property (
    @(posedge i_clk)
    (f_past_valid & $past(i_w)) |-> o_w
);

or

assert property (
    @(posedge i_clk)
    i_w |=> o_w
);

command:

yosys -m systemverilog -p "read_systemverilog -formal -debug -no_dump_ptr -dump_rtlil  mre.sv"

output: run.log

Versions:

yosys   0.38
synlig  2024-03-13-d844d8d
surelog 1.82
uhdm    1.82
jjjt-git commented 2 months ago

Ok, I have investigated a bit further and am now convinced, that the problem is something in my setup, since I get each and every single always-Block duplicated, which obviously causes problems. If you have an idea, pointers would be welcome.

jjjt-git commented 2 months ago

Found the problem with the duplicated always-blocks. Turns out I accidentality used the wrong surelog version.

However, the crash does still happen.