sby/docs/examples/indinv

Proving and Using Inductive Invariants for Interval Property Checking

Inductive invariants are boolean functions over the design state, that

1. return true for every reachable state (=invariants), and
2. if they return true for a state then they will also return true for every state reachable from the given state (=inductive)

Formally, inductive invariants are sets of states that are closed under the state transition function (=inductive), and contain the entire set of reachable states (=invariants).

A user-friendly set of features to support Inductive Invariants (and Interval Property Checking) is in development. Until this is completed we recommend the following technique for proving and using inductive invariants.

Consider the following circuit (stripped-down example.sv):

module example(clk, state); 
	input logic clk;
	output logic [4:0] state = 27;

	always_ff @(posedge clk) state <= (5'd 2 * state - 5'd 1) ^ (state & 5'd 7);

	always_comb assert (state != 0);
endmodule

For better understanding of this circuit we provide the complete state graph for that example design (as generated by example.py):

The 5-bit function f(x) produces 2 loops:
   f = lambda x: (2*x-1) ^ (x&7)

4-Element Loop:
   31 ->- 26 ->- 17 ->-  0 ->- 31
8 Lead-Ins:
    0 -<-  1 -<-  2
             `<- 18
   17 -<- 10 -<-  7
             `<- 23
   26 -<- 15 -<-  8
             `<- 24
   31 -<- 16 -<-  9
             `<- 25

4-Element Loop:
   28 ->- 19 ->-  6 ->- 13 ->- 28
8 Lead-Ins:
    6 -<-  3 -<-  4
             `<- 20
   13 -<- 22 -<- 11
             `<- 27
   19 -<- 12 -<-  5
             `<- 21
   28 -<- 29 -<- 14
             `<- 30

Loop Membership:
   (31, 26, 17, 0) |***....****....****....****....*|
   (28, 19, 6, 13) |...****....****....****....****.|

We can see that there are two distinct sets of states. The assertion state != 0 holds because the init state 27 is in the second set of states, and the zero-state is in the first set of states. Let's call the state != 0 property p0:

let p0 = (state != 0);

So p0 is a true invariant for our circuit, but it is not an inductive invariant, because we can go from a state for which p0 is true to a state for which it is false. Specifically there are two such states for this circuit: 1 and 17

(The property p0 is k-inductive for k=6, but for this example we are only interested in proofs via 1-induction.)

The following property however would be inductive, as can be easily confirmed by looking up the 4 states in the state chart above.

let p1 = (state == 28 || state == 19 || state == 6 || state == 13);

Or, using more fancy SystemVerilog syntax:

let p1 = (state inside {28, 19, 6, 13});

But p1 is not an invariant of our circuit, as can be easily seen: The initial state 27 is not one of the 4 states included in our property.

We can of course add additional states to our property until it covers the entire path from the initial state to state 13:

let p2 = (state inside {28, 19, 6, 13, 22, 27});

The property p2 is an inductive invariant. Actually, it is an exact description of the reachable state space. (As such it is by definition an invariant of the circuit, and inductive.)

However, in real-world verification problems we can't usually enumerate states like this. Instead, we need to find more generic functions that are inductive invariants of the circuit. In almost all cases those will be functions that over-estimate the set of reachable states, instead of describing it exact.

One such function for the above design would be the following property.

let p3 = (state[0] & state[1]) ^ state[2];

The SBY file prove_p23.sby demonstrates how to prove that p2 and p3 are inductive invariants. (Trying to prove p0 or p1 in that manner fails, as they are not inductive invariants.)

And finally prove_p0.sby demonstrates how to prove the original property p0, using the inductive invariants we found to strengthen the proof.