Add inductive invariants example

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

diff --git a/docs/examples/indinv/.gitignore b/docs/examples/indinv/.gitignore
new file mode 100644 (file)
index 0000000..679747b
--- /dev/null
+++ b/docs/examples/indinv/.gitignore
@@ -0,0 +1,3 @@
+/prove_p0_k/
+/prove_p0_p[0123]/
+/prove_p23_p[0123]/

diff --git a/docs/examples/indinv/README.md b/docs/examples/indinv/README.md
new file mode 100644 (file)
index 0000000..feae9ac
--- /dev/null
+++ b/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.

diff --git a/docs/examples/indinv/example.py b/docs/examples/indinv/example.py
new file mode 100644 (file)
index 0000000..0ef9048
--- /dev/null
+++ b/docs/examples/indinv/example.py
@@ -0,0 +1,96 @@
+from collections import defaultdict
+import inspect
+
+N = 32
+f = lambda x: (2*x-1) ^ (x&7)
+
+table = [f(i) & (N-1) for i in range(N)]
+rtable = [table.count(i) for i in range(N)]
+
+def getPath(v):
+    if table[v] is None:
+        return [v]
+    bak = table[v]
+    table[v] = None
+    r = [v] + getPath(bak)
+    table[v] = bak
+    return r
+
+def getPaths():
+    visited = set()
+    paths = list()
+    for i in range(N):
+        if rtable[i] == 0:
+            paths.append(getPath(i))
+    for path in paths:
+        for i in path:
+            visited.add(i)
+    for i in range(N):
+        if i not in visited:
+            paths.append(getPath(i))
+            for j in paths[-1]:
+                visited.add(j)
+    return paths
+
+pathsByLidx = defaultdict(set)
+loopsByIdx = dict()
+loopsByLidx = dict()
+
+for path in getPaths():
+    i = path.index(path[-1])+1
+    head, loop, lidx = tuple(path[:i]), tuple(path[i:]), max(path[i:])
+    pathsByLidx[lidx].add((head, loop))
+
+print()
+print("The %d-bit function f(x) produces %d loops:" % (N.bit_length()-1, len(pathsByLidx)))
+print("  ", inspect.getsource(f).strip())
+
+for lidx, paths in pathsByLidx.items():
+    loop = None
+    for path in paths:
+        for i in path[0] + path[1]:
+            loopsByIdx[i] = lidx
+        if loop is None or path[1][0] > loop[0]:
+            loop = path[1]
+
+    loopsByLidx[lidx] = loop
+    
+    print()
+    print("%d-Element Loop:" % len(loop))
+    print("  ", " ->- ".join(["%2d" % i for i in loop + (loop[0],)]))
+
+    lines = []
+    lastPath = []
+    for path in sorted([tuple(reversed(p[0])) for p in paths]):
+        line = ""
+        for i in range(len(path)):
+            if i < len(lastPath) and lastPath[i] == path[i]:
+                line += " %s   " % (" " if i == 0 else "|  ")
+            else:
+                line += " %s %2d" % (" " if i == 0 else "`<-" if len(lastPath) else "-<-", path[i])
+                lastPath = []
+        lastPath = path
+        lines.append(line)
+
+    for i in range(len(lines)-1, -1, -1):
+        line, nextline = list(lines[i]), "" if i == len(lines)-1 else lines[i+1]
+        if len(nextline) < len(line): nextline = nextline.ljust(len(line))
+
+        for k in range(len(line)):
+            if line[k] == "|" and nextline[k] in " -":
+                line[k] = " "
+
+        lines[i] = "".join(line)
+
+    print("%d Lead-Ins:" % len(lines))
+    for line in lines:
+        print(line)
+
+print()
+print("Loop Membership:")
+for lidx in pathsByLidx:
+    print("%18s |" % (loopsByLidx[lidx],), end="")
+    for i in range(N):
+        print("*" if loopsByIdx[i] == lidx else ".", end="")
+    print("|")
+print()

diff --git a/docs/examples/indinv/example.sv b/docs/examples/indinv/example.sv
new file mode 100644 (file)
index 0000000..40f0c7f
--- /dev/null
+++ b/docs/examples/indinv/example.sv
@@ -0,0 +1,18 @@
+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);
+
+       let p0 = (state != 0);
+       let p1 = (state inside {28, 19, 6, 13});
+       let p2 = (state inside {28, 19, 6, 13, 22, 27});
+       let p3 = (state[0] & state[1]) ^ state[2];
+
+`ifdef ASSERT_PX
+       always_comb assert (`ASSERT_PX);
+`endif
+`ifdef ASSUME_PX
+       always_comb assume (`ASSUME_PX);
+`endif
+endmodule

diff --git a/docs/examples/indinv/prove_p0.sby b/docs/examples/indinv/prove_p0.sby
new file mode 100644 (file)
index 0000000..3d8fbd1
--- /dev/null
+++ b/docs/examples/indinv/prove_p0.sby
@@ -0,0 +1,27 @@
+[tasks]
+: p0
+: p1
+p2
+p3
+k
+
+[options]
+mode prove
+k:  depth 6
+~k: depth 1
+
+[engines]
+smtbmc
+
+[script]
+read -verific
+read -define ASSERT_PX=p0
+p0: read -define ASSUME_PX=p0
+p1: read -define ASSUME_PX=p1
+p2: read -define ASSUME_PX=p2
+p3: read -define ASSUME_PX=p3
+read -sv example.sv
+prep -top example
+
+[files]
+example.sv

diff --git a/docs/examples/indinv/prove_p23.sby b/docs/examples/indinv/prove_p23.sby
new file mode 100644 (file)
index 0000000..fe1b025
--- /dev/null
+++ b/docs/examples/indinv/prove_p23.sby
@@ -0,0 +1,26 @@
+[tasks]
+: p0 unknown
+: p1 failing
+p2
+p3
+
+[options]
+mode prove
+depth 1
+unknown: expect unknown
+failing: expect fail
+
+[engines]
+smtbmc
+
+[script]
+read -verific
+p0: read -define ASSERT_PX=p0
+p1: read -define ASSERT_PX=p1
+p2: read -define ASSERT_PX=p2
+p3: read -define ASSERT_PX=p3
+read -sv example.sv
+prep -top example
+
+[files]
+example.sv