Formal Verification : Unconstrained Initial Value Leads to Invalid Verification Results

[Qin141209]

Hello Everyone,

I hope this message finds you well. I am currently trying to use Yosys for formal verification, but I've encountered a couple of issues. Here is a test case:

module test(clk, rst);
input clk, rst;
reg [3:0] a;
wire [3:0] b;

always @(posedge clk or negedge rst) begin
    if (!rst) begin
        a <= 4'b0000;
    end
    else begin if (a <= 4'b1000)
        a <= a + 4'b0001;
    else begin
        a <= 4'b0001;
    end
end

assign b = a;

assert property(b <= 4'b1000);

endmodule

In this test case, there is a counter a that is incremented by 1 on each clock cycle, but it resets to 4'b0000 when rst is low. The assertion b <= 4'b1000 is used to check that b (which is assigned the value of a) does not exceed 4'b1000.

The first issue arises because at time 0, a can have an arbitrary value. While I can resolve this by explicitly setting a to 4'b0000 at time 0, this solution becomes impractical for larger designs where many registers may need initialization, and some registers may not be initialized through reset.

Additionally, this situation may lead to a problem where I could potentially reach any state when verifying a state machine circuit. This is because the initial state of the state machine is not constrained by the reset condition.

I would like to know how to address these issues, such as using assume statements or other techniques in Yosys for formal verification. Any guidance on how to handle these situations would be greatly appreciated. Thank you for your help.

[Qin141209]

I am using the large scale as an example to illustrate that it is not easy to assign an initial value to all registers, especially when some registers do not have a reset initialization.

I want to convey the issue of how to establish a constraint on the initial values of all registers at the initial time step by setting a constraint on the reset signal. However, the reset signal is of type wire, and I cannot control it using initial.

[KrystalDelusion]

I would instead phrase this as two questions:

1. How to initialise the circuit into a known state (e.g. reset), and
2. How to ignore assertions during the initial (potentially invalid) state.

For the first question there are a few options, the simplest is to add the following line:

initial assume (!rst);

Which will work for wires, registers, and anything else (and as an aside, if you have an active low reset like this it is common to put _n or similar after the name to signify).

Another option for if you want to reset once and only once:

reg init = 0;
always @(posedge clk) begin
    assume (rst == init);
    if (init) begin
        assert (b <= 4'b1000);
    end
    init <= 1;
end

This method then also solves the second question by only asserting once init goes high. However, the downside to taking the first question as a given is that forcing an initial state can limit the solver and hide bugs. For example, the common problem where you have a counter which evaluates if a == 4'b1000 rather than a >= 4'b1000. Such a case would pass verification from a valid initial state, but says nothing about the systems ability to recover from an invalid state.

Another option then is to ignore the first question entirely and let the solver do what the solver does. We are then left with the question of ignoring assertions in the initial state. If we want to verify that our design can recover from any invalid state within N cycles, and then raise an assertions on any invalid states after that we can do the following:

read_verilog -formal test.sv
prep -top test
chformal -assert -skip <N>

And as another aside, I do hope you are using SBY for formal verification rather than Yosys directly. While it is certainly possible to use Yosys in that way, SBY makes it much easier.

[Qin141209]

Thank you for your response! It completely resolved my doubts.