From: Clifford Wolf Date: Sat, 20 Aug 2016 16:41:57 +0000 (+0200) Subject: Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end impro... X-Git-Tag: yosys-0.7~121 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c325bae792a953037c115ad6763081c7ad15f01c;p=yosys.git Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end improvements --- diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index da65b7bce..9acbfbeb8 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -32,7 +32,7 @@ struct Smt2Worker CellTypes ct; SigMap sigmap; RTLIL::Module *module; - bool bvmode, memmode, regsmode, wiresmode, verbose; + bool bvmode, memmode, wiresmode, verbose; int idcounter; std::vector decls, trans, hier; @@ -44,9 +44,9 @@ struct Smt2Worker std::map memarrays; std::map bvsizes; - Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool wiresmode, bool verbose) : + Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), - regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0) + wiresmode(wiresmode), verbose(verbose), idcounter(0) { decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module))); decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", log_id(module), log_id(module))); @@ -383,7 +383,13 @@ struct Smt2Worker if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's'); if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's'); - // FIXME: $shift $shiftx + if (cell->type.in("$shift", "$shiftx")) { + if (cell->getParam("\\B_SIGNED").as_bool()) { + /* FIXME */ + } else { + return export_bvop(cell, "(bvlshr A B)", 's'); + } + } if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b'); if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b'); @@ -454,6 +460,7 @@ struct Smt2Worker decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", log_id(module), arrayid, log_id(module), abits, width, log_id(cell))); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d\n", log_id(cell), abits, width)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n", log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid)); @@ -542,21 +549,18 @@ struct Smt2Worker if (verbose) log("=> export logic driving outputs\n"); pool reg_bits; - if (regsmode) { - for (auto cell : module->cells()) - if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) { - // not using sigmap -- we want the net directly at the dff output - for (auto bit : cell->getPort("\\Q")) - reg_bits.insert(bit); - } - } + for (auto cell : module->cells()) + if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) { + // not using sigmap -- we want the net directly at the dff output + for (auto bit : cell->getPort("\\Q")) + reg_bits.insert(bit); + } for (auto wire : module->wires()) { bool is_register = false; - if (regsmode) - for (auto bit : SigSpec(wire)) - if (reg_bits.count(bit)) - is_register = true; + for (auto bit : SigSpec(wire)) + if (reg_bits.count(bit)) + is_register = true; if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) { RTLIL::SigSpec sig = sigmap(wire); if (wire->port_input) @@ -753,8 +757,8 @@ struct Smt2Backend : public Backend { log("\n"); log("The '_s' sort represents a module state. Additional '_n' functions\n"); log("are provided that can be used to access the values of the signals in the module.\n"); - log("By default only ports, and signals with the 'keep' attribute set are made\n"); - log("available via such functions. Without the -bv option, multi-bit wires are\n"); + log("By default only ports, registers, and wires with the 'keep' attribute set are\n"); + log("made available via such functions. Without the -bv option, multi-bit wires are\n"); log("exported as separate functions of type Bool for the individual bits. With the\n"); log("-bv option multi-bit wires are exported as single functions of type BitVec.\n"); log("\n"); @@ -792,11 +796,9 @@ struct Smt2Backend : public Backend { log(" will be generated for accessing the arrays that are used to represent\n"); log(" memories.\n"); log("\n"); - log(" -regs\n"); - log(" also create '_n' functions for all registers.\n"); - log("\n"); log(" -wires\n"); - log(" also create '_n' functions for all public wires.\n"); + log(" create '_n' functions for all public wires. by default only ports,\n"); + log(" registers, and wires with the 'keep' attribute set are exported.\n"); log("\n"); log(" -tpl \n"); log(" use the given template file. the line containing only the token '%%%%'\n"); @@ -854,7 +856,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 = false, memmode = false, regsmode = false, wiresmode = false, verbose = false; + bool bvmode = false, memmode = false, wiresmode = false, verbose = false; log_header(design, "Executing SMT2 backend.\n"); @@ -876,10 +878,6 @@ struct Smt2Backend : public Backend { memmode = true; continue; } - if (args[argidx] == "-regs") { - regsmode = true; - continue; - } if (args[argidx] == "-wires") { wiresmode = true; continue; @@ -942,7 +940,7 @@ struct Smt2Backend : public Backend { log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); - Smt2Worker worker(module, bvmode, memmode, regsmode, wiresmode, verbose); + Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose); worker.run(); worker.write(*f); }