riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Added boolector support to yosys-smtbmc

This commit is contained in:
Clifford Wolf 2016-09-03 14:26:00 +02:00
parent d2eba7631f
commit fa5565b606
3 changed files with 58 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
backends/smt2/smt2.cc
View File

@ -751,27 +751,39 @@ struct Smt2Worker
string assert_expr = assert_list.empty() ? "true" : "(and"; string assert_expr = assert_list.empty() ? "true" : "(and";
if (!assert_list.empty()) { if (!assert_list.empty()) {
for (auto &str : assert_list) if (GetSize(assert_list) == 1) {
assert_expr += stringf("\n %s", str.c_str()); assert_expr = assert_list.front();
assert_expr += "\n)"; } else {
for (auto &str : assert_list)
assert_expr += stringf("\n %s", str.c_str());
assert_expr += "\n)";
}
} }
decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n", decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
get_id(module), get_id(module), assert_expr.c_str())); get_id(module), get_id(module), assert_expr.c_str()));
string assume_expr = assume_list.empty() ? "true" : "(and"; string assume_expr = assume_list.empty() ? "true" : "(and";
if (!assume_list.empty()) { if (!assume_list.empty()) {
for (auto &str : assume_list) if (GetSize(assume_list) == 1) {
assume_expr += stringf("\n %s", str.c_str()); assume_expr = assume_list.front();
assume_expr += "\n)"; } else {
for (auto &str : assume_list)
assume_expr += stringf("\n %s", str.c_str());
assume_expr += "\n)";
}
} }
decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n", decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
get_id(module), get_id(module), assume_expr.c_str())); get_id(module), get_id(module), assume_expr.c_str()));
string init_expr = init_list.empty() ? "true" : "(and"; string init_expr = init_list.empty() ? "true" : "(and";
if (!init_list.empty()) { if (!init_list.empty()) {
for (auto &str : init_list) if (GetSize(init_list) == 1) {
init_expr += stringf("\n %s", str.c_str()); init_expr = init_list.front();
init_expr += "\n)"; } else {
for (auto &str : init_list)
init_expr += stringf("\n %s", str.c_str());
init_expr += "\n)";
}
} }
decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n", decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
get_id(module), get_id(module), init_expr.c_str())); get_id(module), get_id(module), init_expr.c_str()));

44
backends/smt2/smtbmc.py
View File

@ -514,17 +514,17 @@ if tempind:
retstatus = False retstatus = False
skip_counter = step_size skip_counter = step_size
for step in range(num_steps, -1, -1): for step in range(num_steps, -1, -1):
smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (|%s_u| s%d))" % (topmod, step))
smt.write("(assert (%s_h s%d))" % (topmod, step)) smt.write("(assert (|%s_h| s%d))" % (topmod, step))
smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
if step == num_steps: if step == num_steps:
smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) smt.write("(assert (not (|%s_a| s%d)))" % (topmod, step))
else: else:
smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1))
smt.write("(assert (%s_a s%d))" % (topmod, step)) smt.write("(assert (|%s_a| s%d))" % (topmod, step))
if step > num_steps-skip_steps: if step > num_steps-skip_steps:
print("%s Skipping induction in step %d.." % (smt.timestamp(), step)) print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
@ -560,23 +560,23 @@ else: # not tempind
step = 0 step = 0
retstatus = True retstatus = True
while step < num_steps: while step < num_steps:
smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (|%s_u| s%d))" % (topmod, step))
smt.write("(assert (%s_h s%d))" % (topmod, step)) smt.write("(assert (|%s_h| s%d))" % (topmod, step))
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
if step == 0: if step == 0:
smt.write("(assert (%s_i s0))" % (topmod)) smt.write("(assert (|%s_i| s0))" % (topmod))
smt.write("(assert (%s_is s0))" % (topmod)) smt.write("(assert (|%s_is| s0))" % (topmod))
else: else:
smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
if step < skip_steps: if step < skip_steps:
if assume_skipped is not None and step >= assume_skipped: if assume_skipped is not None and step >= assume_skipped:
print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step)) print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step))
smt.write("(assert (%s_a s%d))" % (topmod, step)) smt.write("(assert (|%s_a| s%d))" % (topmod, step))
smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
else: else:
print("%s Skipping step %d.." % (smt.timestamp(), step)) print("%s Skipping step %d.." % (smt.timestamp(), step))
@ -586,10 +586,10 @@ else: # not tempind
last_check_step = step last_check_step = step
for i in range(1, step_size): for i in range(1, step_size):
if step+i < num_steps: if step+i < num_steps:
smt.write("(declare-fun s%d () %s_s)" % (step+i, topmod)) smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step+i)) smt.write("(assert (|%s_u| s%d))" % (topmod, step+i))
smt.write("(assert (%s_h s%d))" % (topmod, step+i)) smt.write("(assert (|%s_h| s%d))" % (topmod, step+i))
smt.write("(assert (%s_t s%d s%d))" % (topmod, step+i-1, step+i)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i))
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i)) smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
last_check_step = step+i last_check_step = step+i
@ -601,7 +601,7 @@ else: # not tempind
print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step)) print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
smt.write("(push 1)") 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)] + 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)])) [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
if smt.check_sat() == "sat": if smt.check_sat() == "sat":
@ -616,7 +616,7 @@ else: # not tempind
smt.write("(pop 1)") smt.write("(pop 1)")
for i in range(step, last_check_step+1): for i in range(step, last_check_step+1):
smt.write("(assert (%s_a s%d))" % (topmod, i)) smt.write("(assert (|%s_a| s%d))" % (topmod, i))
smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
if constr_final_start is not None: if constr_final_start is not None:
@ -644,7 +644,7 @@ else: # not tempind
else: # gentrace else: # gentrace
for i in range(step, last_check_step+1): for i in range(step, last_check_step+1):
smt.write("(assert (%s_a s%d))" % (topmod, i)) smt.write("(assert (|%s_a| s%d))" % (topmod, i))
smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
print("%s Solving for step %d.." % (smt.timestamp(), last_check_step)) print("%s Solving for step %d.." % (smt.timestamp(), last_check_step))

17
backends/smt2/smtio.py
View File

@ -17,8 +17,7 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
# #
import sys import sys, subprocess, re
import subprocess
from select import select from select import select
from time import time from time import time
@ -84,6 +83,10 @@ class SmtIo:
if self.solver == "mathsat": if self.solver == "mathsat":
popen_vargs = ['mathsat'] popen_vargs = ['mathsat']
if self.solver == "boolector":
self.declared_sorts = list()
popen_vargs = ['boolector', '--smt2', '-i']
self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
self.start_time = time() self.start_time = time()
@ -104,11 +107,21 @@ class SmtIo:
def write(self, stmt): def write(self, stmt):
stmt = stmt.strip() stmt = stmt.strip()
if self.solver == "boolector":
if stmt.startswith("(declare-sort"):
self.declared_sorts.append(stmt.split()[1])
return
for n in self.declared_sorts:
stmt = stmt.replace(n, "(_ BitVec 16)")
if self.debug_print: if self.debug_print:
print("> %s" % stmt) print("> %s" % stmt)
if self.debug_file: if self.debug_file:
print(stmt, file=self.debug_file) print(stmt, file=self.debug_file)
self.debug_file.flush() self.debug_file.flush()
self.p.stdin.write(bytes(stmt + "\n", "ascii")) self.p.stdin.write(bytes(stmt + "\n", "ascii"))
self.p.stdin.flush() self.p.stdin.flush()