From 4a07e026ddb1342b4f21fa035002605dff67aa7c Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Fri, 17 Dec 2021 15:42:04 +0100 Subject: [PATCH] Add inductive invariants example Signed-off-by: Claire Xenia Wolf --- docs/examples/indinv/.gitignore | 3 + docs/examples/indinv/README.md | 120 +++++++++++++++++++++++++++++ docs/examples/indinv/example.py | 96 +++++++++++++++++++++++ docs/examples/indinv/example.sv | 18 +++++ docs/examples/indinv/prove_p0.sby | 27 +++++++ docs/examples/indinv/prove_p23.sby | 26 +++++++ 6 files changed, 290 insertions(+) create mode 100644 docs/examples/indinv/.gitignore create mode 100644 docs/examples/indinv/README.md create mode 100644 docs/examples/indinv/example.py create mode 100644 docs/examples/indinv/example.sv create mode 100644 docs/examples/indinv/prove_p0.sby create mode 100644 docs/examples/indinv/prove_p23.sby diff --git a/docs/examples/indinv/.gitignore b/docs/examples/indinv/.gitignore new file mode 100644 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 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 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 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 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 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 -- 2.30.2