summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/aiger.cc42
-rw-r--r--backends/blif/blif.cc32
-rw-r--r--backends/btor/btor.cc158
-rw-r--r--backends/edif/edif.cc63
-rw-r--r--backends/firrtl/firrtl.cc531
-rw-r--r--backends/ilang/ilang_backend.cc13
-rw-r--r--backends/intersynth/intersynth.cc2
-rw-r--r--backends/json/json.cc9
-rw-r--r--backends/protobuf/protobuf.cc7
-rw-r--r--backends/simplec/test00_uut.v6
-rw-r--r--backends/smt2/Makefile.inc18
-rw-r--r--backends/smt2/smt2.cc26
-rw-r--r--backends/smt2/smtbmc.py125
-rw-r--r--backends/smt2/smtio.py38
-rw-r--r--backends/smv/smv.cc85
-rw-r--r--backends/spice/spice.cc2
-rw-r--r--backends/table/table.cc2
-rw-r--r--backends/verilog/verilog_backend.cc341
18 files changed, 1236 insertions, 264 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index c323691a..6863b40f 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -89,7 +89,8 @@ struct AigerWriter
aig_map[bit] = mkgate(a0, a1);
} else
if (alias_map.count(bit)) {
- aig_map[bit] = bit2aig(alias_map.at(bit));
+ int a = bit2aig(alias_map.at(bit));
+ aig_map[bit] = a;
}
if (bit == State::Sx || bit == State::Sz)
@@ -100,7 +101,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<SigBit> undriven_bits;
pool<SigBit> unused_bits;
@@ -293,6 +294,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 +376,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 +388,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 +704,11 @@ struct AigerBackend : public Backend {
log(" -vmap <filename>\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<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
@@ -697,6 +717,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 +752,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,10 +773,11 @@ 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()) {
+ rewrite_filename(filename);
std::ofstream mapf;
mapf.open(map_filename.c_str(), std::ofstream::trunc);
if (mapf.fail())
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index 0db5ff27..a1761b66 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -140,7 +140,7 @@ struct BlifDumper
return "subckt";
if (!design->modules_.count(RTLIL::escape_id(cell_type)))
return "gate";
- if (design->modules_.at(RTLIL::escape_id(cell_type))->get_bool_attribute("\\blackbox"))
+ if (design->modules_.at(RTLIL::escape_id(cell_type))->get_blackbox_attribute())
return "gate";
return "subckt";
}
@@ -196,7 +196,7 @@ struct BlifDumper
}
f << stringf("\n");
- if (module->get_bool_attribute("\\blackbox")) {
+ if (module->get_blackbox_attribute()) {
f << stringf(".blackbox\n");
f << stringf(".end\n");
return;
@@ -409,12 +409,26 @@ struct BlifDumper
f << stringf(".%s %s", subckt_or_gate(cell->type.str()), cstr(cell->type));
for (auto &conn : cell->connections())
- for (int i = 0; i < conn.second.size(); i++) {
- if (conn.second.size() == 1)
- f << stringf(" %s", cstr(conn.first));
- else
- f << stringf(" %s[%d]", cstr(conn.first), i);
- f << stringf("=%s", cstr(conn.second.extract(i, 1)));
+ {
+ if (conn.second.size() == 1) {
+ f << stringf(" %s=%s", cstr(conn.first), cstr(conn.second[0]));
+ continue;
+ }
+
+ Module *m = design->module(cell->type);
+ Wire *w = m ? m->wire(conn.first) : nullptr;
+
+ if (w == nullptr) {
+ for (int i = 0; i < GetSize(conn.second); i++)
+ f << stringf(" %s[%d]=%s", cstr(conn.first), i, cstr(conn.second[i]));
+ } else {
+ for (int i = 0; i < std::min(GetSize(conn.second), GetSize(w)); i++) {
+ SigBit sig(w, i);
+ f << stringf(" %s[%d]=%s", cstr(conn.first), sig.wire->upto ?
+ sig.wire->start_offset+sig.wire->width-sig.offset-1 :
+ sig.wire->start_offset+sig.offset, cstr(conn.second[i]));
+ }
+ }
}
f << stringf("\n");
@@ -640,7 +654,7 @@ struct BlifBackend : public Backend {
for (auto module_it : design->modules_)
{
RTLIL::Module *module = module_it.second;
- if (module->get_bool_attribute("\\blackbox") && !config.blackbox_mode)
+ if (module->get_blackbox_attribute() && !config.blackbox_mode)
continue;
if (module->processes.size() != 0)
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 58d2a862..a507b120 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -17,6 +17,11 @@
*
*/
+// [[CITE]] Btor2 , BtorMC and Boolector 3.0
+// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
+// Computer Aided Verification - 30th International Conference, CAV 2018
+// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
+
#include "kernel/rtlil.h"
#include "kernel/register.h"
#include "kernel/sigtools.h"
@@ -129,16 +134,23 @@ struct BtorWorker
void export_cell(Cell *cell)
{
- log_assert(cell_recursion_guard.count(cell) == 0);
+ if (cell_recursion_guard.count(cell)) {
+ string cell_list;
+ for (auto c : cell_recursion_guard)
+ cell_list += stringf("\n %s", log_id(c));
+ log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell), cell_list.c_str());
+ }
+
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 +158,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 +227,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);
@@ -304,7 +351,7 @@ struct BtorWorker
if (cell->type == "$lt") btor_op = "lt";
if (cell->type == "$le") btor_op = "lte";
if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
- if (cell->type.in("$ne", "$nex")) btor_op = "ne";
+ if (cell->type.in("$ne", "$nex")) btor_op = "neq";
if (cell->type == "$ge") btor_op = "gte";
if (cell->type == "$gt") btor_op = "gt";
log_assert(!btor_op.empty());
@@ -506,6 +553,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 +573,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));
@@ -575,6 +626,7 @@ struct BtorWorker
{
int abits = cell->getParam("\\ABITS").as_int();
int width = cell->getParam("\\WIDTH").as_int();
+ int nwords = cell->getParam("\\SIZE").as_int();
int rdports = cell->getParam("\\RD_PORTS").as_int();
int wrports = cell->getParam("\\WR_PORTS").as_int();
@@ -601,6 +653,52 @@ struct BtorWorker
int data_sid = get_bv_sid(width);
int bool_sid = get_bv_sid(1);
int sid = get_mem_sid(abits, width);
+
+ Const initdata = cell->getParam("\\INIT");
+ initdata.exts(nwords*width);
+ int nid_init_val = -1;
+
+ if (!initdata.is_fully_undef())
+ {
+ bool constword = true;
+ Const firstword = initdata.extract(0, width);
+
+ for (int i = 1; i < nwords; i++) {
+ Const thisword = initdata.extract(i*width, width);
+ if (thisword != firstword) {
+ constword = false;
+ break;
+ }
+ }
+
+ if (constword)
+ {
+ if (verbose)
+ btorf("; initval = %s\n", log_signal(firstword));
+ nid_init_val = get_sig_nid(firstword);
+ }
+ else
+ {
+ int nid_init_val = next_nid++;
+ btorf("%d state %d\n", nid_init_val, sid);
+
+ for (int i = 0; i < nwords; i++) {
+ Const thisword = initdata.extract(i*width, width);
+ if (thisword.is_fully_undef())
+ continue;
+ Const thisaddr(i, abits);
+ int nid_thisword = get_sig_nid(thisword);
+ int nid_thisaddr = get_sig_nid(thisaddr);
+ int last_nid_init_val = nid_init_val;
+ nid_init_val = next_nid++;
+ if (verbose)
+ btorf("; initval[%d] = %s\n", i, log_signal(thisword));
+ btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword);
+ }
+ }
+ }
+
+
int nid = next_nid++;
int nid_head = nid;
@@ -609,6 +707,12 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(cell));
+ if (nid_init_val >= 0)
+ {
+ int nid_init = next_nid++;
+ btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
+ }
+
if (asyncwr)
{
for (int port = 0; port < wrports; port++)
@@ -776,9 +880,28 @@ struct BtorWorker
else
{
if (bit_cell.count(bit) == 0)
- log_error("No driver for signal bit %s.\n", log_signal(bit));
- export_cell(bit_cell.at(bit));
- log_assert(bit_nid.count(bit));
+ {
+ SigSpec s = bit;
+
+ while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
+ bit_cell.count(sig[i+GetSize(s)]) == 0)
+ s.append(sig[i+GetSize(s)]);
+
+ log_warning("No driver for signal %s.\n", log_signal(s));
+
+ int sid = get_bv_sid(GetSize(s));
+ int nid = next_nid++;
+ btorf("%d input %d %s\n", nid, sid);
+ nid_width[nid] = GetSize(s);
+
+ i += GetSize(s)-1;
+ continue;
+ }
+ else
+ {
+ export_cell(bit_cell.at(bit));
+ log_assert(bit_nid.count(bit));
+ }
}
}
@@ -892,9 +1015,8 @@ struct BtorWorker
btorf_push(stringf("output %s", log_id(wire)));
- int sid = get_bv_sid(GetSize(wire));
int nid = get_sig_nid(wire);
- btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
+ btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
btorf_pop(stringf("output %s", log_id(wire)));
}
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 5f9ec54f..6d946953 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -106,6 +106,13 @@ 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(" -gndvccy\n");
+ log(" create \"GND\" and \"VCC\" cells with \"Y\" outputs. (the default is \"G\"\n");
+ log(" for \"GND\" and \"P\" for \"VCC\".)\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,8 +128,9 @@ 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<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
- bool nogndvcc = false;
+ bool nogndvcc = false, gndvccy = false;
CellTypes ct(design);
EdifNames edif_names;
@@ -137,6 +145,14 @@ struct EdifBackend : public Backend {
nogndvcc = true;
continue;
}
+ if (args[argidx] == "-gndvccy") {
+ gndvccy = true;
+ continue;
+ }
+ if (args[argidx] == "-attrprop") {
+ attr_properties = true;
+ continue;
+ }
if (args[argidx] == "-pvector" && argidx+1 < args.size()) {
std::string parray;
port_rename = true;
@@ -162,7 +178,7 @@ struct EdifBackend : public Backend {
for (auto module_it : design->modules_)
{
RTLIL::Module *module = module_it.second;
- if (module->get_bool_attribute("\\blackbox"))
+ if (module->get_blackbox_attribute())
continue;
if (top_module_name.empty())
@@ -176,7 +192,7 @@ struct EdifBackend : public Backend {
for (auto cell_it : module->cells_)
{
RTLIL::Cell *cell = cell_it.second;
- if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_bool_attribute("\\blackbox")) {
+ if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_blackbox_attribute()) {
lib_cell_ports[cell->type];
for (auto p : cell->connections())
lib_cell_ports[cell->type][p.first] = GetSize(p.second);
@@ -203,7 +219,7 @@ struct EdifBackend : public Backend {
*f << stringf(" (cellType GENERIC)\n");
*f << stringf(" (view VIEW_NETLIST\n");
*f << stringf(" (viewType NETLIST)\n");
- *f << stringf(" (interface (port G (direction OUTPUT)))\n");
+ *f << stringf(" (interface (port %c (direction OUTPUT)))\n", gndvccy ? 'Y' : 'G');
*f << stringf(" )\n");
*f << stringf(" )\n");
@@ -211,7 +227,7 @@ struct EdifBackend : public Backend {
*f << stringf(" (cellType GENERIC)\n");
*f << stringf(" (view VIEW_NETLIST\n");
*f << stringf(" (viewType NETLIST)\n");
- *f << stringf(" (interface (port P (direction OUTPUT)))\n");
+ *f << stringf(" (interface (port %c (direction OUTPUT)))\n", gndvccy ? 'Y' : 'P');
*f << stringf(" )\n");
*f << stringf(" )\n");
}
@@ -286,7 +302,7 @@ struct EdifBackend : public Backend {
*f << stringf(" (technology (numberDefinition))\n");
for (auto module : sorted_modules)
{
- if (module->get_bool_attribute("\\blackbox"))
+ if (module->get_blackbox_attribute())
continue;
SigMap sigmap(module);
@@ -332,24 +348,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);
@@ -403,9 +428,9 @@ struct EdifBackend : public Backend {
if (nogndvcc)
log_error("Design contains constant nodes (map with \"hilomap\" first).\n");
if (sig == RTLIL::State::S0)
- *f << stringf(" (portRef G (instanceRef GND))\n");
+ *f << stringf(" (portRef %c (instanceRef GND))\n", gndvccy ? 'Y' : 'G');
if (sig == RTLIL::State::S1)
- *f << stringf(" (portRef P (instanceRef VCC))\n");
+ *f << stringf(" (portRef %c (instanceRef VCC))\n", gndvccy ? 'Y' : 'P');
}
*f << stringf(" ))\n");
}
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 32410a65..1c7a7351 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -23,7 +23,11 @@
#include "kernel/celltypes.h"
#include "kernel/cellaigs.h"
#include "kernel/log.h"
+#include <algorithm>
#include <string>
+#include <regex>
+#include <vector>
+#include <cmath>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -37,6 +41,7 @@ static const FDirection FD_NODIRECTION = 0x0;
static const FDirection FD_IN = 0x1;
static const FDirection FD_OUT = 0x2;
static const FDirection FD_INOUT = 0x3;
+static const int FIRRTL_MAX_DSH_WIDTH_ERROR = 20; // For historic reasons, this is actually one greater than the maximum allowed shift width
// Get a port direction with respect to a specific module.
FDirection getPortFDirection(IdString id, Module *module)
@@ -101,6 +106,125 @@ struct FirrtlWorker
RTLIL::Design *design;
std::string indent;
+ // Define read/write ports and memories.
+ // We'll collect their definitions and emit the corresponding FIRRTL definitions at the appropriate point in module construction.
+ // For the moment, we don't handle $readmemh or $readmemb.
+ // These will be part of a subsequent PR.
+ struct read_port {
+ string name;
+ bool clk_enable;
+ bool clk_parity;
+ bool transparent;
+ RTLIL::SigSpec clk;
+ RTLIL::SigSpec ena;
+ RTLIL::SigSpec addr;
+ read_port(string name, bool clk_enable, bool clk_parity, bool transparent, RTLIL::SigSpec clk, RTLIL::SigSpec ena, RTLIL::SigSpec addr) : name(name), clk_enable(clk_enable), clk_parity(clk_parity), transparent(transparent), clk(clk), ena(ena), addr(addr) {
+ // Current (3/13/2019) conventions:
+ // generate a constant 0 for clock and a constant 1 for enable if they are undefined.
+ if (!clk.is_fully_def())
+ this->clk = SigSpec(RTLIL::Const(0, 1));
+ if (!ena.is_fully_def())
+ this->ena = SigSpec(RTLIL::Const(1, 1));
+ }
+ string gen_read(const char * indent) {
+ string addr_expr = make_expr(addr);
+ string ena_expr = make_expr(ena);
+ string clk_expr = make_expr(clk);
+ string addr_str = stringf("%s%s.addr <= %s\n", indent, name.c_str(), addr_expr.c_str());
+ string ena_str = stringf("%s%s.en <= %s\n", indent, name.c_str(), ena_expr.c_str());
+ string clk_str = stringf("%s%s.clk <= asClock(%s)\n", indent, name.c_str(), clk_expr.c_str());
+ return addr_str + ena_str + clk_str;
+ }
+ };
+ struct write_port : read_port {
+ RTLIL::SigSpec mask;
+ write_port(string name, bool clk_enable, bool clk_parity, bool transparent, RTLIL::SigSpec clk, RTLIL::SigSpec ena, RTLIL::SigSpec addr, RTLIL::SigSpec mask) : read_port(name, clk_enable, clk_parity, transparent, clk, ena, addr), mask(mask) {
+ if (!clk.is_fully_def())
+ this->clk = SigSpec(RTLIL::Const(0));
+ if (!ena.is_fully_def())
+ this->ena = SigSpec(RTLIL::Const(0));
+ if (!mask.is_fully_def())
+ this->ena = SigSpec(RTLIL::Const(1));
+ }
+ string gen_read(const char * /* indent */) {
+ log_error("gen_read called on write_port: %s\n", name.c_str());
+ return stringf("gen_read called on write_port: %s\n", name.c_str());
+ }
+ string gen_write(const char * indent) {
+ string addr_expr = make_expr(addr);
+ string ena_expr = make_expr(ena);
+ string clk_expr = make_expr(clk);
+ string mask_expr = make_expr(mask);
+ string mask_str = stringf("%s%s.mask <= %s\n", indent, name.c_str(), mask_expr.c_str());
+ string addr_str = stringf("%s%s.addr <= %s\n", indent, name.c_str(), addr_expr.c_str());
+ string ena_str = stringf("%s%s.en <= %s\n", indent, name.c_str(), ena_expr.c_str());
+ string clk_str = stringf("%s%s.clk <= asClock(%s)\n", indent, name.c_str(), clk_expr.c_str());
+ return addr_str + ena_str + clk_str + mask_str;
+ }
+ };
+ /* Memories defined within this module. */
+ struct memory {
+ Cell *pCell; // for error reporting
+ string name; // memory name
+ int abits; // number of address bits
+ int size; // size (in units) of the memory
+ int width; // size (in bits) of each element
+ int read_latency;
+ int write_latency;
+ vector<read_port> read_ports;
+ vector<write_port> write_ports;
+ std::string init_file;
+ std::string init_file_srcFileSpec;
+ string srcLine;
+ memory(Cell *pCell, string name, int abits, int size, int width) : pCell(pCell), name(name), abits(abits), size(size), width(width), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec("") {
+ // Provide defaults for abits or size if one (but not the other) is specified.
+ if (this->abits == 0 && this->size != 0) {
+ this->abits = ceil_log2(this->size);
+ } else if (this->abits != 0 && this->size == 0) {
+ this->size = 1 << this->abits;
+ }
+ // Sanity-check this construction.
+ if (this->name == "") {
+ log_error("Nameless memory%s\n", this->atLine());
+ }
+ if (this->abits == 0 && this->size == 0) {
+ log_error("Memory %s has zero address bits and size%s\n", this->name.c_str(), this->atLine());
+ }
+ if (this->width == 0) {
+ log_error("Memory %s has zero width%s\n", this->name.c_str(), this->atLine());
+ }
+ }
+ // We need a default constructor for the dict insert.
+ memory() : pCell(0), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec(""){}
+
+ const char *atLine() {
+ if (srcLine == "") {
+ if (pCell) {
+ auto p = pCell->attributes.find("\\src");
+ srcLine = " at " + p->second.decode_string();
+ }
+ }
+ return srcLine.c_str();
+ }
+ void add_memory_read_port(read_port &rp) {
+ read_ports.push_back(rp);
+ }
+ void add_memory_write_port(write_port &wp) {
+ write_ports.push_back(wp);
+ }
+ void add_memory_file(std::string init_file, std::string init_file_srcFileSpec) {
+ this->init_file = init_file;
+ this->init_file_srcFileSpec = init_file_srcFileSpec;
+ }
+
+ };
+ dict<string, memory> memories;
+
+ void register_memory(memory &m)
+ {
+ memories[m.name] = m;
+ }
+
void register_reverse_wire_map(string id, SigSpec sig)
{
for (int i = 0; i < GetSize(sig); i++)
@@ -111,7 +235,7 @@ struct FirrtlWorker
{
}
- string make_expr(const SigSpec &sig)
+ static string make_expr(const SigSpec &sig)
{
string expr;
@@ -160,11 +284,9 @@ struct FirrtlWorker
std::string fid(RTLIL::IdString internal_id)
{
- const char *str = internal_id.c_str();
- return *str == '\\' ? str + 1 : str;
+ return make_id(internal_id);
}
-
std::string cellname(RTLIL::Cell *cell)
{
return fid(cell->name).c_str();
@@ -173,6 +295,26 @@ struct FirrtlWorker
void process_instance(RTLIL::Cell *cell, vector<string> &wire_exprs)
{
std::string cell_type = fid(cell->type);
+ std::string instanceOf;
+ // If this is a parameterized module, its parent module is encoded in the cell type
+ if (cell->type.substr(0, 8) == "$paramod")
+ {
+ std::string::iterator it;
+ for (it = cell_type.begin(); it < cell_type.end(); it++)
+ {
+ switch (*it) {
+ case '\\': /* FALL_THROUGH */
+ case '=': /* FALL_THROUGH */
+ case '\'': /* FALL_THROUGH */
+ case '$': instanceOf.append("_"); break;
+ default: instanceOf.append(1, *it); break;
+ }
+ }
+ }
+ else
+ {
+ instanceOf = cell_type;
+ }
std::string cell_name = cellname(cell);
std::string cell_name_comment;
@@ -182,41 +324,75 @@ struct FirrtlWorker
cell_name_comment = "";
// Find the module corresponding to this instance.
auto instModule = design->module(cell->type);
- wire_exprs.push_back(stringf("%s" "inst %s%s of %s", indent.c_str(), cell_name.c_str(), cell_name_comment.c_str(), cell_type.c_str()));
+ // If there is no instance for this, just return.
+ if (instModule == NULL)
+ {
+ log_warning("No instance for %s.%s\n", cell_type.c_str(), cell_name.c_str());
+ return;
+ }
+ wire_exprs.push_back(stringf("%s" "inst %s%s of %s", indent.c_str(), cell_name.c_str(), cell_name_comment.c_str(), instanceOf.c_str()));
for (auto it = cell->connections().begin(); it != cell->connections().end(); ++it) {
if (it->second.size() > 0) {
const SigSpec &secondSig = it->second;
const std::string firstName = cell_name + "." + make_id(it->first);
- const std::string secondName = make_expr(secondSig);
+ const std::string secondExpr = make_expr(secondSig);
// Find the direction for this port.
FDirection dir = getPortFDirection(it->first, instModule);
- std::string source, sink;
+ std::string sourceExpr, sinkExpr;
+ const SigSpec *sinkSig = nullptr;
switch (dir) {
case FD_INOUT:
- log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", log_id(cell_type), log_signal(it->second));
+ log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", cell_type.c_str(), log_signal(it->second));
+ /* FALLTHRU */
case FD_OUT:
- source = firstName;
- sink = secondName;
+ sourceExpr = firstName;
+ sinkExpr = secondExpr;
+ sinkSig = &secondSig;
break;
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 */
+ log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", cell_type.c_str(), log_signal(it->second));
+ /* FALLTHRU */
case FD_IN:
- source = secondName;
- sink = firstName;
+ sourceExpr = secondExpr;
+ sinkExpr = firstName;
break;
default:
- log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", log_id(cell_type), log_signal(it->second), dir);
+ log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", cell_type.c_str(), log_signal(it->second), dir);
break;
}
- wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sink.c_str(), source.c_str()));
+ // Check for subfield assignment.
+ std::string bitsString = "bits(";
+ if (sinkExpr.substr(0, bitsString.length()) == bitsString ) {
+ if (sinkSig == nullptr)
+ log_error("Unknown subfield %s.%s\n", cell_type.c_str(), sinkExpr.c_str());
+ // Don't generate the assignment here.
+ // Add the source and sink to the "reverse_wire_map" and we'll output the assignment
+ // as part of the coalesced subfield assignments for this wire.
+ register_reverse_wire_map(sourceExpr, *sinkSig);
+ } else {
+ wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sinkExpr.c_str(), sourceExpr.c_str()));
+ }
}
}
wire_exprs.push_back(stringf("\n"));
}
+ // Given an expression for a shift amount, and a maximum width,
+ // generate the FIRRTL expression for equivalent dynamic shift taking into account FIRRTL shift semantics.
+ std::string gen_dshl(const string b_expr, const int b_padded_width)
+ {
+ string result = b_expr;
+ if (b_padded_width >= FIRRTL_MAX_DSH_WIDTH_ERROR) {
+ int max_shift_width_bits = FIRRTL_MAX_DSH_WIDTH_ERROR - 1;
+ string max_shift_string = stringf("UInt<%d>(%d)", max_shift_width_bits, (1<<max_shift_width_bits) - 1);
+ // Deal with the difference in semantics between FIRRTL and verilog
+ result = stringf("mux(gt(%s, %s), %s, bits(%s, %d, 0))", b_expr.c_str(), max_shift_string.c_str(), max_shift_string.c_str(), b_expr.c_str(), max_shift_width_bits - 1);
+ }
+ return result;
+ }
+
void run()
{
f << stringf(" module %s:\n", make_id(module->name));
@@ -225,6 +401,12 @@ struct FirrtlWorker
for (auto wire : module->wires())
{
const auto wireName = make_id(wire->name);
+ // If a wire has initial data, issue a warning since FIRRTL doesn't currently support it.
+ if (wire->attributes.count("\\init")) {
+ log_warning("Initial value (%s) for (%s.%s) not supported\n",
+ wire->attributes.at("\\init").as_string().c_str(),
+ log_id(module), log_id(wire));
+ }
if (wire->port_id)
{
if (wire->port_input && wire->port_output)
@@ -240,7 +422,8 @@ struct FirrtlWorker
for (auto cell : module->cells())
{
- // Is this cell is a module instance?
+ bool extract_y_bits = false; // Assume no extraction of final bits will be required.
+ // Is this cell is a module instance?
if (cell->type[0] != '$')
{
process_instance(cell, wire_exprs);
@@ -264,21 +447,23 @@ struct FirrtlWorker
}
string primop;
- bool always_uint = false;
+ bool always_uint = false;
if (cell->type == "$not") primop = "not";
- if (cell->type == "$neg") primop = "neg";
- if (cell->type == "$logic_not") {
+ else if (cell->type == "$neg") {
+ primop = "neg";
+ is_signed = true; // Result of "neg" is signed (an SInt).
+ } else if (cell->type == "$logic_not") {
primop = "eq";
a_expr = stringf("%s, UInt(0)", a_expr.c_str());
}
- if (cell->type == "$reduce_and") primop = "andr";
- if (cell->type == "$reduce_or") primop = "orr";
- if (cell->type == "$reduce_xor") primop = "xorr";
- if (cell->type == "$reduce_xnor") {
+ else if (cell->type == "$reduce_and") primop = "andr";
+ else if (cell->type == "$reduce_or") primop = "orr";
+ else if (cell->type == "$reduce_xor") primop = "xorr";
+ else if (cell->type == "$reduce_xnor") {
primop = "not";
a_expr = stringf("xorr(%s)", a_expr.c_str());
}
- if (cell->type == "$reduce_bool") {
+ else if (cell->type == "$reduce_bool") {
primop = "neq";
// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
bool a_signed = cell->parameters.at("\\A_SIGNED").as_bool();
@@ -297,14 +482,15 @@ struct FirrtlWorker
continue;
}
if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$and", "$or", "$eq", "$eqx",
- "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
- "$logic_and", "$logic_or"))
+ "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
+ "$logic_and", "$logic_or"))
{
string y_id = make_id(cell->name);
bool is_signed = cell->parameters.at("\\A_SIGNED").as_bool();
int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
string b_expr = make_expr(cell->getPort("\\B"));
+ int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
if (cell->parameters.at("\\A_SIGNED").as_bool()) {
@@ -315,67 +501,95 @@ struct FirrtlWorker
if (cell->parameters.at("\\B_SIGNED").as_bool()) {
b_expr = "asSInt(" + b_expr + ")";
}
- b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+ if (b_padded_width < y_width) {
+ auto b_sig = cell->getPort("\\B");
+ b_padded_width = y_width;
+ }
}
- a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ auto a_sig = cell->getPort("\\A");
if (cell->parameters.at("\\A_SIGNED").as_bool() & (cell->type == "$shr")) {
a_expr = "asUInt(" + a_expr + ")";
}
string primop;
- bool always_uint = false;
+ bool always_uint = false;
if (cell->type == "$add") primop = "add";
- if (cell->type == "$sub") primop = "sub";
- if (cell->type == "$mul") primop = "mul";
- if (cell->type == "$div") primop = "div";
- if (cell->type == "$mod") primop = "rem";
- if (cell->type == "$and") {
+ else if (cell->type == "$sub") primop = "sub";
+ else if (cell->type == "$mul") primop = "mul";
+ else if (cell->type == "$div") primop = "div";
+ else if (cell->type == "$mod") primop = "rem";
+ else if (cell->type == "$and") {
primop = "and";
always_uint = true;
}
- if (cell->type == "$or" ) {
+ else if (cell->type == "$or" ) {
primop = "or";
always_uint = true;
}
- if (cell->type == "$xor") {
+ else if (cell->type == "$xor") {
primop = "xor";
always_uint = true;
}
- if ((cell->type == "$eq") | (cell->type == "$eqx")) {
+ else if ((cell->type == "$eq") | (cell->type == "$eqx")) {
primop = "eq";
always_uint = true;
}
- if ((cell->type == "$ne") | (cell->type == "$nex")) {
+ else if ((cell->type == "$ne") | (cell->type == "$nex")) {
primop = "neq";
always_uint = true;
}
- if (cell->type == "$gt") {
+ else if (cell->type == "$gt") {
primop = "gt";
always_uint = true;
}
- if (cell->type == "$ge") {
+ else if (cell->type == "$ge") {
primop = "geq";
always_uint = true;
}
- if (cell->type == "$lt") {
+ else if (cell->type == "$lt") {
primop = "lt";
always_uint = true;
}
- if (cell->type == "$le") {
+ else if (cell->type == "$le") {
primop = "leq";
always_uint = true;
}
- if ((cell->type == "$shl") | (cell->type == "$sshl")) primop = "dshl";
- if ((cell->type == "$shr") | (cell->type == "$sshr")) primop = "dshr";
- if ((cell->type == "$logic_and")) {
+ else if ((cell->type == "$shl") | (cell->type == "$sshl")) {
+ // FIRRTL will widen the result (y) by the amount of the shift.
+ // We'll need to offset this by extracting the un-widened portion as Verilog would do.
+ extract_y_bits = true;
+ // Is the shift amount constant?
+ auto b_sig = cell->getPort("\\B");
+ if (b_sig.is_fully_const()) {
+ primop = "shl";
+ b_expr = std::to_string(b_sig.as_int());
+ } else {
+ primop = "dshl";
+ // Convert from FIRRTL left shift semantics.
+ b_expr = gen_dshl(b_expr, b_padded_width);
+ }
+ }
+ else if ((cell->type == "$shr") | (cell->type == "$sshr")) {
+ // We don't need to extract a specific range of bits.
+ extract_y_bits = false;
+ // Is the shift amount constant?
+ auto b_sig = cell->getPort("\\B");
+ if (b_sig.is_fully_const()) {
+ primop = "shr";
+ b_expr = std::to_string(b_sig.as_int());
+ } else {
+ primop = "dshr";
+ }
+ }
+ else if ((cell->type == "$logic_and")) {
primop = "and";
a_expr = "neq(" + a_expr + ", UInt(0))";
b_expr = "neq(" + b_expr + ", UInt(0))";
always_uint = true;
}
- if ((cell->type == "$logic_or")) {
+ else if ((cell->type == "$logic_or")) {
primop = "or";
a_expr = "neq(" + a_expr + ", UInt(0))";
b_expr = "neq(" + b_expr + ", UInt(0))";
@@ -388,6 +602,11 @@ struct FirrtlWorker
string expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+ // Deal with FIRRTL's "shift widens" semantics
+ if (extract_y_bits) {
+ expr = stringf("bits(%s, %d, 0)", expr.c_str(), y_width - 1);
+ }
+
if ((is_signed && !always_uint) || cell->type.in("$sub"))
expr = stringf("asUInt(%s)", expr.c_str());
@@ -420,6 +639,7 @@ struct FirrtlWorker
int abits = cell->parameters.at("\\ABITS").as_int();
int width = cell->parameters.at("\\WIDTH").as_int();
int size = cell->parameters.at("\\SIZE").as_int();
+ memory m(cell, mem_id, abits, size, width);
int rd_ports = cell->parameters.at("\\RD_PORTS").as_int();
int wr_ports = cell->parameters.at("\\WR_PORTS").as_int();
@@ -436,33 +656,24 @@ struct FirrtlWorker
if (offset != 0)
log_error("Memory with nonzero offset: %s.%s\n", log_id(module), log_id(cell));
- cell_exprs.push_back(stringf(" mem %s:\n", mem_id.c_str()));
- cell_exprs.push_back(stringf(" data-type => UInt<%d>\n", width));
- cell_exprs.push_back(stringf(" depth => %d\n", size));
-
- for (int i = 0; i < rd_ports; i++)
- cell_exprs.push_back(stringf(" reader => r%d\n", i));
-
- for (int i = 0; i < wr_ports; i++)
- cell_exprs.push_back(stringf(" writer => w%d\n", i));
-
- cell_exprs.push_back(stringf(" read-latency => 0\n"));
- cell_exprs.push_back(stringf(" write-latency => 1\n"));
- cell_exprs.push_back(stringf(" read-under-write => undefined\n"));
-
for (int i = 0; i < rd_ports; i++)
{
if (rd_clk_enable[i] != State::S0)
log_error("Clocked read port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
+ SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
SigSpec data_sig = cell->getPort("\\RD_DATA").extract(i*width, width);
- string addr_expr = make_expr(cell->getPort("\\RD_ADDR").extract(i*abits, abits));
-
- cell_exprs.push_back(stringf(" %s.r%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
- cell_exprs.push_back(stringf(" %s.r%d.en <= UInt<1>(1)\n", mem_id.c_str(), i));
- cell_exprs.push_back(stringf(" %s.r%d.clk <= asClock(UInt<1>(0))\n", mem_id.c_str(), i));
-
- register_reverse_wire_map(stringf("%s.r%d.data", mem_id.c_str(), i), data_sig);
+ string addr_expr = make_expr(addr_sig);
+ string name(stringf("%s.r%d", m.name.c_str(), i));
+ bool clk_enable = false;
+ bool clk_parity = true;
+ bool transparency = false;
+ SigSpec ena_sig = RTLIL::SigSpec(RTLIL::State::S1, 1);
+ SigSpec clk_sig = RTLIL::SigSpec(RTLIL::State::S0, 1);
+ read_port rp(name, clk_enable, clk_parity, transparency, clk_sig, ena_sig, addr_sig);
+ m.add_memory_read_port(rp);
+ cell_exprs.push_back(rp.gen_read(indent.c_str()));
+ register_reverse_wire_map(stringf("%s.data", name.c_str()), data_sig);
}
for (int i = 0; i < wr_ports; i++)
@@ -473,9 +684,16 @@ struct FirrtlWorker
if (wr_clk_polarity[i] != State::S1)
log_error("Negedge write port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
- string addr_expr = make_expr(cell->getPort("\\WR_ADDR").extract(i*abits, abits));
- string data_expr = make_expr(cell->getPort("\\WR_DATA").extract(i*width, width));
- string clk_expr = make_expr(cell->getPort("\\WR_CLK").extract(i));
+ string name(stringf("%s.w%d", m.name.c_str(), i));
+ bool clk_enable = true;
+ bool clk_parity = true;
+ bool transparency = false;
+ SigSpec addr_sig =cell->getPort("\\WR_ADDR").extract(i*abits, abits);
+ string addr_expr = make_expr(addr_sig);
+ SigSpec data_sig =cell->getPort("\\WR_DATA").extract(i*width, width);
+ string data_expr = make_expr(data_sig);
+ SigSpec clk_sig = cell->getPort("\\WR_CLK").extract(i);
+ string clk_expr = make_expr(clk_sig);
SigSpec wen_sig = cell->getPort("\\WR_EN").extract(i*width, width);
string wen_expr = make_expr(wen_sig[0]);
@@ -484,13 +702,57 @@ struct FirrtlWorker
if (wen_sig[0] != wen_sig[i])
log_error("Complex write enable on port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
- cell_exprs.push_back(stringf(" %s.w%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
- cell_exprs.push_back(stringf(" %s.w%d.data <= %s\n", mem_id.c_str(), i, data_expr.c_str()));
- cell_exprs.push_back(stringf(" %s.w%d.en <= %s\n", mem_id.c_str(), i, wen_expr.c_str()));
- cell_exprs.push_back(stringf(" %s.w%d.mask <= UInt<1>(1)\n", mem_id.c_str(), i));
- cell_exprs.push_back(stringf(" %s.w%d.clk <= asClock(%s)\n", mem_id.c_str(), i, clk_expr.c_str()));
+ SigSpec mask_sig = RTLIL::SigSpec(RTLIL::State::S1, 1);
+ write_port wp(name, clk_enable, clk_parity, transparency, clk_sig, wen_sig[0], addr_sig, mask_sig);
+ m.add_memory_write_port(wp);
+ cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), name.c_str(), data_expr.c_str()));
+ cell_exprs.push_back(wp.gen_write(indent.c_str()));
}
+ register_memory(m);
+ continue;
+ }
+ if (cell->type.in("$memwr", "$memrd", "$meminit"))
+ {
+ std::string cell_type = fid(cell->type);
+ std::string mem_id = make_id(cell->parameters["\\MEMID"].decode_string());
+ int abits = cell->parameters.at("\\ABITS").as_int();
+ int width = cell->parameters.at("\\WIDTH").as_int();
+ memory *mp = nullptr;
+ if (cell->type == "$meminit" ) {
+ log_error("$meminit (%s.%s.%s) currently unsupported\n", log_id(module), log_id(cell), mem_id.c_str());
+ } else {
+ // It's a $memwr or $memrd. Remember the read/write port parameters for the eventual FIRRTL memory definition.
+ auto addrSig = cell->getPort("\\ADDR");
+ auto dataSig = cell->getPort("\\DATA");
+ auto enableSig = cell->getPort("\\EN");
+ auto clockSig = cell->getPort("\\CLK");
+ Const clk_enable = cell->parameters.at("\\CLK_ENABLE");
+ Const clk_polarity = cell->parameters.at("\\CLK_POLARITY");
+
+ // Do we already have an entry for this memory?
+ if (memories.count(mem_id) == 0) {
+ memory m(cell, mem_id, abits, 0, width);
+ register_memory(m);
+ }
+ mp = &memories.at(mem_id);
+ int portNum = 0;
+ bool transparency = false;
+ string data_expr = make_expr(dataSig);
+ if (cell->type.in("$memwr")) {
+ portNum = (int) mp->write_ports.size();
+ write_port wp(stringf("%s.w%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(), transparency, clockSig, enableSig, addrSig, dataSig);
+ mp->add_memory_write_port(wp);
+ cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), wp.name.c_str(), data_expr.c_str()));
+ cell_exprs.push_back(wp.gen_write(indent.c_str()));
+ } else if (cell->type.in("$memrd")) {
+ portNum = (int) mp->read_ports.size();
+ read_port rp(stringf("%s.r%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(), transparency, clockSig, enableSig, addrSig);
+ mp->add_memory_read_port(rp);
+ cell_exprs.push_back(rp.gen_read(indent.c_str()));
+ register_reverse_wire_map(stringf("%s.data", rp.name.c_str()), dataSig);
+ }
+ }
continue;
}
@@ -513,7 +775,65 @@ struct FirrtlWorker
continue;
}
- log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
+ // This may be a parameterized module - paramod.
+ if (cell->type.substr(0, 8) == "$paramod")
+ {
+ process_instance(cell, wire_exprs);
+ continue;
+ }
+ if (cell->type == "$shiftx") {
+ // assign y = a[b +: y_width];
+ // We'll extract the correct bits as part of the primop.
+
+ string y_id = make_id(cell->name);
+ int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
+ string a_expr = make_expr(cell->getPort("\\A"));
+ // Get the initial bit selector
+ string b_expr = make_expr(cell->getPort("\\B"));
+ wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+
+ if (cell->getParam("\\B_SIGNED").as_bool()) {
+ // Use validif to constrain the selection (test the sign bit)
+ auto b_string = b_expr.c_str();
+ int b_sign = cell->parameters.at("\\B_WIDTH").as_int() - 1;
+ b_expr = stringf("validif(not(bits(%s, %d, %d)), %s)", b_string, b_sign, b_sign, b_string);
+ }
+ string expr = stringf("dshr(%s, %s)", a_expr.c_str(), b_expr.c_str());
+
+ cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+ continue;
+ }
+ if (cell->type == "$shift") {
+ // assign y = a >> b;
+ // where b may be negative
+
+ string y_id = make_id(cell->name);
+ int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
+ string a_expr = make_expr(cell->getPort("\\A"));
+ string b_expr = make_expr(cell->getPort("\\B"));
+ auto b_string = b_expr.c_str();
+ int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
+ string expr;
+ wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+
+ if (cell->getParam("\\B_SIGNED").as_bool()) {
+ // We generate a left or right shift based on the sign of b.
+ std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_padded_width).c_str(), y_width);
+ std::string dshr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
+ expr = stringf("mux(%s < 0, %s, %s)",
+ b_string,
+ dshl.c_str(),
+ dshr.c_str()
+ );
+ } else {
+ expr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
+ }
+ cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+ continue;
+ }
+ log_warning("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
}
for (auto conn : module->connections())
@@ -610,6 +930,24 @@ struct FirrtlWorker
f << stringf("\n");
+ // If we have any memory definitions, output them.
+ for (auto kv : memories) {
+ memory &m = kv.second;
+ f << stringf(" mem %s:\n", m.name.c_str());
+ f << stringf(" data-type => UInt<%d>\n", m.width);
+ f << stringf(" depth => %d\n", m.size);
+ for (int i = 0; i < (int) m.read_ports.size(); i += 1) {
+ f << stringf(" reader => r%d\n", i);
+ }
+ for (int i = 0; i < (int) m.write_ports.size(); i += 1) {
+ f << stringf(" writer => w%d\n", i);
+ }
+ f << stringf(" read-latency => %d\n", m.read_latency);
+ f << stringf(" write-latency => %d\n", m.write_latency);
+ f << stringf(" read-under-write => undefined\n");
+ }
+ f << stringf("\n");
+
for (auto str : cell_exprs)
f << str;
@@ -629,38 +967,53 @@ struct FirrtlBackend : public Backend {
log(" write_firrtl [options] [filename]\n");
log("\n");
log("Write a FIRRTL netlist of the current design.\n");
+ log("The following commands are executed by this command:\n");
+ log(" pmuxtree\n");
log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++)
- {
- // if (args[argidx] == "-aig") {
- // aig_mode = true;
- // continue;
- // }
- break;
+ size_t argidx = args.size(); // We aren't expecting any arguments.
+
+ // If we weren't explicitly passed a filename, use the last argument (if it isn't a flag).
+ if (filename == "") {
+ if (argidx > 0 && args[argidx - 1][0] != '-') {
+ // extra_args and friends need to see this argument.
+ argidx -= 1;
+ filename = args[argidx];
+ }
}
extra_args(f, filename, args, argidx);
- log_header(design, "Executing FIRRTL backend.\n");
+ if (!design->full_selection())
+ log_cmd_error("This command only operates on fully selected designs!\n");
- Module *top = design->top_module();
+ log_header(design, "Executing FIRRTL backend.\n");
+ log_push();
- if (top == nullptr)
- log_error("No top module found!\n");
+ Pass::call(design, stringf("pmuxtree"));
namecache.clear();
autoid_counter = 0;
+ // Get the top module, or a reasonable facsimile - we need something for the circuit name.
+ Module *top = design->top_module();
+ Module *last = nullptr;
+ // Generate module and wire names.
for (auto module : design->modules()) {
make_id(module->name);
+ last = module;
+ if (top == nullptr && module->get_bool_attribute("\\top")) {
+ top = module;
+ }
for (auto wire : module->wires())
if (wire->port_id)
make_id(wire->name);
}
+ if (top == nullptr)
+ top = last;
+
*f << stringf("circuit %s:\n", make_id(top->name));
for (auto module : design->modules())
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 4c58ea08..313af7d5 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -160,7 +160,10 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::
}
f << stringf("%s" "cell %s %s\n", indent.c_str(), cell->type.c_str(), cell->name.c_str());
for (auto &it : cell->parameters) {
- f << stringf("%s parameter%s %s ", indent.c_str(), (it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "", it.first.c_str());
+ f << stringf("%s parameter%s%s %s ", indent.c_str(),
+ (it.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0 ? " signed" : "",
+ (it.second.flags & RTLIL::CONST_FLAG_REAL) != 0 ? " real" : "",
+ it.first.c_str());
dump_const(f, it.second);
f << stringf("\n");
}
@@ -201,10 +204,15 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it)
{
+ for (auto ait = (*it)->attributes.begin(); ait != (*it)->attributes.end(); ++ait) {
+ f << stringf("%s attribute %s ", indent.c_str(), ait->first.c_str());
+ dump_const(f, ait->second);
+ f << stringf("\n");
+ }
f << stringf("%s case ", indent.c_str());
for (size_t i = 0; i < (*it)->compare.size(); i++) {
if (i > 0)
- f << stringf(", ");
+ f << stringf(" , ");
dump_sigspec(f, (*it)->compare[i]);
}
f << stringf("\n");
@@ -480,6 +488,7 @@ struct DumpPass : public Pass {
std::stringstream buf;
if (!filename.empty()) {
+ rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), append ? std::ofstream::app : std::ofstream::trunc);
if (ff->fail()) {
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 2eb08dbe..b0e3cd25 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -127,7 +127,7 @@ struct IntersynthBackend : public Backend {
RTLIL::Module *module = module_it.second;
SigMap sigmap(module);
- if (module->get_bool_attribute("\\blackbox"))
+ if (module->get_blackbox_attribute())
continue;
if (module->memories.size() == 0 && module->processes.size() == 0 && module->cells_.size() == 0)
continue;
diff --git a/backends/json/json.cc b/backends/json/json.cc
index f5c68798..dda4dfed 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -126,6 +126,10 @@ struct JsonWriter
f << stringf("%s\n", first ? "" : ",");
f << stringf(" %s: {\n", get_name(n).c_str());
f << stringf(" \"direction\": \"%s\",\n", w->port_input ? w->port_output ? "inout" : "input" : "output");
+ if (w->start_offset)
+ f << stringf(" \"offset\": %d,\n", w->start_offset);
+ if (w->upto)
+ f << stringf(" \"upto\": 1,\n");
f << stringf(" \"bits\": %s\n", get_bits(w).c_str());
f << stringf(" }");
first = false;
@@ -189,6 +193,10 @@ struct JsonWriter
f << stringf(" %s: {\n", get_name(w->name).c_str());
f << stringf(" \"hide_name\": %s,\n", w->name[0] == '$' ? "1" : "0");
f << stringf(" \"bits\": %s,\n", get_bits(w).c_str());
+ if (w->start_offset)
+ f << stringf(" \"offset\": %d,\n", w->start_offset);
+ if (w->upto)
+ f << stringf(" \"upto\": 1,\n");
f << stringf(" \"attributes\": {");
write_parameters(w->attributes);
f << stringf("\n }\n");
@@ -525,6 +533,7 @@ struct JsonPass : public Pass {
std::stringstream buf;
if (!filename.empty()) {
+ rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), std::ofstream::trunc);
if (ff->fail()) {
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index f56147ce..fff110bb 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -48,7 +48,7 @@ struct ProtobufDesignSerializer
ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
aig_mode_(aig_mode), use_selection_(use_selection) { }
-
+
string get_name(IdString name)
{
return RTLIL::unescape_id(name);
@@ -60,7 +60,7 @@ struct ProtobufDesignSerializer
{
for (auto &param : parameters) {
std::string key = get_name(param.first);
-
+
yosys::pb::Parameter pb_param;
@@ -207,7 +207,7 @@ struct ProtobufDesignSerializer
(*models)[aig.name] = pb_model;
}
}
-
+
void serialize_design(yosys::pb::Design *pb, Design *design)
{
GOOGLE_PROTOBUF_VERIFY_VERSION;
@@ -336,6 +336,7 @@ struct ProtobufPass : public Pass {
std::stringstream buf;
if (!filename.empty()) {
+ rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), std::ofstream::trunc);
if (ff->fail()) {
diff --git a/backends/simplec/test00_uut.v b/backends/simplec/test00_uut.v
index 744dbe9e..92329a6f 100644
--- a/backends/simplec/test00_uut.v
+++ b/backends/simplec/test00_uut.v
@@ -3,12 +3,12 @@ module test(input [31:0] a, b, c, output [31:0] x, y, z, w);
unit_y unit_y_inst (.a(a), .b(b), .c(c), .y(y));
assign z = a ^ b ^ c, w = z;
endmodule
-
+
module unit_x(input [31:0] a, b, c, output [31:0] x);
assign x = (a & b) | c;
endmodule
-
+
module unit_y(input [31:0] a, b, c, output [31:0] y);
assign y = a & (b | c);
endmodule
-
+
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index f98e6104..2c0b7c69 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o
ifneq ($(CONFIG),mxe)
ifneq ($(CONFIG),emcc)
+
+# MSYS targets support yosys-smtbmc, but require a launcher script
+ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
+TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py
+# Needed to find the Python interpreter for yosys-smtbmc scripts.
+# Override if necessary, it is only used for msys2 targets.
+PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
+
+yosys-smtbmc-script.py: backends/smt2/smtbmc.py
+ $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \
+ -e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+
+yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
+ $(P) gcc -DGUI=0 -O -s -o $@ $<
+# Other targets
+else
TARGETS += yosys-smtbmc
yosys-smtbmc: backends/smt2/smtbmc.py
$(P) sed 's|##yosys-sys-path##|sys.path += ["/usr/share/yosys"]|;' < $< > $@.new
$(Q) chmod +x $@.new
$(Q) mv $@.new $@
+endif
$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
endif
endif
-
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e2777ae0..e318a405 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -416,6 +416,7 @@ struct Smt2Worker
for (char ch : expr) {
if (ch == 'A') processed_expr += get_bv(sig_a);
else if (ch == 'B') processed_expr += get_bv(sig_b);
+ else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
else processed_expr += ch;
@@ -554,7 +555,9 @@ struct Smt2Worker
if (cell->type.in("$shift", "$shiftx")) {
if (cell->getParam("\\B_SIGNED").as_bool()) {
- /* FIXME */
+ return export_bvop(cell, stringf("(ite (bvsge P #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');
}
@@ -885,8 +888,8 @@ struct Smt2Worker
string name_a = get_bool(cell->getPort("\\A"));
string name_en = get_bool(cell->getPort("\\EN"));
- decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
- cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+ string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+ decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
if (cell->type == "$cover")
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1101,20 +1104,27 @@ struct Smt2Worker
break;
Const initword = init_data.extract(i*width, width, State::Sx);
+ Const initmask = initword;
bool gen_init_constr = false;
- for (auto bit : initword.bits)
- if (bit == State::S0 || bit == State::S1)
+ for (int k = 0; k < GetSize(initword); k++) {
+ if (initword[k] == State::S0 || initword[k] == State::S1) {
gen_init_constr = true;
+ initmask[k] = State::S1;
+ } else {
+ initmask[k] = State::S0;
+ initword[k] = State::S0;
+ }
+ }
if (gen_init_constr)
{
if (statebv)
/* FIXME */;
else
- init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+ init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
get_id(module), arrayid, Const(i, abits).as_string().c_str(),
- initword.as_string().c_str(), get_id(cell), i));
+ initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
}
}
}
@@ -1533,7 +1543,7 @@ struct Smt2Backend : public Backend {
for (auto module : sorted_modules)
{
- if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
+ if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn())
continue;
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 6af2a5ac..445a42e0 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -32,6 +32,7 @@ cexfile = None
aimfile = None
aiwfile = None
aigheader = True
+btorwitfile = None
vlogtbfile = None
vlogtbtop = None
inconstr = list()
@@ -86,12 +87,15 @@ yosys-smtbmc [options] <yosys_smt2_output>
--aig <aim_filename>:<aiw_filename>
like above, but for map files and witness files that do not
- share a filename prefix (or use differen file extensions).
+ share a filename prefix (or use different file extensions).
--aig-noheader
the AIGER witness file does not include the status and
properties lines.
+ --btorwit <btor_witness_filename>
+ read a BTOR witness.
+
--noinfo
only run the core proof, do not collect and print any
additional information (e.g. which assert failed)
@@ -99,8 +103,8 @@ yosys-smtbmc [options] <yosys_smt2_output>
--presat
check if the design with assumptions but without assertions
is SAT before checking if assertions are UNSAT. This will
- detect if there are contradicting assumtions. In some cases
- this will also help to "warmup" the solver, potentially
+ detect if there are contradicting assumptions. In some cases
+ this will also help to "warm up" the solver, potentially
yielding a speedup.
--final-only
@@ -145,14 +149,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
--append <num_steps>
add <num_steps> time steps at the end of the trace
when creating a counter example (this additional time
- steps will still be constrained by assumtions)
+ steps will still be constrained by assumptions)
""" + so.helpmsg())
sys.exit(1)
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 +193,8 @@ for o, a in opts:
aiwfile = a + ".aiw"
elif o == "--aig-noheader":
aigheader = False
+ elif o == "--btorwit":
+ btorwitfile = a
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-vlogtb":
@@ -575,6 +581,103 @@ if aimfile is not None:
num_steps = max(num_steps, step+1)
step += 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)
print_msg("Writing trace to VCD file: %s" % (filename))
@@ -1259,7 +1362,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 +1484,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)
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 3fc823e3..ae7968a1 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -31,11 +31,19 @@ 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
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))
+
+ 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:
+ resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
# currently running solvers (so we can kill them)
@@ -158,19 +166,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":
@@ -767,7 +784,7 @@ class SmtIo:
def get_path(self, mod, path):
assert mod in self.modinfo
- path = path.split(".")
+ path = path.replace("\\", "/").split(".")
for i in range(len(path)-1):
first = ".".join(path[0:i+1])
@@ -1006,6 +1023,8 @@ class MkVcd:
assert t >= self.t
if t != self.t:
if self.t == -1:
+ print("$version Generated by Yosys-SMTBMC $end", file=self.f)
+ print("$timescale 1ns $end", file=self.f)
print("$var integer 32 t smt_step $end", file=self.f)
print("$var event 1 ! smt_clock $end", file=self.f)
@@ -1024,7 +1043,10 @@ class MkVcd:
scope = scope[:-1]
while uipath[:-1] != scope:
- print("$scope module %s $end" % uipath[len(scope)], file=self.f)
+ scopename = uipath[len(scope)]
+ if scopename.startswith("$"):
+ scopename = "\\" + scopename
+ print("$scope module %s $end" % scopename, file=self.f)
scope.append(uipath[len(scope)])
if path in self.clocks and self.clocks[path][1] == "event":
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index b8383412..d75456c1 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -42,7 +42,7 @@ struct SmvWorker
pool<Wire*> partial_assignment_wires;
dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
- vector<string> assignments, invarspecs;
+ vector<string> 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"))));
@@ -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()) {
@@ -720,7 +739,7 @@ struct SmvBackend : public Backend {
pool<Module*> modules;
for (auto module : design->modules())
- if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
+ if (!module->get_blackbox_attribute() && !module->has_memories_warn() && !module->has_processes_warn())
modules.insert(module);
if (template_f.is_open())
diff --git a/backends/spice/spice.cc b/backends/spice/spice.cc
index b6a3f1e7..6738a4bb 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -212,7 +212,7 @@ struct SpiceBackend : public Backend {
for (auto module_it : design->modules_)
{
RTLIL::Module *module = module_it.second;
- if (module->get_bool_attribute("\\blackbox"))
+ if (module->get_blackbox_attribute())
continue;
if (module->processes.size() != 0)
diff --git a/backends/table/table.cc b/backends/table/table.cc
index b75169ea..796f1805 100644
--- a/backends/table/table.cc
+++ b/backends/table/table.cc
@@ -67,7 +67,7 @@ struct TableBackend : public Backend {
for (auto module : design->modules())
{
- if (module->get_bool_attribute("\\blackbox"))
+ if (module->get_blackbox_attribute())
continue;
SigMap sigmap(module);
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index d53df2e7..087c6fec 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -33,7 +33,7 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal, siminit;
int auto_name_counter, auto_name_offset, auto_name_digits;
std::map<RTLIL::IdString, int> auto_name_map;
std::set<RTLIL::IdString> reg_wires, reg_ct;
@@ -126,6 +126,33 @@ std::string id(RTLIL::IdString internal_id, bool may_rename = true)
break;
}
+ const pool<string> keywords = {
+ // IEEE 1800-2017 Annex B
+ "accept_on", "alias", "always", "always_comb", "always_ff", "always_latch", "and", "assert", "assign", "assume", "automatic", "before",
+ "begin", "bind", "bins", "binsof", "bit", "break", "buf", "bufif0", "bufif1", "byte", "case", "casex", "casez", "cell", "chandle",
+ "checker", "class", "clocking", "cmos", "config", "const", "constraint", "context", "continue", "cover", "covergroup", "coverpoint",
+ "cross", "deassign", "default", "defparam", "design", "disable", "dist", "do", "edge", "else", "end", "endcase", "endchecker",
+ "endclass", "endclocking", "endconfig", "endfunction", "endgenerate", "endgroup", "endinterface", "endmodule", "endpackage",
+ "endprimitive", "endprogram", "endproperty", "endsequence", "endspecify", "endtable", "endtask", "enum", "event", "eventually",
+ "expect", "export", "extends", "extern", "final", "first_match", "for", "force", "foreach", "forever", "fork", "forkjoin", "function",
+ "generate", "genvar", "global", "highz0", "highz1", "if", "iff", "ifnone", "ignore_bins", "illegal_bins", "implements", "implies",
+ "import", "incdir", "include", "initial", "inout", "input", "inside", "instance", "int", "integer", "interconnect", "interface",
+ "intersect", "join", "join_any", "join_none", "large", "let", "liblist", "library", "local", "localparam", "logic", "longint",
+ "macromodule", "matches", "medium", "modport", "module", "nand", "negedge", "nettype", "new", "nexttime", "nmos", "nor",
+ "noshowcancelled", "not", "notif0", "notif1", "null", "or", "output", "package", "packed", "parameter", "pmos", "posedge", "primitive",
+ "priority", "program", "property", "protected", "pull0", "pull1", "pulldown", "pullup", "pulsestyle_ondetect", "pulsestyle_onevent",
+ "pure", "rand", "randc", "randcase", "randsequence", "rcmos", "real", "realtime", "ref", "reg", "reject_on", "release", "repeat",
+ "restrict", "return", "rnmos", "rpmos", "rtran", "rtranif0", "rtranif1", "s_always", "s_eventually", "s_nexttime", "s_until",
+ "s_until_with", "scalared", "sequence", "shortint", "shortreal", "showcancelled", "signed", "small", "soft", "solve", "specify",
+ "specparam", "static", "string", "strong", "strong0", "strong1", "struct", "super", "supply0", "supply1", "sync_accept_on",
+ "sync_reject_on", "table", "tagged", "task", "this", "throughout", "time", "timeprecision", "timeunit", "tran", "tranif0", "tranif1",
+ "tri", "tri0", "tri1", "triand", "trior", "trireg", "type", "typedef", "union", "unique", "unique0", "unsigned", "until", "until_with",
+ "untyped", "use", "uwire", "var", "vectored", "virtual", "void", "wait", "wait_order", "wand", "weak", "weak0", "weak1", "while",
+ "wildcard", "wire", "with", "within", "wor", "xnor", "xor",
+ };
+ if (keywords.count(str))
+ do_escape = true;
+
if (do_escape)
return "\\" + std::string(str) + " ";
return std::string(str);
@@ -156,10 +183,15 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
return true;
}
-void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool set_signed = false, bool escape_comment = false)
+void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool no_decimal = false, bool escape_comment = false)
{
+ bool set_signed = (data.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
if (width < 0)
width = data.bits.size() - offset;
+ if (width == 0) {
+ f << "\"\"";
+ return;
+ }
if (nostr)
goto dump_hex;
if ((data.flags & RTLIL::CONST_FLAG_STRING) == 0 || width != (int)data.bits.size()) {
@@ -244,7 +276,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
}
}
} else {
- f << stringf("\"");
+ if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0)
+ f << stringf("\"");
std::string str = data.decode_string();
for (size_t i = 0; i < str.size(); i++) {
if (str[i] == '\n')
@@ -262,7 +295,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
else
f << str[i];
}
- f << stringf("\"");
+ if ((data.flags & RTLIL::CONST_FLAG_REAL) == 0)
+ f << stringf("\"");
}
}
@@ -313,6 +347,10 @@ void dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool no_decima
void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
{
+ if (GetSize(sig) == 0) {
+ f << "\"\"";
+ return;
+ }
if (sig.is_chunk()) {
dump_sigchunk(f, sig.as_chunk());
} else {
@@ -326,20 +364,22 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
}
}
-void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false)
+void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false, bool as_comment = false)
{
if (noattr)
return;
+ if (attr2comment)
+ as_comment = true;
for (auto it = attributes.begin(); it != attributes.end(); ++it) {
- f << stringf("%s" "%s %s", indent.c_str(), attr2comment ? "/*" : "(*", id(it->first).c_str());
+ f << stringf("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str());
f << stringf(" = ");
if (modattr && (it->second == Const(0, 1) || it->second == Const(0)))
f << stringf(" 0 ");
else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
f << stringf(" 1 ");
else
- dump_const(f, it->second, -1, 0, false, false, attr2comment);
- f << stringf(" %s%c", attr2comment ? "*/" : "*)", term);
+ dump_const(f, it->second, -1, 0, false, as_comment);
+ f << stringf(" %s%c", as_comment ? "*/" : "*)", term);
}
}
@@ -388,7 +428,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)
@@ -678,13 +718,45 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
#undef HANDLE_UNIOP
#undef HANDLE_BINOP
- if (cell->type == "$shiftx")
+ 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")
+ {
+ std::string temp_id = next_auto_id();
+ f << stringf("%s" "wire [%d:0] %s = ", indent.c_str(), GetSize(cell->getPort("\\A"))-1, temp_id.c_str());
dump_sigspec(f, cell->getPort("\\A"));
- f << stringf("[");
+ f << stringf(";\n");
+
+ f << stringf("%s" "assign ", indent.c_str());
+ dump_sigspec(f, cell->getPort("\\Y"));
+ f << stringf(" = %s[", temp_id.c_str());
if (cell->getParam("\\B_SIGNED").as_bool())
f << stringf("$signed(");
dump_sigspec(f, cell->getPort("\\B"));
@@ -757,6 +829,18 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type == "$tribuf")
+ {
+ f << stringf("%s" "assign ", indent.c_str());
+ dump_sigspec(f, cell->getPort("\\Y"));
+ f << stringf(" = ");
+ dump_sigspec(f, cell->getPort("\\EN"));
+ f << stringf(" ? ");
+ dump_sigspec(f, cell->getPort("\\A"));
+ f << stringf(" : %d'bz;\n", cell->parameters.at("\\WIDTH").as_int());
+ return true;
+ }
+
if (cell->type == "$slice")
{
f << stringf("%s" "assign ", indent.c_str());
@@ -952,6 +1036,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 +1045,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());
@@ -993,43 +1078,46 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
use_rd_clk = cell->parameters["\\RD_CLK_ENABLE"].extract(i).as_bool();
rd_clk_posedge = cell->parameters["\\RD_CLK_POLARITY"].extract(i).as_bool();
rd_transparent = cell->parameters["\\RD_TRANSPARENT"].extract(i).as_bool();
+ if (use_rd_clk)
{
- std::ostringstream os;
- dump_sigspec(os, sig_rd_clk);
- clk_domain_str = stringf("%sedge %s", rd_clk_posedge ? "pos" : "neg", os.str().c_str());
- if( clk_to_lof_body.count(clk_domain_str) == 0 )
- clk_to_lof_body[clk_domain_str] = std::vector<std::string>();
- }
- if (use_rd_clk && !rd_transparent)
- {
- // for clocked read ports make something like:
- // reg [..] temp_id;
- // always @(posedge clk)
- // if (rd_en) temp_id <= array_reg[r_addr];
- // assign r_data = temp_id;
- std::string temp_id = next_auto_id();
- lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", sig_rd_data.size() - 1, temp_id.c_str()) );
{
std::ostringstream os;
- if (sig_rd_en != RTLIL::SigBit(true))
+ dump_sigspec(os, sig_rd_clk);
+ clk_domain_str = stringf("%sedge %s", rd_clk_posedge ? "pos" : "neg", os.str().c_str());
+ if( clk_to_lof_body.count(clk_domain_str) == 0 )
+ clk_to_lof_body[clk_domain_str] = std::vector<std::string>();
+ }
+ if (!rd_transparent)
+ {
+ // for clocked read ports make something like:
+ // reg [..] temp_id;
+ // always @(posedge clk)
+ // if (rd_en) temp_id <= array_reg[r_addr];
+ // assign r_data = temp_id;
+ std::string temp_id = next_auto_id();
+ lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", sig_rd_data.size() - 1, temp_id.c_str()) );
+ {
+ std::ostringstream os;
+ if (sig_rd_en != RTLIL::SigBit(true))
+ {
+ os << stringf("if (");
+ dump_sigspec(os, sig_rd_en);
+ os << stringf(") ");
+ }
+ os << stringf("%s <= %s[", temp_id.c_str(), mem_id.c_str());
+ dump_sigspec(os, sig_rd_addr);
+ os << stringf("];\n");
+ clk_to_lof_body[clk_domain_str].push_back(os.str());
+ }
{
- os << stringf("if (");
- dump_sigspec(os, sig_rd_en);
- os << stringf(") ");
+ std::ostringstream os;
+ dump_sigspec(os, sig_rd_data);
+ std::string line = stringf("assign %s = %s;\n", os.str().c_str(), temp_id.c_str());
+ clk_to_lof_body[""].push_back(line);
}
- os << stringf("%s <= %s[", temp_id.c_str(), mem_id.c_str());
- dump_sigspec(os, sig_rd_addr);
- os << stringf("];\n");
- clk_to_lof_body[clk_domain_str].push_back(os.str());
}
+ else
{
- std::ostringstream os;
- dump_sigspec(os, sig_rd_data);
- std::string line = stringf("assign %s = %s;\n", os.str().c_str(), temp_id.c_str());
- clk_to_lof_body[""].push_back(line);
- }
- } else {
- if (rd_transparent) {
// for rd-transparent read-ports make something like:
// reg [..] temp_id;
// always @(posedge clk)
@@ -1049,15 +1137,15 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), temp_id.c_str());
clk_to_lof_body[""].push_back(line);
}
- } else {
- // for non-clocked read-ports make something like:
- // assign r_data = array_reg[r_addr];
- std::ostringstream os, os2;
- dump_sigspec(os, sig_rd_data);
- dump_sigspec(os2, sig_rd_addr);
- std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), os2.str().c_str());
- clk_to_lof_body[""].push_back(line);
}
+ } else {
+ // for non-clocked read-ports make something like:
+ // assign r_data = array_reg[r_addr];
+ std::ostringstream os, os2;
+ dump_sigspec(os, sig_rd_data);
+ dump_sigspec(os2, sig_rd_addr);
+ std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), os2.str().c_str());
+ clk_to_lof_body[""].push_back(line);
}
}
@@ -1159,6 +1247,118 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type.in("$assert", "$assume", "$cover"))
+ {
+ f << stringf("%s" "always @* if (", indent.c_str());
+ dump_sigspec(f, cell->getPort("\\EN"));
+ f << stringf(") %s(", cell->type.c_str()+1);
+ dump_sigspec(f, cell->getPort("\\A"));
+ f << stringf(");\n");
+ return true;
+ }
+
+ if (cell->type.in("$specify2", "$specify3"))
+ {
+ f << stringf("%s" "specify\n%s ", indent.c_str(), indent.c_str());
+
+ SigSpec en = cell->getPort("\\EN");
+ if (en != State::S1) {
+ f << stringf("if (");
+ dump_sigspec(f, cell->getPort("\\EN"));
+ f << stringf(") ");
+ }
+
+ f << "(";
+ if (cell->type == "$specify3" && cell->getParam("\\EDGE_EN").as_bool())
+ f << (cell->getParam("\\EDGE_POL").as_bool() ? "posedge ": "negedge ");
+
+ dump_sigspec(f, cell->getPort("\\SRC"));
+
+ f << " ";
+ if (cell->getParam("\\SRC_DST_PEN").as_bool())
+ f << (cell->getParam("\\SRC_DST_POL").as_bool() ? "+": "-");
+ f << (cell->getParam("\\FULL").as_bool() ? "*> ": "=> ");
+
+ if (cell->type == "$specify3") {
+ f << "(";
+ dump_sigspec(f, cell->getPort("\\DST"));
+ f << " ";
+ if (cell->getParam("\\DAT_DST_PEN").as_bool())
+ f << (cell->getParam("\\DAT_DST_POL").as_bool() ? "+": "-");
+ f << ": ";
+ dump_sigspec(f, cell->getPort("\\DAT"));
+ f << ")";
+ } else {
+ dump_sigspec(f, cell->getPort("\\DST"));
+ }
+
+ bool bak_decimal = decimal;
+ decimal = 1;
+
+ f << ") = (";
+ dump_const(f, cell->getParam("\\T_RISE_MIN"));
+ f << ":";
+ dump_const(f, cell->getParam("\\T_RISE_TYP"));
+ f << ":";
+ dump_const(f, cell->getParam("\\T_RISE_MAX"));
+ f << ", ";
+ dump_const(f, cell->getParam("\\T_FALL_MIN"));
+ f << ":";
+ dump_const(f, cell->getParam("\\T_FALL_TYP"));
+ f << ":";
+ dump_const(f, cell->getParam("\\T_FALL_MAX"));
+ f << ");\n";
+
+ decimal = bak_decimal;
+
+ f << stringf("%s" "endspecify\n", indent.c_str());
+ return true;
+ }
+
+ if (cell->type == "$specrule")
+ {
+ f << stringf("%s" "specify\n%s ", indent.c_str(), indent.c_str());
+
+ string spec_type = cell->getParam("\\TYPE").decode_string();
+ f << stringf("%s(", spec_type.c_str());
+
+ if (cell->getParam("\\SRC_PEN").as_bool())
+ f << (cell->getParam("\\SRC_POL").as_bool() ? "posedge ": "negedge ");
+ dump_sigspec(f, cell->getPort("\\SRC"));
+
+ if (cell->getPort("\\SRC_EN") != State::S1) {
+ f << " &&& ";
+ dump_sigspec(f, cell->getPort("\\SRC_EN"));
+ }
+
+ f << ", ";
+ if (cell->getParam("\\DST_PEN").as_bool())
+ f << (cell->getParam("\\DST_POL").as_bool() ? "posedge ": "negedge ");
+ dump_sigspec(f, cell->getPort("\\DST"));
+
+ if (cell->getPort("\\DST_EN") != State::S1) {
+ f << " &&& ";
+ dump_sigspec(f, cell->getPort("\\DST_EN"));
+ }
+
+ bool bak_decimal = decimal;
+ decimal = 1;
+
+ f << ", ";
+ dump_const(f, cell->getParam("\\T_LIMIT"));
+
+ if (spec_type == "$setuphold" || spec_type == "$recrem" || spec_type == "$fullskew") {
+ f << ", ";
+ dump_const(f, cell->getParam("\\T_LIMIT2"));
+ }
+
+ f << ");\n";
+ decimal = bak_decimal;
+
+ f << stringf("%s" "endspecify\n", indent.c_str());
+ return true;
+ }
+
// FIXME: $_SR_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_
// FIXME: $sr, $dlatch, $memrd, $memwr, $fsm
@@ -1181,8 +1381,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
if (it != cell->parameters.begin())
f << stringf(",");
f << stringf("\n%s .%s(", indent.c_str(), id(it->first).c_str());
- bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
- dump_const(f, it->second, -1, 0, false, is_signed);
+ dump_const(f, it->second);
f << stringf(")");
}
f << stringf("\n%s" ")", indent.c_str());
@@ -1229,12 +1428,20 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
if (defparam && cell->parameters.size() > 0) {
for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) {
f << stringf("%sdefparam %s.%s = ", indent.c_str(), cell_name.c_str(), id(it->first).c_str());
- bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
- dump_const(f, it->second, -1, 0, false, is_signed);
+ dump_const(f, it->second);
f << stringf(";\n");
}
}
+ if (siminit && reg_ct.count(cell->type) && cell->hasPort("\\Q")) {
+ std::stringstream ss;
+ dump_reg_init(ss, cell->getPort("\\Q"));
+ if (!ss.str().empty()) {
+ f << stringf("%sinitial %s.Q", indent.c_str(), cell_name.c_str());
+ f << ss.str();
+ f << ";\n";
+ }
+ }
}
void dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right)
@@ -1287,12 +1494,14 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
return;
}
+ dump_attributes(f, indent, sw->attributes);
f << stringf("%s" "casez (", indent.c_str());
dump_sigspec(f, sw->signal);
f << stringf(")\n");
bool got_default = false;
for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
+ dump_attributes(f, indent + " ", (*it)->attributes, '\n', /*modattr=*/false, /*as_comment=*/true);
if ((*it)->compare.size() == 0) {
if (got_default)
continue;
@@ -1351,6 +1560,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)
@@ -1411,14 +1622,15 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
SigSpec sig = active_sigmap(wire);
Const val = wire->attributes.at("\\init");
for (int i = 0; i < GetSize(sig) && i < GetSize(val); i++)
- active_initdata[sig[i]] = val.bits.at(i);
+ if (val[i] == State::S0 || val[i] == State::S1)
+ active_initdata[sig[i]] = val[i];
}
if (!module->processes.empty())
log_warning("Module %s contains unmapped RTLIL processes. 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)
@@ -1454,7 +1666,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
}
}
- dump_attributes(f, indent, module->attributes, '\n', true);
+ dump_attributes(f, indent, module->attributes, '\n', /*attr2comment=*/true);
f << stringf("%s" "module %s(", indent.c_str(), id(module->name, false).c_str());
bool keep_running = true;
for (int port_id = 1; keep_running; port_id++) {
@@ -1521,6 +1733,10 @@ struct VerilogBackend : public Backend {
log(" without this option all internal cells are converted to Verilog\n");
log(" expressions.\n");
log("\n");
+ log(" -siminit\n");
+ log(" add initial statements with hierarchical refs to initialize FFs when\n");
+ log(" in -noexpr mode.\n");
+ log("\n");
log(" -nodec\n");
log(" 32-bit constant values are by default dumped as decimal numbers,\n");
log(" not bit pattern. This option deactivates this feature and instead\n");
@@ -1577,11 +1793,14 @@ struct VerilogBackend : public Backend {
nostr = false;
defparam = false;
decimal = false;
+ siminit = false;
auto_prefix = "";
bool blackboxes = false;
bool selected = false;
+ auto_name_map.clear();
+ reg_wires.clear();
reg_ct.clear();
reg_ct.insert("$dff");
@@ -1653,6 +1872,10 @@ struct VerilogBackend : public Backend {
decimal = true;
continue;
}
+ if (arg == "-siminit") {
+ siminit = true;
+ continue;
+ }
if (arg == "-blackboxes") {
blackboxes = true;
continue;
@@ -1673,7 +1896,7 @@ struct VerilogBackend : public Backend {
*f << stringf("/* Generated by %s */\n", yosys_version_str);
for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
- if (it->second->get_bool_attribute("\\blackbox") != blackboxes)
+ if (it->second->get_blackbox_attribute() != blackboxes)
continue;
if (selected && !design->selected_whole_module(it->first)) {
if (design->selected_module(it->first))
@@ -1684,6 +1907,8 @@ struct VerilogBackend : public Backend {
dump_module(*f, "", it->second);
}
+ auto_name_map.clear();
+ reg_wires.clear();
reg_ct.clear();
}
} VerilogBackend;
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-26 19:00:25 +0000