mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 03:32:29 +00:00
Add "write_smt2 -stdt" mode
This commit is contained in:
Clifford Wolf
parent
0ac72e759d
commit
106e44f406
2 changed files with 90 additions and 43 deletions
|
|
@ -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)));
|
||||
|
|
@ -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<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);
|
||||
|
||||
|
|
|
|||
|
|
@ -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,40 +83,6 @@ class SmtIo:
|
|||
self.info_stmts = list()
|
||||
self.nocomments = False
|
||||
|
||||
if self.solver == "yices":
|
||||
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
|
||||
|
||||
if self.solver == "z3":
|
||||
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
|
||||
|
||||
if self.solver == "cvc4":
|
||||
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts
|
||||
|
||||
if self.solver == "mathsat":
|
||||
self.popen_vargs = ['mathsat'] + self.solver_opts
|
||||
|
||||
if self.solver == "boolector":
|
||||
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
|
||||
self.unroll = True
|
||||
|
||||
if self.solver == "abc":
|
||||
if len(self.solver_opts) > 0:
|
||||
self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
|
||||
else:
|
||||
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
|
||||
self.logic_ax = False
|
||||
self.unroll = True
|
||||
self.noincr = True
|
||||
|
||||
if self.solver == "dummy":
|
||||
assert self.dummy_file is not None
|
||||
self.dummy_fd = open(self.dummy_file, "r")
|
||||
else:
|
||||
if self.dummy_file is not None:
|
||||
self.dummy_fd = open(self.dummy_file, "w")
|
||||
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
|
||||
|
|
@ -142,6 +109,41 @@ class SmtIo:
|
|||
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
|
||||
|
||||
if self.solver == "z3":
|
||||
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
|
||||
|
||||
if self.solver == "cvc4":
|
||||
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
|
||||
|
||||
if self.solver == "boolector":
|
||||
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
|
||||
self.unroll = True
|
||||
|
||||
if self.solver == "abc":
|
||||
if len(self.solver_opts) > 0:
|
||||
self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
|
||||
else:
|
||||
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
|
||||
self.logic_ax = False
|
||||
self.unroll = True
|
||||
self.noincr = True
|
||||
|
||||
if self.solver == "dummy":
|
||||
assert self.dummy_file is not None
|
||||
self.dummy_fd = open(self.dummy_file, "r")
|
||||
else:
|
||||
if self.dummy_file is not None:
|
||||
self.dummy_fd = open(self.dummy_file, "w")
|
||||
if not self.noincr:
|
||||
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
|
||||
|
||||
self.setup_done = True
|
||||
|
||||
|
|
@ -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()
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue