Add inductive invariants example

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

docs/examples/indinv/README.md

@@ -0,0 +1,120 @@
+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(input logic clk, output reg [4:0] state); 
+	initial 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 `state != 0` is a true invariant for our circuit, but it is not an inductive invariant,
+because we can go from a state for which `state != 0` is true to a state for
+which it is false. Specifically there are two such states for this circuit: 1 and 17
+
+(The property `state != 0` is k-inductive for k=4, but for this example we are
+only interested in 1-induction.)
+
+However, the following property 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.