Not able to identify which assertion failed when using generators

[zputrle]

If I run the following program (test.v)

module test #(
    parameter n = 5
)
(
    input clk_i,
    input [n:0] x,
    input [n:0] y,
    output [n:0] z);

generate

genvar i;
for (i = 0; i < n; i = i + 1) begin

    if (i != 2) begin
        assign z[i] = x[i] & y[i];
    end

    always @(clk_i) begin
        assert (z[i] != (x[i] & y[i]));
    end

end

endgenerate

endmodule

with script

[tasks]
t_bmc

[options]
t_bmc: mode bmc
t_bmc: depth 30
t_bmc: append 0

[engines]
smtbmc --dumpsmt2 z3

[script]
read -formal test.v
prep -top test

[files]
tmp/test.v

I get the following output

...
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: starting process "cd ./run/verify_test_t_bmc; yosys-smtbmc -s z3 --presat --dump-smt2 engine_0/trace.smt2 --noprogress -t 30  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Solver: z3
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: test.v:22.9-22.39 (_witness_.check_assert_test_v_22_17)
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: test.v:22.9-22.39 (_witness_.check_assert_test_v_22_12)
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY 13:19:22 [./run/verify_test_t_bmc] engine_0: ##   0:00:00  Status: failed
...

As far as I can see, there is no way to determine which assertion has failed (in this case assert (z[2] != (x[2] & y[2]))) directly from the Symbiyosys's terminal output, or any other way, except for looking through the generated trace.

This is usually not a problem for small designs, but as you start to verify larger Verilog designs that rely on generators and parameters to be configurable, this becomes an annoying and time consuming problem as you need to figure out which assertion failed from the trace. This is especially problematic for designs that have a lot of repeating signals for different modules, e.g. interconnects.

This can probably be addressed by using assert (<cnd>) else $error(<msg>); pattern provided by SystemVerilog assertions, but this pattern is not supported in open source version of Symbiyosys.

Is there any way to get around this in the open source version of Symbiyosys?

I would argue that this problem can be a major drawback for using open source version of Symbiyosys in industrial setting.

Note that this problem might be specific to smtbmc backend.

[nakengelhardt]

Compounding this problem, if you try to give a label to the assertion, it errors out:

    always @(clk_i) begin
        p_label: assert (z[i] != (x[i] & y[i]));
    end

SBY 15:34:50 [test_t_bmc] base: starting process "cd test_t_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:34:50 [test_t_bmc] base: test.v:20: ERROR: Cannot add procedural assertion `\p_label' because a cell with the same name was already created at test.v:20.9-20.48!

With the verific frontend that would work around it by generating a different instance name for each iteration of the generate:

SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: genblk1[4].p_label
SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: genblk1[3].p_label
SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: genblk1[2].p_label
SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: genblk1[1].p_label
SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  Assert failed in test: genblk1[0].p_label
SBY 15:40:27 [test_t_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd

So if we could get read_verilog to disambiguate the labels/instance names in a similar way that would give a way to distinguish them.