Search code examples
verilogformal-verificationyosys

Formal verification of state machine with SymbiYosys not giving expected results

I'm trying to verify a very simple state machine written in verilog with SymbiYosys. It is failing and I cannot figure out what I am doing incorrectly, and would like some help in figuring it out. I have an incoming request signal, and the state machine will cycle through LEDs lighting them up one by one, then back down.

What is happening in the induction step is that the output signal is getting set to zero, and the asserts for o_led based on state are failing.

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

vcd of the failing case: enter image description here

In the above image, you can see how o_led is zero, even though state has not yet reached its highest value.

My SymbiYosys configuration is as follows:

[tasks]
prf
cvr

[options]
prf: mode prove
cvr: mode cover

[engines]
smtbmc

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

[files]
cascade.v

and I'm running the command with sby -f cascade.sby.

The verilog module is:

`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
Solution

  • Yosys is synthesizing a ROM for the case switch that drives the value of o_led and you seem to have run into the issue described in https://github.com/YosysHQ/yosys/issues/3378.

    Basically, this is an existing bug in yosys in how it represents ROM memory in the SMT solver. As a workaround, you can add memory_map -rom-only at the end of the [script] section of you sby file as follows:

    [script]
read -formal cascade.v
prep -top cascade
memory_map -rom-only

    Using the abc pdr engine instead of smtbmc also seems to work in this case.