Proof engine is going into wrong case in case statement

[lejar]

The issue

When running a formal proof on my module (below), the default case of my case statement is being triggered, even though the input is defined in another case.

What I would expect is that the proof passes. Someone in the slack ran it through Verific for me, and it passed there. Removing the default line in the design causes the proof to pass.

SBY 16:51:34 [cascade_prf] summary: engine_0 (smtbmc) returned pass for basecase
SBY 16:51:34 [cascade_prf] summary: engine_0 (smtbmc) returned FAIL for induction
SBY 16:51:34 [cascade_prf] summary: counterexample trace [induction]: cascade_prf/engine_0/trace_induct.vcd
SBY 16:51:34 [cascade_prf] summary:   failed assertion cascade._witness_.check_assert_cascade_v_90_45 at cascade.v:90.10-90.31 in step 0

Steps to reproduce the issue

The verilog module in question:

`default_nettype none


module cascade(i_clk, i_req, o_led);
    input wire i_clk;
    input wire i_req;

    output reg [5:0] o_led;

    initial o_led = 6'h0;

    wire busy;

    reg [3:0] state;
    initial state = 4'b0;

    // As soon as we start the sequence, stay busy until we finish.
    assign busy = (state != 0);

    always @(posedge i_clk)
    begin
        if (i_req && !busy)
            state <= 4'h1;
        else if (state >= 4'hb)
        begin
            state <= 4'h0;
        end
        else if (state != 0)
            state <= state + 1'b1;
    end

    always @(state)
    begin
        case(state)
            4'h1: o_led = 6'b00_0001;
            4'h2: o_led = 6'b00_0010;
            4'h3: o_led = 6'b00_0100;
            4'h4: o_led = 6'b00_1000;
            4'h5: o_led = 6'b01_0000;
            4'h6: o_led = 6'b10_0000;
            4'h7: o_led = 6'b01_0000;
            4'h8: o_led = 6'b00_1000;
            4'h9: o_led = 6'b00_0100;
            4'ha: o_led = 6'b00_0010;
            4'hb: o_led = 6'b00_0001;

            default:
                o_led = 6'b00_0000;
        endcase
    end

// Verification code.
`ifdef  FORMAL
    reg f_past_valid;
    initial f_past_valid = 0;
    always @(posedge i_clk)
        f_past_valid = 1'b1;

    initial assume(!i_req);
    // No overlapping requests.
    always @(posedge i_clk)
    if (busy)
    begin
        assume(!i_req);
    end

    always @(posedge i_clk)
    begin
        // At some point, we should be busy and then not busy.
        if (f_past_valid)
            cover(!busy && $past(busy));
    end

    always @(*)
    assert(busy != (state == 0));

    always @(posedge i_clk)
    if (f_past_valid && $past(busy) && $past(state) < 4'hb)
    begin
        assert(state == ($past(state) + 1));
    end

    always @(state)
    begin
        case(state)
            4'h0: assert(o_led == 6'h0);
            4'h1: assert(o_led == 6'h1);
            4'h2: assert(o_led == 6'h2);
            4'h3: assert(o_led == 6'h4);
            4'h4: assert(o_led == 6'h8);
            4'h5: assert(o_led == 6'h10);
            4'h6: assert(o_led == 6'h20);
            4'h7: assert(o_led == 6'h10);
            4'h8: assert(o_led == 6'h8);
            4'h9: assert(o_led == 6'h4);
            4'ha: assert(o_led == 6'h2);
            4'hb: assert(o_led == 6'h1);

            default:
                assert(o_led == 6'b00_0000);
        endcase
    end

    always @(*)
        assert(state <= 4'hc);

`endif

endmodule

SymbiYosys configuration file

[tasks]
prf
cvr

[options]
prf: mode prove
cvr: mode cover

[engines]
smtbmc

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

[files]
cascade.v

Run with sby -f cascade.sby.

[KrystalDelusion]

Having looked into this a bit further, it seems that both read_verilog and verific generate a mux-fed $dlatch for o_led when there is no default case. But when there is a default case, read_verilog generates a $mem_v2 which fails induction in SBY, but verific generates a mux (now without the latch) and passes induction. Although I have no idea why that difference is occurring, or why it makes it fail.

[lejar]

I think this is a duplicate of #3378

[KrystalDelusion]

That does indeed appear to be the underlying issue. Thanks @lejar !