From efac8a45a6965bdcbb7fb810d657d2c63b6cb7fe Mon Sep 17 00:00:00 2001 From: acw1251 Date: Tue, 18 Sep 2018 13:34:30 -0400 Subject: Fixed typo in "verilog_write" help message --- backends/verilog/verilog_backend.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index d3262ec47..ae9031510 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -1523,7 +1523,7 @@ struct VerilogBackend : public Backend { log("\n"); log(" -nodec\n"); log(" 32-bit constant values are by default dumped as decimal numbers,\n"); - log(" not bit pattern. This option decativates this feature and instead\n"); + log(" not bit pattern. This option deactivates this feature and instead\n"); log(" will write out all constants in binary.\n"); log("\n"); log(" -decimal\n"); @@ -1531,13 +1531,13 @@ struct VerilogBackend : public Backend { log("\n"); log(" -nohex\n"); log(" constant values that are compatible with hex output are usually\n"); - log(" dumped as hex values. This option decativates this feature and\n"); + log(" dumped as hex values. This option deactivates this feature and\n"); log(" instead will write out all constants in binary.\n"); log("\n"); log(" -nostr\n"); log(" Parameters and attributes that are specified as strings in the\n"); log(" original input will be output as strings by this back-end. This\n"); - log(" decativates this feature and instead will write string constants\n"); + log(" deactivates this feature and instead will write string constants\n"); log(" as binary numbers.\n"); log("\n"); log(" -defparam\n"); -- cgit v1.2.3 From 41affeeeb9935db73bb2774e74e6038a70cf667d Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 21 Sep 2018 20:43:49 +0200 Subject: added prefix to FDirection constants, fixing windows build --- backends/firrtl/firrtl.cc | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'backends') diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc index 94236d0b1..32410a651 100644 --- a/backends/firrtl/firrtl.cc +++ b/backends/firrtl/firrtl.cc @@ -33,22 +33,22 @@ dict namecache; int autoid_counter; typedef unsigned FDirection; -static const FDirection NODIRECTION = 0x0; -static const FDirection IN = 0x1; -static const FDirection OUT = 0x2; -static const FDirection INOUT = 0x3; +static const FDirection FD_NODIRECTION = 0x0; +static const FDirection FD_IN = 0x1; +static const FDirection FD_OUT = 0x2; +static const FDirection FD_INOUT = 0x3; // Get a port direction with respect to a specific module. FDirection getPortFDirection(IdString id, Module *module) { Wire *wire = module->wires_.at(id); - FDirection direction = NODIRECTION; + FDirection direction = FD_NODIRECTION; if (wire && wire->port_id) { if (wire->port_input) - direction |= IN; + direction |= FD_IN; if (wire->port_output) - direction |= OUT; + direction |= FD_OUT; } return direction; } @@ -193,16 +193,16 @@ struct FirrtlWorker FDirection dir = getPortFDirection(it->first, instModule); std::string source, sink; switch (dir) { - case INOUT: + case FD_INOUT: log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", log_id(cell_type), log_signal(it->second)); - case OUT: + case FD_OUT: source = firstName; sink = secondName; break; - case NODIRECTION: + case FD_NODIRECTION: log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", log_id(cell_type), log_signal(it->second)); /* FALL_THROUGH */ - case IN: + case FD_IN: source = secondName; sink = firstName; break; -- cgit v1.2.3 From 90e0938f9a94464ac48a8fd4acdfbf805216b763 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 1 Oct 2018 19:03:10 -0400 Subject: Update to .smv backend Splitting VAR and ASSIGN into IVAR, VAR, DEFINE and ASSIGN. This allows better handling by nuXmv for post-processing (since now only state variables are listed under VAR). --- backends/smv/smv.cc | 85 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 52 insertions(+), 33 deletions(-) (limited to 'backends') diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index b8383412b..a53ee7a7c 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -42,7 +42,7 @@ struct SmvWorker pool partial_assignment_wires; dict> partial_assignment_bits; - vector assignments, invarspecs; + vector inputvars, vars, definitions, assignments, invarspecs; const char *cid() { @@ -195,7 +195,7 @@ struct SmvWorker return rvalue(sig); const char *temp_id = cid(); - f << stringf(" %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig)); +// f << stringf(" %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig)); int offset = 0; for (auto bit : sig) { @@ -210,14 +210,14 @@ struct SmvWorker void run() { f << stringf("MODULE %s\n", cid(module->name)); - f << stringf(" VAR\n"); for (auto wire : module->wires()) { if (SigSpec(wire) != sigmap(wire)) partial_assignment_wires.insert(wire); - f << stringf(" %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire)); + if (wire->port_input) + inputvars.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire->name), wire->width, log_id(wire))); if (wire->attributes.count("\\init")) assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at("\\init")))); @@ -232,7 +232,7 @@ struct SmvWorker SigSpec sig_a = cell->getPort("\\A"); SigSpec sig_en = cell->getPort("\\EN"); - invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a))); + invarspecs.push_back(stringf("(!bool(%s) | bool(%s));", rvalue(sig_en), rvalue(sig_a))); continue; } @@ -275,8 +275,8 @@ struct SmvWorker const char *b_shr = rvalue_u(sig_b); const char *b_shl = cid(); - f << stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b)); - assignments.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b))); +// f << stringf(" %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b)); + definitions.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b))); string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y); string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y); @@ -303,7 +303,7 @@ struct SmvWorker GetSize(sig_b)-shift_b_width, width_y, expr.c_str()); } - assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str())); + definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str())); continue; } @@ -319,12 +319,12 @@ struct SmvWorker if (cell->getParam("\\A_SIGNED").as_bool()) { - assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue_s(cell->getPort("\\A"), width))); } else { - assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue_u(cell->getPort("\\A"), width))); } @@ -346,12 +346,12 @@ struct SmvWorker if (cell->getParam("\\A_SIGNED").as_bool()) { - assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")), rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width))); } else { - assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")), rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width))); } @@ -370,12 +370,12 @@ struct SmvWorker if (cell->getParam("\\A_SIGNED").as_bool()) { - assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")), rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y)); } else { - assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")), rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y)); } @@ -407,7 +407,7 @@ struct SmvWorker expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width); } - assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")), expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y")))); continue; @@ -425,7 +425,7 @@ struct SmvWorker if (cell->type == "$reduce_or") expr = stringf("%s != 0ub%d_0", expr_a, width_a); if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a); - assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y)); + definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y)); continue; } @@ -444,7 +444,7 @@ struct SmvWorker if (cell->type == "$reduce_xnor") expr = "!(" + expr + ")"; - assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y)); + definitions.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y)); continue; } @@ -462,7 +462,7 @@ struct SmvWorker if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b; if (cell->type == "$logic_or") expr = expr_a + " | " + expr_b; - assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y)); + definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y)); continue; } @@ -474,7 +474,7 @@ struct SmvWorker string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a); const char *expr_y = lvalue(cell->getPort("\\Y")); - assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y)); + definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y)); continue; } @@ -490,12 +490,13 @@ struct SmvWorker expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width))); expr += rvalue(sig_a); - assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str())); + definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str())); continue; } if (cell->type == "$dff") { + vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort("\\Q")), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")))); assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D")))); continue; } @@ -503,7 +504,7 @@ struct SmvWorker if (cell->type.in("$_BUF_", "$_NOT_")) { string op = cell->type == "$_NOT_" ? "!" : ""; - assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A")))); + definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A")))); continue; } @@ -517,49 +518,49 @@ struct SmvWorker if (cell->type.in("$_XNOR_")) op = "xnor"; if (cell->type.in("$_ANDNOT_", "$_ORNOT_")) - assignments.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B")))); else if (cell->type.in("$_NAND_", "$_NOR_")) - assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B")))); else - assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B")))); continue; } if (cell->type == "$_MUX_") { - assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A")))); continue; } if (cell->type == "$_AOI3_") { - assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")))); continue; } if (cell->type == "$_OAI3_") { - assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")))); continue; } if (cell->type == "$_AOI4_") { - assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D")))); continue; } if (cell->type == "$_OAI4_") { - assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")), + definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")), rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D")))); continue; } @@ -567,13 +568,13 @@ struct SmvWorker if (cell->type[0] == '$') log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell)); - f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type)); +// f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type)); for (auto &conn : cell->connections()) if (cell->output(conn.first)) - assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first))); + definitions.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first))); else - assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second))); + definitions.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second))); } for (Wire *wire : partial_assignment_wires) @@ -657,7 +658,25 @@ struct SmvWorker } } - assignments.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str())); + definitions.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str())); + } + + if (!inputvars.empty()) { + f << stringf(" IVAR\n"); + for (const string &line : inputvars) + f << stringf(" %s\n", line.c_str()); + } + + if (!vars.empty()) { + f << stringf(" VAR\n"); + for (const string &line : vars) + f << stringf(" %s\n", line.c_str()); + } + + if (!definitions.empty()) { + f << stringf(" DEFINE\n"); + for (const string &line : definitions) + f << stringf(" %s\n", line.c_str()); } if (!assignments.empty()) { -- cgit v1.2.3 From 115ca576475a2e8d30e63b339ae6a1b5db6906a6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 5 Oct 2018 09:41:18 +0200 Subject: Add "write_edif -attrprop" Signed-off-by: Clifford Wolf --- backends/edif/edif.cc | 39 ++++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) (limited to 'backends') diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc index 5f9ec54fd..d4e56a9eb 100644 --- a/backends/edif/edif.cc +++ b/backends/edif/edif.cc @@ -106,6 +106,9 @@ struct EdifBackend : public Backend { log(" if the design contains constant nets. use \"hilomap\" to map to custom\n"); log(" constant drivers first)\n"); log("\n"); + log(" -attrprop\n"); + log(" create EDIF properties for cell attributes\n"); + log("\n"); log(" -pvector {par|bra|ang}\n"); log(" sets the delimiting character for module port rename clauses to\n"); log(" parentheses, square brackets, or angle brackets.\n"); @@ -121,6 +124,7 @@ struct EdifBackend : public Backend { log_header(design, "Executing EDIF backend.\n"); std::string top_module_name; bool port_rename = false; + bool attr_properties = false; std::map> lib_cell_ports; bool nogndvcc = false; CellTypes ct(design); @@ -137,6 +141,10 @@ struct EdifBackend : public Backend { nogndvcc = true; continue; } + if (args[argidx] == "-attrprop") { + attr_properties = true; + continue; + } if (args[argidx] == "-pvector" && argidx+1 < args.size()) { std::string parray; port_rename = true; @@ -332,24 +340,33 @@ struct EdifBackend : public Backend { *f << stringf(" (instance %s\n", EDIF_DEF(cell->name)); *f << stringf(" (viewRef VIEW_NETLIST (cellRef %s%s))", EDIF_REF(cell->type), lib_cell_ports.count(cell->type) > 0 ? " (libraryRef LIB)" : ""); - for (auto &p : cell->parameters) - if ((p.second.flags & RTLIL::CONST_FLAG_STRING) != 0) - *f << stringf("\n (property %s (string \"%s\"))", EDIF_DEF(p.first), p.second.decode_string().c_str()); - else if (p.second.bits.size() <= 32 && RTLIL::SigSpec(p.second).is_fully_def()) - *f << stringf("\n (property %s (integer %u))", EDIF_DEF(p.first), p.second.as_int()); + + auto add_prop = [&](IdString name, Const val) { + if ((val.flags & RTLIL::CONST_FLAG_STRING) != 0) + *f << stringf("\n (property %s (string \"%s\"))", EDIF_DEF(name), val.decode_string().c_str()); + else if (val.bits.size() <= 32 && RTLIL::SigSpec(val).is_fully_def()) + *f << stringf("\n (property %s (integer %u))", EDIF_DEF(name), val.as_int()); else { std::string hex_string = ""; - for (size_t i = 0; i < p.second.bits.size(); i += 4) { + for (size_t i = 0; i < val.bits.size(); i += 4) { int digit_value = 0; - if (i+0 < p.second.bits.size() && p.second.bits.at(i+0) == RTLIL::State::S1) digit_value |= 1; - if (i+1 < p.second.bits.size() && p.second.bits.at(i+1) == RTLIL::State::S1) digit_value |= 2; - if (i+2 < p.second.bits.size() && p.second.bits.at(i+2) == RTLIL::State::S1) digit_value |= 4; - if (i+3 < p.second.bits.size() && p.second.bits.at(i+3) == RTLIL::State::S1) digit_value |= 8; + if (i+0 < val.bits.size() && val.bits.at(i+0) == RTLIL::State::S1) digit_value |= 1; + if (i+1 < val.bits.size() && val.bits.at(i+1) == RTLIL::State::S1) digit_value |= 2; + if (i+2 < val.bits.size() && val.bits.at(i+2) == RTLIL::State::S1) digit_value |= 4; + if (i+3 < val.bits.size() && val.bits.at(i+3) == RTLIL::State::S1) digit_value |= 8; char digit_str[2] = { "0123456789abcdef"[digit_value], 0 }; hex_string = std::string(digit_str) + hex_string; } - *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(p.first), GetSize(p.second.bits), hex_string.c_str()); + *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(name), GetSize(val.bits), hex_string.c_str()); } + }; + + for (auto &p : cell->parameters) + add_prop(p.first, p.second); + if (attr_properties) + for (auto &p : cell->attributes) + add_prop(p.first, p.second); + *f << stringf(")\n"); for (auto &p : cell->connections()) { RTLIL::SigSpec sig = sigmap(p.second); -- cgit v1.2.3 From 749b3ed62a8665f756267fafd7520beb55570df5 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 15 Oct 2018 13:54:12 -0400 Subject: Minor update --- backends/smv/smv.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index a53ee7a7c..f379c9c48 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -232,7 +232,7 @@ struct SmvWorker SigSpec sig_a = cell->getPort("\\A"); SigSpec sig_en = cell->getPort("\\EN"); - invarspecs.push_back(stringf("(!bool(%s) | bool(%s));", rvalue(sig_en), rvalue(sig_a))); + invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a))); continue; } -- cgit v1.2.3 From 609f46eeb7b23fec2140dcfaaa5f3a8377153f43 Mon Sep 17 00:00:00 2001 From: rafaeltp Date: Thu, 18 Oct 2018 16:20:21 -0700 Subject: adding offset info to memories --- backends/verilog/verilog_backend.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index ae9031510..39683922f 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -388,7 +388,7 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire) void dump_memory(std::ostream &f, std::string indent, RTLIL::Memory *memory) { dump_attributes(f, indent, memory->attributes); - f << stringf("%s" "reg [%d:0] %s [%d:0];\n", indent.c_str(), memory->width-1, id(memory->name).c_str(), memory->size-1); + f << stringf("%s" "reg [%d:0] %s [%d:%d];\n", indent.c_str(), (memory->width-1), id(memory->name).c_str(), memory->size+memory->start_offset-1, memory->start_offset); } void dump_cell_expr_port(std::ostream &f, RTLIL::Cell *cell, std::string port, bool gen_signed = true) @@ -952,6 +952,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) std::string mem_id = id(cell->parameters["\\MEMID"].decode_string()); int abits = cell->parameters["\\ABITS"].as_int(); int size = cell->parameters["\\SIZE"].as_int(); + int offset = cell->parameters["\\OFFSET"].as_int(); int width = cell->parameters["\\WIDTH"].as_int(); bool use_init = !(RTLIL::SigSpec(cell->parameters["\\INIT"]).is_fully_undef()); @@ -960,7 +961,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) // initial begin // memid[0] = ... // end - f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size-1, 0); + f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size+offset-1, offset); if (use_init) { f << stringf("%s" "initial begin\n", indent.c_str()); -- cgit v1.2.3 From c7770d9eeaf9fba0c9d07e7cce020fe89ec71600 Mon Sep 17 00:00:00 2001 From: rafaeltp Date: Thu, 18 Oct 2018 16:22:33 -0700 Subject: adding offset info to memories --- backends/verilog/verilog_backend.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 39683922f..dde03f920 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -388,7 +388,7 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire) void dump_memory(std::ostream &f, std::string indent, RTLIL::Memory *memory) { dump_attributes(f, indent, memory->attributes); - f << stringf("%s" "reg [%d:0] %s [%d:%d];\n", indent.c_str(), (memory->width-1), id(memory->name).c_str(), memory->size+memory->start_offset-1, memory->start_offset); + f << stringf("%s" "reg [%d:0] %s [%d:%d];\n", indent.c_str(), memory->width-1, id(memory->name).c_str(), memory->size+memory->start_offset-1, memory->start_offset); } void dump_cell_expr_port(std::ostream &f, RTLIL::Cell *cell, std::string port, bool gen_signed = true) -- cgit v1.2.3 From b6781c6f4ba20ba14d1649a993fc09691921de2b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 1 Nov 2018 11:40:58 +0100 Subject: Add support for signed $shift/$shiftx in smt2 back-end Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e2777ae04..418f8d766 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -554,7 +554,9 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - /* FIXME */ + return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " + "(bvlshr A B) (bvlshr A (bvneg B)))", + GetSize(cell->getPort("\\B")), 0), 's'); } else { return export_bvop(cell, "(bvlshr A B)", 's'); } -- cgit v1.2.3 From d0acea4f2e6c98f09246584c2ac0903acc254093 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 4 Nov 2018 14:41:28 +0100 Subject: Add proper error message for when smtbmc "append" fails Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 6af2a5ac1..b944ee004 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1259,7 +1259,11 @@ elif covermode: smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") - assert smt_check_sat() == "sat" + if smt_check_sat() == "unsat": + print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + found_failed_assert = True + retstatus = False + break reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) assert len(reached_covers) == len(cover_desc) @@ -1377,7 +1381,11 @@ else: # not tempind, covermode smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) - assert smt_check_sat() == "sat" + print_msg("Re-solving with appended steps..") + if smt_check_sat() == "unsat": + print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + retstatus = False + break print_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) -- cgit v1.2.3 From 2b935421718c9a8d8f2183d9cb4a4973c078bcfa Mon Sep 17 00:00:00 2001 From: Arjen Roodselaar Date: Sun, 4 Nov 2018 21:58:09 -0800 Subject: Use conservative stack size for SMT2 on MacOS --- backends/smt2/smtio.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 3fc823e3e..e8ed5e63b 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -32,10 +32,15 @@ from threading import Thread if os.name == "posix": smtio_reclimit = 64 * 1024 smtio_stacksize = 128 * 1024 * 1024 + smtio_stacklimit = resource.RLIM_INFINITY + if os.uname().sysname == "Darwin": + # MacOS has rather conservative stack limits + smtio_stacksize = 16 * 1024 * 1024 + smtio_stacklimit = resource.getrlimit(resource.RLIMIT_STACK)[1] if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, smtio_stacklimit)) # currently running solvers (so we can kill them) -- cgit v1.2.3 From 79075d123f749ad39bf35f658f00a79a24efcf98 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Nov 2018 10:05:23 +0100 Subject: Improve stack rlimit code in smtio.py Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e8ed5e63b..e417b7758 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -31,16 +31,16 @@ from threading import Thread # does not run out of stack frames when parsing large expressions if os.name == "posix": smtio_reclimit = 64 * 1024 - smtio_stacksize = 128 * 1024 * 1024 - smtio_stacklimit = resource.RLIM_INFINITY - if os.uname().sysname == "Darwin": - # MacOS has rather conservative stack limits - smtio_stacksize = 16 * 1024 * 1024 - smtio_stacklimit = resource.getrlimit(resource.RLIMIT_STACK)[1] if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) - if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, smtio_stacklimit)) + + smtio_stacksize = 128 * 1024 * 1024 + current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) + if current_rlimit_stack[0] != resource.RLIM_INFINITY: + if current_rlimit_stack[1] != resource.RLIM_INFINITY: + smtio_stacksize = min(smtio_stacksize, smtio_stacklimit) + if current_rlimit_stack[0] < smtio_stacksize: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) # currently running solvers (so we can kill them) -- cgit v1.2.3 From 4c50e3abb9b39fe088cc0a08c63fcadb8abdabb7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Nov 2018 10:09:03 +0100 Subject: Fix for improved smtio.py rlimit code Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e417b7758..108f6bcfe 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -38,7 +38,7 @@ if os.name == "posix": current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) if current_rlimit_stack[0] != resource.RLIM_INFINITY: if current_rlimit_stack[1] != resource.RLIM_INFINITY: - smtio_stacksize = min(smtio_stacksize, smtio_stacklimit) + smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) if current_rlimit_stack[0] < smtio_stacksize: resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) -- cgit v1.2.3 From f6c4485a3ac315fbed76f1a2e1f22df7afb36886 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Nov 2018 11:11:05 +0100 Subject: Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e8ed5e63b..4c3245984 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -163,19 +163,28 @@ class SmtIo: self.unroll = False if self.solver == "yices": - self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['yices-smt2'] + self.solver_opts + else: + 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.noincr: + self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + else: + 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 + if self.noincr: + self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts + else: + self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts self.unroll = True if self.solver == "abc": -- cgit v1.2.3 From b54bf7c0f9720526dffce684ef1353b81f99547c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Nov 2018 15:32:34 +0100 Subject: Limit stack size to 16 MB on Darwin Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 108f6bcfe..afbcf1fc4 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -34,9 +34,12 @@ if os.name == "posix": if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) - smtio_stacksize = 128 * 1024 * 1024 current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) if current_rlimit_stack[0] != resource.RLIM_INFINITY: + smtio_stacksize = 128 * 1024 * 1024 + if os.uname().sysname == "Darwin": + # MacOS has rather conservative stack limits + smtio_stacksize = 16 * 1024 * 1024 if current_rlimit_stack[1] != resource.RLIM_INFINITY: smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) if current_rlimit_stack[0] < smtio_stacksize: -- cgit v1.2.3 From 82aaf6d9086176c746bb157f33fd085a2e03e461 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 12 Nov 2018 09:27:33 +0100 Subject: Add "write_aiger -I -O -B" Signed-off-by: Clifford Wolf --- backends/aiger/aiger.cc | 38 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) (limited to 'backends') diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index c323691a3..dfe506c66 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -100,7 +100,7 @@ struct AigerWriter return aig_map.at(bit); } - AigerWriter(Module *module, bool zinit_mode) : module(module), zinit_mode(zinit_mode), sigmap(module) + AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module) { pool undriven_bits; pool unused_bits; @@ -293,6 +293,10 @@ struct AigerWriter aig_map[bit] = 2*aig_m; } + if (imode && input_bits.empty()) { + aig_m++, aig_i++; + } + if (zinit_mode) { for (auto it : ff_map) { @@ -371,6 +375,11 @@ struct AigerWriter aig_outputs.push_back(bit2aig(bit)); } + if (omode && output_bits.empty()) { + aig_o++; + aig_outputs.push_back(0); + } + for (auto it : asserts) { aig_b++; int bit_a = bit2aig(it.first); @@ -378,6 +387,11 @@ struct AigerWriter aig_outputs.push_back(mkgate(bit_a^1, bit_en)); } + if (bmode && asserts.empty()) { + aig_b++; + aig_outputs.push_back(0); + } + for (auto it : assumes) { aig_c++; int bit_a = bit2aig(it.first); @@ -689,6 +703,11 @@ struct AigerBackend : public Backend { log(" -vmap \n"); log(" like -map, but more verbose\n"); log("\n"); + log(" -I, -O, -B\n"); + log(" If the design contains no input/output/assert then create one\n"); + log(" dummy input/output/bad_state pin to make the tools reading the\n"); + log(" AIGER file happy.\n"); + log("\n"); } void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) YS_OVERRIDE { @@ -697,6 +716,9 @@ struct AigerBackend : public Backend { bool miter_mode = false; bool symbols_mode = false; bool verbose_map = false; + bool imode = false; + bool omode = false; + bool bmode = false; std::string map_filename; log_header(design, "Executing AIGER backend.\n"); @@ -729,6 +751,18 @@ struct AigerBackend : public Backend { verbose_map = true; continue; } + if (args[argidx] == "-I") { + imode = true; + continue; + } + if (args[argidx] == "-O") { + omode = true; + continue; + } + if (args[argidx] == "-B") { + bmode = true; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -738,7 +772,7 @@ struct AigerBackend : public Backend { if (top_module == nullptr) log_error("Can't find top module in current design!\n"); - AigerWriter writer(top_module, zinit_mode); + AigerWriter writer(top_module, zinit_mode, imode, omode, bmode); writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode); if (!map_filename.empty()) { -- cgit v1.2.3 From 7fe770a441a129c509fd4da04b60ada942a28bc8 Mon Sep 17 00:00:00 2001 From: whitequark Date: Fri, 7 Dec 2018 18:48:06 +0000 Subject: write_verilog: correctly map RTLIL `sync init`. --- backends/verilog/verilog_backend.cc | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index dde03f920..922b4c44c 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -1352,6 +1352,8 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo if (sync->type == RTLIL::STa) { f << stringf("%s" "always @* begin\n", indent.c_str()); + } else if (sync->type == RTLIL::STi) { + f << stringf("%s" "initial begin\n", indent.c_str()); } else { f << stringf("%s" "always @(", indent.c_str()); if (sync->type == RTLIL::STp || sync->type == RTLIL::ST1) -- cgit v1.2.3 From ed3c57fad3616b981e54e2f209e7ee40ff87c8a7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 8 Dec 2018 06:21:31 +0100 Subject: Fix btor init value handling Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 58d2a8625..ab2702807 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -506,6 +506,18 @@ struct BtorWorker } } + Const initval; + for (int i = 0; i < GetSize(sig_q); i++) + if (initbits.count(sig_q[i])) + initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); + else + initval.bits.push_back(State::Sx); + + int nid_init_val = -1; + + if (!initval.is_fully_undef()) + nid_init_val = get_sig_nid(initval); + int sid = get_bv_sid(GetSize(sig_q)); int nid = next_nid++; @@ -514,15 +526,7 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(symbol)); - Const initval; - for (int i = 0; i < GetSize(sig_q); i++) - if (initbits.count(sig_q[i])) - initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); - else - initval.bits.push_back(State::Sx); - - if (!initval.is_fully_undef()) { - int nid_init_val = get_sig_nid(initval); + if (nid_init_val >= 0) { int nid_init = next_nid++; if (verbose) btorf("; initval = %s\n", log_signal(initval)); -- cgit v1.2.3 From 47a5dfdaa4bd7d400c6e3d58476de80904df460d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 8 Dec 2018 06:59:27 +0100 Subject: Add "yosys-smtbmc --btorwit" skeleton Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index b944ee004..57b50ccb6 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -32,6 +32,8 @@ cexfile = None aimfile = None aiwfile = None aigheader = True +btorfile = None +witfile = None vlogtbfile = None vlogtbtop = None inconstr = list() @@ -92,6 +94,10 @@ yosys-smtbmc [options] the AIGER witness file does not include the status and properties lines. + --btorwit + --btorwit : + read a BTOR file and a BTOR witness for that BTOR file. + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -152,7 +158,7 @@ yosys-smtbmc [options] try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat", + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat", "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "smtc-init", "smtc-top=", "noinit"]) except: @@ -189,6 +195,12 @@ for o, a in opts: aiwfile = a + ".aiw" elif o == "--aig-noheader": aigheader = False + elif o == "--btorwit": + if ":" in a: + btorfile, witfile = a.split(":") + else: + btorfile = a + ".btor" + witfile = a + ".wit" elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -575,6 +587,12 @@ if aimfile is not None: num_steps = max(num_steps, step+1) step += 1 +if btorfile is not None: + print("The --btorwit feature is not implemented yet") + smt.write("(exit)") + smt.wait() + sys.exit(1) + def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) print_msg("Writing trace to VCD file: %s" % (filename)) -- cgit v1.2.3 From 0b9bb852c66ec2a6e9b4b510b3e2e32b8c6a6b16 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 10 Dec 2018 03:43:07 +0100 Subject: Add yosys-smtbmc support for btor witness Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 115 +++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 100 insertions(+), 15 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 57b50ccb6..721a395e3 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -32,8 +32,7 @@ cexfile = None aimfile = None aiwfile = None aigheader = True -btorfile = None -witfile = None +btorwitfile = None vlogtbfile = None vlogtbtop = None inconstr = list() @@ -94,9 +93,8 @@ yosys-smtbmc [options] the AIGER witness file does not include the status and properties lines. - --btorwit - --btorwit : - read a BTOR file and a BTOR witness for that BTOR file. + --btorwit + read a BTOR witness. --noinfo only run the core proof, do not collect and print any @@ -196,11 +194,7 @@ for o, a in opts: elif o == "--aig-noheader": aigheader = False elif o == "--btorwit": - if ":" in a: - btorfile, witfile = a.split(":") - else: - btorfile = a + ".btor" - witfile = a + ".wit" + btorwitfile = a elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -587,11 +581,102 @@ if aimfile is not None: num_steps = max(num_steps, step+1) step += 1 -if btorfile is not None: - print("The --btorwit feature is not implemented yet") - smt.write("(exit)") - smt.wait() - sys.exit(1) +if btorwitfile is not None: + with open(btorwitfile, "r") as f: + step = None + suffix = None + altsuffix = None + header_okay = False + + for line in f: + line = line.strip() + + if line == "sat": + header_okay = True + continue + + if not header_okay: + continue + + if line == "" or line[0] == "b" or line[0] == "j": + continue + + if line == ".": + break + + if line[0] == '#' or line[0] == '@': + step = int(line[1:]) + suffix = line + altsuffix = suffix + if suffix[0] == "@": + altsuffix = "#" + suffix[1:] + else: + altsuffix = "@" + suffix[1:] + continue + + line = line.split() + + if len(line) == 0: + continue + + if line[-1].endswith(suffix): + line[-1] = line[-1][0:len(line[-1]) - len(suffix)] + + if line[-1].endswith(altsuffix): + line[-1] = line[-1][0:len(line[-1]) - len(altsuffix)] + + if line[-1][0] == "$": + continue + + # BV assignments + if len(line) == 3 and line[1][0] != "[": + value = line[1] + name = line[2] + + path = smt.get_path(topmod, name) + + if not smt.net_exists(topmod, path): + continue + + width = smt.net_width(topmod, path) + + if width == 1: + assert value in ["0", "1"] + value = "true" if value == "1" else "false" + else: + value = "#b" + value + + smtexpr = "(= [%s] %s)" % (name, value) + constr_assumes[step].append((btorwitfile, smtexpr)) + + # Array assignments + if len(line) == 4 and line[1][0] == "[": + index = line[1] + value = line[2] + name = line[3] + + path = smt.get_path(topmod, name) + + if not smt.mem_exists(topmod, path): + continue + + meminfo = smt.mem_info(topmod, path) + + if meminfo[1] == 1: + assert value in ["0", "1"] + value = "true" if value == "1" else "false" + else: + value = "#b" + value + + assert index[0] == "[" + assert index[-1] == "]" + index = "#b" + index[1:-1] + + smtexpr = "(= (select [%s] %s) %s)" % (name, index, value) + constr_assumes[step].append((btorwitfile, smtexpr)) + + skip_steps = step + num_steps = step+1 def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) -- cgit v1.2.3 From fccaa25ec1b053259a377991d8deba0f71021956 Mon Sep 17 00:00:00 2001 From: whitequark Date: Thu, 13 Dec 2018 04:36:02 +0000 Subject: write_verilog: add a missing newline. --- backends/verilog/verilog_backend.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index dde03f920..850abfad7 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -1419,7 +1419,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) log_warning("Module %s contains unmapped RTLIL proccesses. RTLIL processes\n" "can't always be mapped directly to Verilog always blocks. Unintended\n" "changes in simulation behavior are possible! Use \"proc\" to convert\n" - "processes to logic networks and registers.", log_id(module)); + "processes to logic networks and registers.\n", log_id(module)); f << stringf("\n"); for (auto it = module->processes.begin(); it != module->processes.end(); ++it) -- cgit v1.2.3 From ca866d384e666f27e2cd7bb80950d0a1dd7c0ebd Mon Sep 17 00:00:00 2001 From: whitequark Date: Sun, 16 Dec 2018 18:46:32 +0000 Subject: write_verilog: handle the $shift cell. The implementation corresponds to the following Verilog, which is lifted straight from simlib.v: module \\$shift (A, B, Y); parameter A_SIGNED = 0; parameter B_SIGNED = 0; parameter A_WIDTH = 0; parameter B_WIDTH = 0; parameter Y_WIDTH = 0; input [A_WIDTH-1:0] A; input [B_WIDTH-1:0] B; output [Y_WIDTH-1:0] Y; generate if (B_SIGNED) begin:BLOCK1 assign Y = $signed(B) < 0 ? A << -B : A >> B; end else begin:BLOCK2 assign Y = A >> B; end endgenerate endmodule --- backends/verilog/verilog_backend.cc | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) (limited to 'backends') diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 3a47b478f..71db25f98 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -678,6 +678,35 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) #undef HANDLE_UNIOP #undef HANDLE_BINOP + if (cell->type == "$shift") + { + f << stringf("%s" "assign ", indent.c_str()); + dump_sigspec(f, cell->getPort("\\Y")); + f << stringf(" = "); + if (cell->getParam("\\B_SIGNED").as_bool()) + { + f << stringf("$signed("); + dump_sigspec(f, cell->getPort("\\B")); + f << stringf(")"); + f << stringf(" < 0 ? "); + dump_sigspec(f, cell->getPort("\\A")); + f << stringf(" << - "); + dump_sigspec(f, cell->getPort("\\B")); + f << stringf(" : "); + dump_sigspec(f, cell->getPort("\\A")); + f << stringf(" >> "); + dump_sigspec(f, cell->getPort("\\B")); + } + else + { + dump_sigspec(f, cell->getPort("\\A")); + f << stringf(" >> "); + dump_sigspec(f, cell->getPort("\\B")); + } + f << stringf(";\n"); + return true; + } + if (cell->type == "$shiftx") { f << stringf("%s" "assign ", indent.c_str()); -- cgit v1.2.3 From abf5930a3325b8ae89f8cbb89a0f963e316c0889 Mon Sep 17 00:00:00 2001 From: makaimann Date: Mon, 5 Nov 2018 11:49:31 -0800 Subject: Add btor ops for $mul, $div, $mod and $concat --- backends/btor/btor.cc | 40 ++++++++++++++++++++++++++++++++++++++-- backends/btor/test_cells.sh | 0 2 files changed, 38 insertions(+), 2 deletions(-) mode change 100644 => 100755 backends/btor/test_cells.sh (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index ab2702807..d3fb9b858 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -133,12 +133,13 @@ struct BtorWorker cell_recursion_guard.insert(cell); btorf_push(log_id(cell)); - if (cell->type.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx", - "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) + if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx", + "$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) { string btor_op; if (cell->type == "$add") btor_op = "add"; if (cell->type == "$sub") btor_op = "sub"; + if (cell->type == "$mul") btor_op = "mul"; if (cell->type.in("$shl", "$sshl")) btor_op = "sll"; if (cell->type == "$shr") btor_op = "srl"; if (cell->type == "$sshr") btor_op = "sra"; @@ -146,6 +147,7 @@ struct BtorWorker if (cell->type.in("$and", "$_AND_")) btor_op = "and"; if (cell->type.in("$or", "$_OR_")) btor_op = "or"; if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor"; + if (cell->type == "$concat") btor_op = "concat"; if (cell->type == "$_NAND_") btor_op = "nand"; if (cell->type == "$_NOR_") btor_op = "nor"; if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor"; @@ -214,6 +216,40 @@ struct BtorWorker goto okay; } + if (cell->type.in("$div", "$mod")) + { + string btor_op; + if (cell->type == "$div") btor_op = "div"; + if (cell->type == "$mod") btor_op = "rem"; + log_assert(!btor_op.empty()); + + int width = GetSize(cell->getPort("\\Y")); + width = std::max(width, GetSize(cell->getPort("\\A"))); + width = std::max(width, GetSize(cell->getPort("\\B"))); + + bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; + bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false; + + int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); + int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + + int sid = get_bv_sid(width); + int nid = next_nid++; + btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b); + + SigSpec sig = sigmap(cell->getPort("\\Y")); + + if (GetSize(sig) < width) { + int sid = get_bv_sid(GetSize(sig)); + int nid2 = next_nid++; + btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1); + nid = nid2; + } + + add_nid_sig(nid, sig); + goto okay; + } + if (cell->type.in("$_ANDNOT_", "$_ORNOT_")) { int sid = get_bv_sid(1); diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh old mode 100644 new mode 100755 -- cgit v1.2.3