From: Clifford Wolf Date: Mon, 20 Mar 2017 11:00:35 +0000 (+0100) Subject: Add "write_smt2 -stdt" mode X-Git-Tag: yosys-0.8~455 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=106e44f406406766c0c99e46ffa5b582e54abeb1;p=yosys.git Add "write_smt2 -stdt" mode --- 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 &mod_stbv_width; int idcounter, statebv_width; - std::vector decls, trans, hier; + std::vector decls, trans, hier, dtmembers; std::map bit_driver; std::set exported_cells, hiercells, hiercells_queue; pool 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 &mod_stbv_width) : + Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict &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))); @@ -1009,6 +1028,12 @@ struct Smt2Worker if (statebv) { 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)); @@ -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 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 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()