sby/docs/examples/indinv/README.md

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](example.sv)):

```SystemVerilog
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](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`:

```SystemVerilog
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.

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

Or, using more fancy SystemVerilog syntax:

```SystemVerilog
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:

```SystemVerilog
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.

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

The SBY file [prove_p23.sby](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](prove_p0.sby) demonstrates how to prove the original
property `p0`, using the inductive invariants we found to strengthen the proof.