More yosys-smtbmc smtc features

backends/smt2/smtbmc.py

@@ -20,6 +20,7 @@
 import os, sys, getopt, re
 ##yosys-sys-path##
 from smtio import smtio, smtopts, mkvcd
+from collections import defaultdict
 
 skip_steps = 0
 step_size = 1
@@ -120,43 +121,70 @@ if tempind and len(inconstr) != 0:
     sys.exit(1)
 
 
-constr_asserts = dict()
+constr_asserts = defaultdict(list)
-constr_assumes = dict()
+constr_assumes = defaultdict(list)
 
 for fn in inconstr:
-    current_state = None
+    current_states = None
 
     with open(fn, "r") as f:
         for line in f:
+            if line.startswith("#"):
+                continue
+
             tokens = line.split()
 
             if len(tokens) == 0:
                 continue
 
             if tokens[0] == "initial":
-                current_state = 0
+                current_states = set()
+                current_states.add(0)
                 continue
 
             if tokens[0] == "state":
-                current_state = int(tokens[1])
+                current_states = set()
+                for token in tokens[1:]:
+                    tok = token.split(":")
+                    if len(tok) == 1:
+                        current_states.add(int(token))
+                    elif len(tok) == 2:
+                        lower = int(tok[0])
+                        if tok[1] == "*":
+                            upper = num_steps
+                        else:
+                            upper = int(tok[1])
+                        for i in range(lower, upper+1):
+                            current_states.add(i)
+                    else:
+                        assert 0
+                continue
+
+            if tokens[0] == "always":
+                if len(tokens) == 1:
+                    current_states = set(range(0, num_steps+1))
+                elif len(tokens) == 2:
+                    i = int(tokens[1])
+                    assert i < 0
+                    current_states = set(range(-i, num_steps+1))
+                else:
+                    assert 0
                 continue
 
             if tokens[0] == "assert":
-                assert current_state is not None
+                assert current_states is not None
 
-                if current_state not in constr_asserts:
+                for state in current_states:
-                    constr_asserts[current_state] = list()
+                    constr_asserts[state].append(" ".join(tokens[1:]))
 
-                constr_asserts[current_state].append(" ".join(tokens[1:]))
                 continue
 
             if tokens[0] == "assume":
-                assert current_state is not None
+                assert current_states is not None
 
-                if current_state not in constr_assumes:
+                for state in current_states:
-                    constr_assumes[current_state] = list()
+                    constr_assumes[state].append(" ".join(tokens[1:]))
 
-                constr_assumes[current_state].append(" ".join(tokens[1:]))
                 continue
 
             assert 0
@@ -166,9 +194,25 @@ def get_constr_expr(db, state):
     if state not in db:
         return "true"
 
+    netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
+
+    def replace_netref(match):
+        state_sel = match.group(2)
+
+        if state_sel == "":
+            st = state
+        elif state_sel[0] == "-":
+            st = state + int(state_sel[:-1])
+        else:
+            st = int(state_sel[:-1])
+
+        expr = smt.net_expr(topmod, "s%d" % st, smt.get_path(topmod, match.group(3)))
+
+        return match.group(1) + expr
+
     expr_list = list()
     for expr in db[state]:
-        expr = re.sub(r'\[([^\]]+)\]', lambda match: smt.net_expr(topmod, "s%d" % state, smt.get_path(topmod, match.group(1))), expr)
+        expr = netref_regex.sub(replace_netref, expr)
         expr_list.append(expr)
 
     if len(expr_list) == 0:
@@ -430,7 +474,7 @@ if tempind:
             break
 
 
-else: # not tempind, not gentrace
+else: # not tempind
     step = 0
     retstatus = True
     while step < num_steps:

examples/smtbmc/.gitignore

@@ -1,9 +1,12 @@
 demo1.smt2
 demo1.yslog
 demo2.smt2
+demo2.smtc
 demo2.vcd
 demo2.yslog
 demo2_tb
-demo2_tb.smtc
 demo2_tb.v
 demo2_tb.vcd
+demo3.smt2
+demo3.vcd
+demo3.yslog

examples/smtbmc/Makefile

@@ -1,24 +1,31 @@
 
-all: demo1 demo2
+all: demo1 demo2 demo3
 
 demo1: demo1.smt2
 	yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
 	yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
 
 demo2: demo2.smt2
-	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-vlogtb demo2_tb.v --dump-smtc demo2_tb.smtc demo2.smt2
+	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-smtc demo2.smtc --dump-vlogtb demo2_tb.v demo2.smt2
 	iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
 	vvp demo2_tb +vcd=demo2_tb.vcd
 
+demo3: demo3.smt2
+	yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2
+
 demo1.smt2: demo1.v
 	yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2'
 
 demo2.smt2: demo2.v
 	yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires -mem -bv demo2.smt2'
 
+demo3.smt2: demo3.v
+	yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires -mem -bv demo3.smt2'
+
 clean:
 	rm -f demo1.yslog demo1.smt2 demo1.vcd
-	rm -f demo2.yslog demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd demo2_tb.smtc
+	rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
+	rm -f demo3.yslog demo3.smt2 demo3.vcd
 
-.PHONY: demo1 clean
+.PHONY: demo1 demo2 demo3 clean
 

examples/smtbmc/demo3.smtc

@@ -0,0 +1,5 @@
+initial
+assume [rst]
+
+always -1
+assert (= [-1:mem] [mem])

examples/smtbmc/demo3.v

@@ -0,0 +1,18 @@
+// Whatever the initial content of this memory is at reset, it will never change
+// see demo3.smtc for assumptions and assertions
+
+module demo3(input clk, rst, input [15:0] addr, output reg [31:0] data);
+	reg [31:0] mem [0:2**16-1];
+	reg [15:0] addr_q;
+
+	always @(posedge clk) begin
+		if (rst) begin
+			data <= mem[0] ^ 123456789;
+			addr_q <= 0;
+		end else begin
+			mem[addr_q] <= data ^ 123456789;
+			data <= mem[addr] ^ 123456789;
+			addr_q <= addr;
+		end
+	end
+endmodule