aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2/smtbmc.py')
-rw-r--r--backends/smt2/smtbmc.py159
1 files changed, 93 insertions, 66 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 498621612..9dba68b2a 100644
--- a/backends/smt2/smtbmc.py
+++ b/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
@@ -58,7 +59,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
-m <module_name>
name of the top module
- --constr <constr_filename>
+ --smtc <constr_filename>
read constraints file
--dump-vcd <vcd_filename>
@@ -69,14 +70,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
--dump-vlogtb <verilog_filename>
write trace as Verilog test bench
- --dump-constr <constr_filename>
+ --dump-smtc <constr_filename>
write trace as constraints file
""" + so.helpmsg())
sys.exit(1)
try:
- opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["constr=", "dump-vcd=", "dump-vlogtb=", "dump-constr="])
+ opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc="])
except:
usage()
@@ -92,13 +93,13 @@ for o, a in opts:
assume_skipped = int(a)
elif o == "-S":
step_size = int(a)
- elif o == "--constr":
+ elif o == "--smtc":
inconstr.append(a)
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-vlogtb":
vlogtbfile = a
- elif o == "--dump-constr":
+ elif o == "--dump-smtc":
outconstr = a
elif o == "-i":
tempind = True
@@ -116,47 +117,74 @@ if len(args) != 1:
if tempind and len(inconstr) != 0:
- print("Error: options -i and --constr are exclusive.");
+ print("Error: options -i and --smtc are exclusive.");
sys.exit(1)
-constr_asserts = dict()
-constr_assumes = dict()
+constr_asserts = defaultdict(list)
+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:
- constr_asserts[current_state] = list()
+ for state in current_states:
+ 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:
- constr_assumes[current_state] = list()
+ for state in current_states:
+ 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,35 +474,7 @@ if tempind:
break
-elif gentrace:
- retstatus = True
- for step in range(num_steps):
- smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
- smt.write("(assert (%s_u s%d))" % (topmod, step))
- smt.write("(assert (%s_a s%d))" % (topmod, step))
- smt.write("(assert (%s_h s%d))" % (topmod, step))
- smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
- smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
-
- if step == 0:
- smt.write("(assert (%s_i s0))" % (topmod))
- smt.write("(assert (%s_is s0))" % (topmod))
-
- else:
- smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
- smt.write("(assert (not (%s_is s%d)))" % (topmod, step))
-
- print("%s Creating trace of length %d.." % (smt.timestamp(), num_steps))
-
- if smt.check_sat() == "sat":
- write_trace(num_steps)
-
- else:
- print("%s Creating trace failed!" % smt.timestamp())
- retstatus = False
-
-
-else: # not tempind, not gentrace
+else: # not tempind
step = 0
retstatus = True
while step < num_steps:
@@ -495,30 +511,41 @@ else: # not tempind, not gentrace
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
last_check_step = step+i
- if last_check_step == step:
- print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
- else:
- print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
- smt.write("(push 1)")
+ if not gentrace:
+ if last_check_step == step:
+ print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
+ else:
+ print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
+ smt.write("(push 1)")
- smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
- [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
+ smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
+ [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
- if smt.check_sat() == "sat":
- print("%s BMC failed!" % smt.timestamp())
- print_failed_asserts(topmod, "s%d" % step, topmod)
- write_trace(step+step_size)
- retstatus = False
- break
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ print_failed_asserts(topmod, "s%d" % step, topmod)
+ write_trace(step+step_size)
+ retstatus = False
+ break
- else: # unsat
smt.write("(pop 1)")
- for i in range(step, last_check_step+1):
- smt.write("(assert (%s_a s%d))" % (topmod, i))
- smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
+
+ for i in range(step, last_check_step+1):
+ smt.write("(assert (%s_a s%d))" % (topmod, i))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
+
+ if gentrace:
+ print("%s Solving for step %d.." % (smt.timestamp(), step))
+ if smt.check_sat() != "sat":
+ print("%s No solution found!" % smt.timestamp())
+ retstatus = False
+ break
step += step_size
+ if gentrace:
+ write_trace(num_steps)
+
smt.write("(exit)")
smt.wait()
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 06:38:29 +0000