aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2017-03-20 12:00:35 +0100
committerClifford Wolf <clifford@clifford.at>2017-03-20 12:00:35 +0100
commit106e44f406406766c0c99e46ffa5b582e54abeb1 (patch)
tree6e18733dea4c3cb752284c06955558a2d061b0ef /backends/smt2
parent0ac72e759d986149541ee6a90d185811e697c27b (diff)
downloadyosys-106e44f406406766c0c99e46ffa5b582e54abeb1.tar.gz
yosys-106e44f406406766c0c99e46ffa5b582e54abeb1.tar.bz2
yosys-106e44f406406766c0c99e46ffa5b582e54abeb1.zip
Add "write_smt2 -stdt" mode
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smt2.cc56
-rw-r--r--backends/smt2/smtio.py65
2 files changed, 84 insertions, 37 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9d07a1216..372dbeb57 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -32,11 +32,11 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
- bool bvmode, memmode, wiresmode, verbose, statebv;
+ bool bvmode, memmode, wiresmode, verbose, statebv, statedt;
dict<IdString, int> &mod_stbv_width;
int idcounter, statebv_width;
- std::vector<std::string> decls, trans, hier;
+ std::vector<std::string> decls, trans, hier, dtmembers;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
pool<Cell*> recursive_cells, registers;
@@ -78,6 +78,14 @@ struct Smt2Worker
statebv_width += width;
}
}
+ else if (statedt)
+ {
+ if (width == 0) {
+ decl_str = stringf(" (|%s| Bool)", name.c_str());
+ } else {
+ decl_str = stringf(" (|%s| (_ BitVec %d))", name.c_str(), width);
+ }
+ }
else
{
if (width == 0) {
@@ -89,12 +97,16 @@ struct Smt2Worker
if (!comment.empty())
decl_str += " ; " + comment;
- decls.push_back(decl_str + "\n");
+
+ if (statedt)
+ dtmembers.push_back(decl_str + "\n");
+ else
+ decls.push_back(decl_str + "\n");
}
- Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, dict<IdString, int> &mod_stbv_width) :
+ Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict<IdString, int> &mod_stbv_width) :
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
- verbose(verbose), statebv(statebv), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
+ verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
{
makebits(stringf("%s_is", get_id(module)));
@@ -583,8 +595,12 @@ struct Smt2Worker
}
else
{
- decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
- get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
+ if (statedt)
+ dtmembers.push_back(stringf(" (|%s#%d#0| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ get_id(module), arrayid, abits, width, get_id(cell)));
+ else
+ decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid));
@@ -649,6 +665,9 @@ struct Smt2Worker
if (statebv)
makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
+ if (statedt)
+ dtmembers.push_back(stringf(" (|%s_h %s| |%s_s|)\n",
+ get_id(module), get_id(cell->name), get_id(cell->type)));
else
decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
@@ -1010,6 +1029,12 @@ struct Smt2Worker
f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
mod_stbv_width[module->name] = statebv_width;
} else
+ if (statedt) {
+ f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module));
+ for (auto it : dtmembers)
+ f << it;
+ f << stringf(")))\n");
+ } else
f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));
for (auto it : decls)
@@ -1126,6 +1151,10 @@ struct Smt2Backend : public Backend {
log(" sort. As a side-effect this will prevent use of arrays to model\n");
log(" memories.\n");
log("\n");
+ log(" -stdt\n");
+ log(" Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n");
+ log(" uninterpreted sort.\n");
+ log("\n");
log(" -nobv\n");
log(" disable support for BitVec (FixedSizeBitVectors theory). without this\n");
log(" option multi-bit wires are represented using the BitVec sort and\n");
@@ -1199,7 +1228,7 @@ struct Smt2Backend : public Backend {
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
std::ifstream template_f;
- bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false;
+ bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
log_header(design, "Executing SMT2 backend.\n");
@@ -1218,6 +1247,12 @@ struct Smt2Backend : public Backend {
}
if (args[argidx] == "-stbv") {
statebv = true;
+ statedt = false;
+ continue;
+ }
+ if (args[argidx] == "-stdt") {
+ statebv = false;
+ statedt = true;
continue;
}
if (args[argidx] == "-nobv") {
@@ -1264,6 +1299,9 @@ struct Smt2Backend : public Backend {
if (statebv)
*f << stringf("; yosys-smt2-stbv\n");
+ if (statedt)
+ *f << stringf("; yosys-smt2-stdt\n");
+
std::vector<RTLIL::Module*> sorted_modules;
// extract module dependencies
@@ -1304,7 +1342,7 @@ struct Smt2Backend : public Backend {
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
- Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, mod_stbv_width);
+ Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width);
worker.run();
worker.write(*f);
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 38e3f3119..14ee787f6 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -53,6 +53,7 @@ class SmtIo:
self.logic_ax = True
self.logic_uf = True
self.logic_bv = True
+ self.logic_dt = False
self.produce_models = True
self.smt2cache = [list()]
self.p = None
@@ -82,6 +83,34 @@ class SmtIo:
self.info_stmts = list()
self.nocomments = False
+ if self.unroll:
+ self.logic_uf = False
+ self.unroll_idcnt = 0
+ self.unroll_buffer = ""
+ self.unroll_sorts = set()
+ self.unroll_objs = set()
+ self.unroll_decls = dict()
+ self.unroll_cache = dict()
+ self.unroll_stack = list()
+
+ self.start_time = time()
+
+ self.modinfo = dict()
+ self.curmod = None
+ self.topmod = None
+ self.setup_done = False
+
+ def setup(self):
+ assert not self.setup_done
+
+ if self.logic is None:
+ self.logic = ""
+ if self.logic_qf: self.logic += "QF_"
+ if self.logic_ax: self.logic += "A"
+ if self.logic_uf: self.logic += "UF"
+ if self.logic_bv: self.logic += "BV"
+ if self.logic_dt: self.logic = "ALL"
+
if self.solver == "yices":
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
@@ -89,7 +118,7 @@ class SmtIo:
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
if self.solver == "cvc4":
- self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts
+ self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
if self.solver == "mathsat":
self.popen_vargs = ['mathsat'] + self.solver_opts
@@ -116,33 +145,6 @@ class SmtIo:
if not self.noincr:
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
- if self.unroll:
- self.logic_uf = False
- self.unroll_idcnt = 0
- self.unroll_buffer = ""
- self.unroll_sorts = set()
- self.unroll_objs = set()
- self.unroll_decls = dict()
- self.unroll_cache = dict()
- self.unroll_stack = list()
-
- self.start_time = time()
-
- self.modinfo = dict()
- self.curmod = None
- self.topmod = None
- self.setup_done = False
-
- def setup(self):
- assert not self.setup_done
-
- if self.logic is None:
- self.logic = ""
- if self.logic_qf: self.logic += "QF_"
- if self.logic_ax: self.logic += "A"
- if self.logic_uf: self.logic += "UF"
- if self.logic_bv: self.logic += "BV"
-
self.setup_done = True
if self.produce_models:
@@ -209,6 +211,9 @@ class SmtIo:
def write(self, stmt, unroll=True):
if stmt.startswith(";"):
self.info(stmt)
+ if not self.setup_done:
+ self.info_stmts.append(stmt)
+ return
elif not self.setup_done:
self.setup()
@@ -304,6 +309,10 @@ class SmtIo:
if self.logic is None:
self.logic_bv = False
+ if fields[1] == "yosys-smt2-stdt":
+ if self.logic is None:
+ self.logic_dt = True
+
if fields[1] == "yosys-smt2-module":
self.curmod = fields[2]
self.modinfo[self.curmod] = SmtModInfo()