aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/Makefile.inc1
-rw-r--r--backends/aiger/aiger.cc107
-rw-r--r--backends/aiger/xaiger.cc879
-rw-r--r--backends/blif/blif.cc45
-rw-r--r--backends/btor/btor.cc174
-rw-r--r--backends/edif/edif.cc67
-rw-r--r--backends/firrtl/firrtl.cc856
-rw-r--r--backends/ilang/ilang_backend.cc29
-rw-r--r--backends/intersynth/intersynth.cc10
-rw-r--r--backends/json/json.cc65
-rw-r--r--backends/protobuf/protobuf.cc15
-rw-r--r--backends/simplec/simplec.cc12
-rw-r--r--backends/simplec/test00_uut.v6
-rw-r--r--backends/smt2/Makefile.inc20
-rw-r--r--backends/smt2/smt2.cc35
-rw-r--r--backends/smt2/smtbmc.py125
-rw-r--r--backends/smt2/smtio.py57
-rw-r--r--backends/smv/smv.cc98
-rw-r--r--backends/spice/spice.cc6
-rw-r--r--backends/table/table.cc8
-rw-r--r--backends/verilog/verilog_backend.cc422
21 files changed, 2597 insertions, 440 deletions
diff --git a/backends/aiger/Makefile.inc b/backends/aiger/Makefile.inc
index 0fc37e95c..4a4cf30bd 100644
--- a/backends/aiger/Makefile.inc
+++ b/backends/aiger/Makefile.inc
@@ -1,3 +1,4 @@
OBJS += backends/aiger/aiger.o
+OBJS += backends/aiger/xaiger.o
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 526e50a49..0798fb35d 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -70,37 +70,38 @@ struct AigerWriter
int bit2aig(SigBit bit)
{
- if (aig_map.count(bit) == 0)
- {
- aig_map[bit] = -1;
-
- if (initstate_bits.count(bit)) {
- log_assert(initstate_ff > 0);
- aig_map[bit] = initstate_ff;
- } else
- if (not_map.count(bit)) {
- int a = bit2aig(not_map.at(bit)) ^ 1;
- aig_map[bit] = a;
- } else
- if (and_map.count(bit)) {
- auto args = and_map.at(bit);
- int a0 = bit2aig(args.first);
- int a1 = bit2aig(args.second);
- aig_map[bit] = mkgate(a0, a1);
- } else
- if (alias_map.count(bit)) {
- aig_map[bit] = bit2aig(alias_map.at(bit));
- }
+ auto it = aig_map.find(bit);
+ if (it != aig_map.end()) {
+ log_assert(it->second >= 0);
+ return it->second;
+ }
- if (bit == State::Sx || bit == State::Sz)
- log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+ // NB: Cannot use iterator returned from aig_map.insert()
+ // since this function is called recursively
+
+ int a = -1;
+ if (not_map.count(bit)) {
+ a = bit2aig(not_map.at(bit)) ^ 1;
+ } else
+ if (and_map.count(bit)) {
+ auto args = and_map.at(bit);
+ int a0 = bit2aig(args.first);
+ int a1 = bit2aig(args.second);
+ a = mkgate(a0, a1);
+ } else
+ if (alias_map.count(bit)) {
+ a = bit2aig(alias_map.at(bit));
}
- log_assert(aig_map.at(bit) >= 0);
- return aig_map.at(bit);
+ if (bit == State::Sx || bit == State::Sz)
+ log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+
+ log_assert(a >= 0);
+ aig_map[bit] = a;
+ return a;
}
- 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, bool lmode) : 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) {
@@ -362,6 +367,12 @@ struct AigerWriter
aig_latchin.push_back(a);
}
+ if (lmode && aig_l == 0) {
+ aig_m++, aig_l++;
+ aig_latchinit.push_back(0);
+ aig_latchin.push_back(0);
+ }
+
if (!initstate_bits.empty() || !init_inputs.empty())
aig_latchin.push_back(1);
@@ -371,6 +382,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 +394,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);
@@ -657,7 +678,7 @@ struct AigerWriter
struct AigerBackend : public Backend {
AigerBackend() : Backend("aiger", "write design to AIGER file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -671,7 +692,7 @@ struct AigerBackend : public Backend {
log("invariant constraints.\n");
log("\n");
log(" -ascii\n");
- log(" write ASCII version of AGIER format\n");
+ log(" write ASCII version of AIGER format\n");
log("\n");
log(" -zinit\n");
log(" convert FFs to zero-initialized FFs, adding additional inputs for\n");
@@ -689,14 +710,23 @@ struct AigerBackend : public Backend {
log(" -vmap <filename>\n");
log(" like -map, but more verbose\n");
log("\n");
+ log(" -I, -O, -B, -L\n");
+ log(" If the design contains no input/output/assert/flip-flop then create one\n");
+ log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n");
+ log(" AIGER file happy.\n");
+ log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
bool ascii_mode = false;
bool zinit_mode = false;
bool miter_mode = false;
bool symbols_mode = false;
bool verbose_map = false;
+ bool imode = false;
+ bool omode = false;
+ bool bmode = false;
+ bool lmode = false;
std::string map_filename;
log_header(design, "Executing AIGER backend.\n");
@@ -729,6 +759,22 @@ 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;
+ }
+ if (args[argidx] == "-L") {
+ lmode = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -738,10 +784,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, lmode);
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/aiger/xaiger.cc b/backends/aiger/xaiger.cc
new file mode 100644
index 000000000..fa6ba0aca
--- /dev/null
+++ b/backends/aiger/xaiger.cc
@@ -0,0 +1,879 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * 2019 Eddie Hung <eddie@fpgeh.com>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+// https://stackoverflow.com/a/46137633
+#ifdef _MSC_VER
+#include <stdlib.h>
+#define bswap32 _byteswap_ulong
+#elif defined(__APPLE__)
+#include <libkern/OSByteOrder.h>
+#define bswap32 OSSwapInt32
+#elif defined(__GNUC__)
+#define bswap32 __builtin_bswap32
+#else
+#include <cstdint>
+inline static uint32_t bswap32(uint32_t x)
+{
+ // https://stackoverflow.com/a/27796212
+ register uint32_t value = number_to_be_reversed;
+ uint8_t lolo = (value >> 0) & 0xFF;
+ uint8_t lohi = (value >> 8) & 0xFF;
+ uint8_t hilo = (value >> 16) & 0xFF;
+ uint8_t hihi = (value >> 24) & 0xFF;
+ return (hihi << 24)
+ | (hilo << 16)
+ | (lohi << 8)
+ | (lolo << 0);
+}
+#endif
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+#include "kernel/utils.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+inline int32_t to_big_endian(int32_t i32) {
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+ return bswap32(i32);
+#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
+ return i32;
+#else
+#error "Unknown endianness"
+#endif
+}
+
+void aiger_encode(std::ostream &f, int x)
+{
+ log_assert(x >= 0);
+
+ while (x & ~0x7f) {
+ f.put((x & 0x7f) | 0x80);
+ x = x >> 7;
+ }
+
+ f.put(x);
+}
+
+struct XAigerWriter
+{
+ Module *module;
+ SigMap sigmap;
+
+ pool<SigBit> input_bits, output_bits;
+ dict<SigBit, SigBit> not_map, alias_map;
+ dict<SigBit, pair<SigBit, SigBit>> and_map;
+ vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int>> ci_bits;
+ vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int,int>> co_bits;
+ dict<SigBit, float> arrival_times;
+
+ vector<pair<int, int>> aig_gates;
+ vector<int> aig_outputs;
+ int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0;
+
+ dict<SigBit, int> aig_map;
+ dict<SigBit, int> ordered_outputs;
+
+ vector<Cell*> box_list;
+ bool omode = false;
+
+ int mkgate(int a0, int a1)
+ {
+ aig_m++, aig_a++;
+ aig_gates.push_back(a0 > a1 ? make_pair(a0, a1) : make_pair(a1, a0));
+ return 2*aig_m;
+ }
+
+ int bit2aig(SigBit bit)
+ {
+ auto it = aig_map.find(bit);
+ if (it != aig_map.end()) {
+ log_assert(it->second >= 0);
+ return it->second;
+ }
+
+ // NB: Cannot use iterator returned from aig_map.insert()
+ // since this function is called recursively
+
+ int a = -1;
+ if (not_map.count(bit)) {
+ a = bit2aig(not_map.at(bit)) ^ 1;
+ } else
+ if (and_map.count(bit)) {
+ auto args = and_map.at(bit);
+ int a0 = bit2aig(args.first);
+ int a1 = bit2aig(args.second);
+ a = mkgate(a0, a1);
+ } else
+ if (alias_map.count(bit)) {
+ a = bit2aig(alias_map.at(bit));
+ }
+
+ if (bit == State::Sx || bit == State::Sz) {
+ log_debug("Design contains 'x' or 'z' bits. Treating as 1'b0.\n");
+ a = aig_map.at(State::S0);
+ }
+
+ log_assert(a >= 0);
+ aig_map[bit] = a;
+ return a;
+ }
+
+ XAigerWriter(Module *module, bool holes_mode=false) : module(module), sigmap(module)
+ {
+ pool<SigBit> undriven_bits;
+ pool<SigBit> unused_bits;
+ pool<SigBit> keep_bits;
+
+ // promote public wires
+ for (auto wire : module->wires())
+ if (wire->name[0] == '\\')
+ sigmap.add(wire);
+
+ // promote input wires
+ for (auto wire : module->wires())
+ if (wire->port_input)
+ sigmap.add(wire);
+
+ // promote output wires
+ for (auto wire : module->wires())
+ if (wire->port_output)
+ sigmap.add(wire);
+
+ for (auto wire : module->wires())
+ {
+ bool keep = wire->attributes.count("\\keep");
+
+ for (int i = 0; i < GetSize(wire); i++)
+ {
+ SigBit wirebit(wire, i);
+ SigBit bit = sigmap(wirebit);
+
+ if (bit.wire) {
+ undriven_bits.insert(bit);
+ unused_bits.insert(bit);
+ }
+
+ if (keep)
+ keep_bits.insert(bit);
+
+ if (wire->port_input || keep) {
+ if (bit != wirebit)
+ alias_map[bit] = wirebit;
+ input_bits.insert(wirebit);
+ }
+
+ if (wire->port_output || keep) {
+ if (bit != RTLIL::Sx) {
+ if (bit != wirebit)
+ alias_map[wirebit] = bit;
+ output_bits.insert(wirebit);
+ }
+ else
+ log_debug("Skipping PO '%s' driven by 1'bx\n", log_signal(wirebit));
+ }
+ }
+ }
+
+ for (auto bit : input_bits)
+ undriven_bits.erase(sigmap(bit));
+ for (auto bit : output_bits)
+ if (!bit.wire->port_input)
+ unused_bits.erase(bit);
+
+ // TODO: Speed up toposort -- ultimately we care about
+ // box ordering, but not individual AIG cells
+ dict<SigBit, pool<IdString>> bit_drivers, bit_users;
+ TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
+ bool abc_box_seen = false;
+
+ for (auto cell : module->selected_cells()) {
+ if (cell->type == "$_NOT_")
+ {
+ SigBit A = sigmap(cell->getPort("\\A").as_bit());
+ SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+ unused_bits.erase(A);
+ undriven_bits.erase(Y);
+ not_map[Y] = A;
+ if (!holes_mode) {
+ toposort.node(cell->name);
+ bit_users[A].insert(cell->name);
+ bit_drivers[Y].insert(cell->name);
+ }
+ continue;
+ }
+
+ if (cell->type == "$_AND_")
+ {
+ SigBit A = sigmap(cell->getPort("\\A").as_bit());
+ SigBit B = sigmap(cell->getPort("\\B").as_bit());
+ SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+ unused_bits.erase(A);
+ unused_bits.erase(B);
+ undriven_bits.erase(Y);
+ and_map[Y] = make_pair(A, B);
+ if (!holes_mode) {
+ toposort.node(cell->name);
+ bit_users[A].insert(cell->name);
+ bit_users[B].insert(cell->name);
+ bit_drivers[Y].insert(cell->name);
+ }
+ continue;
+ }
+
+ log_assert(!holes_mode);
+
+ RTLIL::Module* inst_module = module->design->module(cell->type);
+ if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
+ abc_box_seen = true;
+
+ if (!holes_mode) {
+ toposort.node(cell->name);
+ for (const auto &conn : cell->connections()) {
+ auto port_wire = inst_module->wire(conn.first);
+ if (port_wire->port_input) {
+ // Ignore inout for the sake of topographical ordering
+ if (port_wire->port_output) continue;
+ for (auto bit : sigmap(conn.second))
+ bit_users[bit].insert(cell->name);
+ }
+
+ if (port_wire->port_output)
+ for (auto bit : sigmap(conn.second))
+ bit_drivers[bit].insert(cell->name);
+ }
+ }
+ }
+ else {
+ bool cell_known = inst_module || cell->known();
+ for (const auto &c : cell->connections()) {
+ if (c.second.is_fully_const()) continue;
+ auto port_wire = inst_module ? inst_module->wire(c.first) : nullptr;
+ auto is_input = (port_wire && port_wire->port_input) || !cell_known || cell->input(c.first);
+ auto is_output = (port_wire && port_wire->port_output) || !cell_known || cell->output(c.first);
+ if (!is_input && !is_output)
+ log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
+
+ if (is_input) {
+ for (auto b : c.second) {
+ Wire *w = b.wire;
+ if (!w) continue;
+ if (!w->port_output || !cell_known) {
+ SigBit I = sigmap(b);
+ if (I != b)
+ alias_map[b] = I;
+ output_bits.insert(b);
+ unused_bits.erase(b);
+
+ if (!cell_known)
+ keep_bits.insert(b);
+ }
+ }
+ }
+ if (is_output) {
+ int arrival = 0;
+ if (port_wire) {
+ auto it = port_wire->attributes.find("\\abc_arrival");
+ if (it != port_wire->attributes.end()) {
+ if (it->second.flags != 0)
+ log_error("Attribute 'abc_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
+ arrival = it->second.as_int();
+ }
+ }
+
+ for (auto b : c.second) {
+ Wire *w = b.wire;
+ if (!w) continue;
+ input_bits.insert(b);
+ SigBit O = sigmap(b);
+ if (O != b)
+ alias_map[O] = b;
+ undriven_bits.erase(O);
+
+ if (arrival)
+ arrival_times[b] = arrival;
+ }
+ }
+ }
+ }
+
+ //log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
+ }
+
+ if (abc_box_seen) {
+ for (auto &it : bit_users)
+ if (bit_drivers.count(it.first))
+ for (auto driver_cell : bit_drivers.at(it.first))
+ for (auto user_cell : it.second)
+ toposort.edge(driver_cell, user_cell);
+
+#if 0
+ toposort.analyze_loops = true;
+#endif
+ bool no_loops YS_ATTRIBUTE(unused) = toposort.sort();
+#if 0
+ unsigned i = 0;
+ for (auto &it : toposort.loops) {
+ log(" loop %d\n", i++);
+ for (auto cell_name : it) {
+ auto cell = module->cell(cell_name);
+ log_assert(cell);
+ log("\t%s (%s @ %s)\n", log_id(cell), log_id(cell->type), cell->get_src_attribute().c_str());
+ }
+ }
+#endif
+ log_assert(no_loops);
+
+ for (auto cell_name : toposort.sorted) {
+ RTLIL::Cell *cell = module->cell(cell_name);
+ log_assert(cell);
+
+ RTLIL::Module* box_module = module->design->module(cell->type);
+ if (!box_module || !box_module->attributes.count("\\abc_box_id"))
+ continue;
+
+ // Fully pad all unused input connections of this box cell with S0
+ // Fully pad all undriven output connections of this box cell with anonymous wires
+ // NB: Assume box_module->ports are sorted alphabetically
+ // (as RTLIL::Module::fixup_ports() would do)
+ for (const auto &port_name : box_module->ports) {
+ RTLIL::Wire* w = box_module->wire(port_name);
+ log_assert(w);
+ auto it = cell->connections_.find(port_name);
+ if (w->port_input) {
+ RTLIL::SigSpec rhs;
+ if (it != cell->connections_.end()) {
+ if (GetSize(it->second) < GetSize(w))
+ it->second.append(RTLIL::SigSpec(State::S0, GetSize(w)-GetSize(it->second)));
+ rhs = it->second;
+ }
+ else {
+ rhs = RTLIL::SigSpec(State::S0, GetSize(w));
+ cell->setPort(port_name, rhs);
+ }
+
+ int offset = 0;
+ for (auto b : rhs.bits()) {
+ SigBit I = sigmap(b);
+ if (b == RTLIL::Sx)
+ b = State::S0;
+ else if (I != b) {
+ if (I == RTLIL::Sx)
+ alias_map[b] = State::S0;
+ else
+ alias_map[b] = I;
+ }
+ co_bits.emplace_back(b, cell, port_name, offset++, 0);
+ unused_bits.erase(b);
+ }
+ }
+ if (w->port_output) {
+ RTLIL::SigSpec rhs;
+ auto it = cell->connections_.find(w->name);
+ if (it != cell->connections_.end()) {
+ if (GetSize(it->second) < GetSize(w))
+ it->second.append(module->addWire(NEW_ID, GetSize(w)-GetSize(it->second)));
+ rhs = it->second;
+ }
+ else {
+ rhs = module->addWire(NEW_ID, GetSize(w));
+ cell->setPort(port_name, rhs);
+ }
+
+ int offset = 0;
+ for (const auto &b : rhs.bits()) {
+ ci_bits.emplace_back(b, cell, port_name, offset++);
+ SigBit O = sigmap(b);
+ if (O != b)
+ alias_map[O] = b;
+ undriven_bits.erase(O);
+
+ auto jt = input_bits.find(b);
+ if (jt != input_bits.end()) {
+ log_assert(keep_bits.count(O));
+ input_bits.erase(b);
+ }
+ }
+ }
+ }
+ box_list.emplace_back(cell);
+ }
+
+ // TODO: Free memory from toposort, bit_drivers, bit_users
+ }
+
+ for (auto bit : input_bits) {
+ if (!output_bits.count(bit))
+ continue;
+ RTLIL::Wire *wire = bit.wire;
+ // If encountering an inout port, or a keep-ed wire, then create a new wire
+ // with $inout.out suffix, make it a PO driven by the existing inout, and
+ // inherit existing inout's drivers
+ if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
+ || keep_bits.count(bit)) {
+ RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
+ RTLIL::Wire *new_wire = module->wire(wire_name);
+ if (!new_wire)
+ new_wire = module->addWire(wire_name, GetSize(wire));
+ SigBit new_bit(new_wire, bit.offset);
+ module->connect(new_bit, bit);
+ if (not_map.count(bit)) {
+ auto a = not_map.at(bit);
+ not_map[new_bit] = a;
+ }
+ else if (and_map.count(bit)) {
+ auto a = and_map.at(bit);
+ and_map[new_bit] = a;
+ }
+ else if (alias_map.count(bit)) {
+ auto a = alias_map.at(bit);
+ alias_map[new_bit] = a;
+ }
+ else
+ alias_map[new_bit] = bit;
+ output_bits.erase(bit);
+ output_bits.insert(new_bit);
+ }
+ }
+
+ for (auto bit : unused_bits)
+ undriven_bits.erase(bit);
+
+ if (!undriven_bits.empty() && !holes_mode) {
+ undriven_bits.sort();
+ for (auto bit : undriven_bits) {
+ log_warning("Treating undriven bit %s.%s like $anyseq.\n", log_id(module), log_signal(bit));
+ input_bits.insert(bit);
+ }
+ log_warning("Treating a total of %d undriven bits in %s like $anyseq.\n", GetSize(undriven_bits), log_id(module));
+ }
+
+ if (holes_mode) {
+ struct sort_by_port_id {
+ bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
+ return a.wire->port_id < b.wire->port_id;
+ }
+ };
+ input_bits.sort(sort_by_port_id());
+ output_bits.sort(sort_by_port_id());
+ }
+ else {
+ input_bits.sort();
+ output_bits.sort();
+ }
+
+ not_map.sort();
+ and_map.sort();
+
+ aig_map[State::S0] = 0;
+ aig_map[State::S1] = 1;
+
+ for (auto bit : input_bits) {
+ aig_m++, aig_i++;
+ log_assert(!aig_map.count(bit));
+ aig_map[bit] = 2*aig_m;
+ }
+
+ for (auto &c : ci_bits) {
+ RTLIL::SigBit bit = std::get<0>(c);
+ aig_m++, aig_i++;
+ aig_map[bit] = 2*aig_m;
+ }
+
+ for (auto &c : co_bits) {
+ RTLIL::SigBit bit = std::get<0>(c);
+ std::get<4>(c) = ordered_outputs[bit] = aig_o++;
+ aig_outputs.push_back(bit2aig(bit));
+ }
+
+ if (output_bits.empty()) {
+ output_bits.insert(State::S0);
+ omode = true;
+ }
+
+ for (auto bit : output_bits) {
+ ordered_outputs[bit] = aig_o++;
+ aig_outputs.push_back(bit2aig(bit));
+ }
+
+ }
+
+ void write_aiger(std::ostream &f, bool ascii_mode)
+ {
+ int aig_obc = aig_o;
+ int aig_obcj = aig_obc;
+ int aig_obcjf = aig_obcj;
+
+ log_assert(aig_m == aig_i + aig_l + aig_a);
+ log_assert(aig_obcjf == GetSize(aig_outputs));
+
+ f << stringf("%s %d %d %d %d %d", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_o, aig_a);
+ f << stringf("\n");
+
+ if (ascii_mode)
+ {
+ for (int i = 0; i < aig_i; i++)
+ f << stringf("%d\n", 2*i+2);
+
+ for (int i = 0; i < aig_obc; i++)
+ f << stringf("%d\n", aig_outputs.at(i));
+
+ for (int i = aig_obc; i < aig_obcj; i++)
+ f << stringf("1\n");
+
+ for (int i = aig_obc; i < aig_obcj; i++)
+ f << stringf("%d\n", aig_outputs.at(i));
+
+ for (int i = aig_obcj; i < aig_obcjf; i++)
+ f << stringf("%d\n", aig_outputs.at(i));
+
+ for (int i = 0; i < aig_a; i++)
+ f << stringf("%d %d %d\n", 2*(aig_i+aig_l+i)+2, aig_gates.at(i).first, aig_gates.at(i).second);
+ }
+ else
+ {
+ for (int i = 0; i < aig_obc; i++)
+ f << stringf("%d\n", aig_outputs.at(i));
+
+ for (int i = aig_obc; i < aig_obcj; i++)
+ f << stringf("1\n");
+
+ for (int i = aig_obc; i < aig_obcj; i++)
+ f << stringf("%d\n", aig_outputs.at(i));
+
+ for (int i = aig_obcj; i < aig_obcjf; i++)
+ f << stringf("%d\n", aig_outputs.at(i));
+
+ for (int i = 0; i < aig_a; i++) {
+ int lhs = 2*(aig_i+aig_l+i)+2;
+ int rhs0 = aig_gates.at(i).first;
+ int rhs1 = aig_gates.at(i).second;
+ int delta0 = lhs - rhs0;
+ int delta1 = rhs0 - rhs1;
+ aiger_encode(f, delta0);
+ aiger_encode(f, delta1);
+ }
+ }
+
+ f << "c";
+
+ log_assert(!output_bits.empty());
+ auto write_buffer = [](std::stringstream &buffer, int i32) {
+ int32_t i32_be = to_big_endian(i32);
+ buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
+ };
+ std::stringstream h_buffer;
+ auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
+ write_h_buffer(1);
+ log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
+ write_h_buffer(input_bits.size() + ci_bits.size());
+ log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
+ write_h_buffer(output_bits.size() + GetSize(co_bits));
+ log_debug("piNum = %d\n", GetSize(input_bits));
+ write_h_buffer(input_bits.size());
+ log_debug("poNum = %d\n", GetSize(output_bits));
+ write_h_buffer(output_bits.size());
+ log_debug("boxNum = %d\n", GetSize(box_list));
+ write_h_buffer(box_list.size());
+
+ auto write_buffer_float = [](std::stringstream &buffer, float f32) {
+ buffer.write(reinterpret_cast<const char*>(&f32), sizeof(f32));
+ };
+ std::stringstream i_buffer;
+ auto write_i_buffer = std::bind(write_buffer_float, std::ref(i_buffer), std::placeholders::_1);
+ for (auto bit : input_bits)
+ write_i_buffer(arrival_times.at(bit, 0));
+ //std::stringstream o_buffer;
+ //auto write_o_buffer = std::bind(write_buffer_float, std::ref(o_buffer), std::placeholders::_1);
+ //for (auto bit : output_bits)
+ // write_o_buffer(0);
+
+ if (!box_list.empty()) {
+ RTLIL::Module *holes_module = module->design->addModule("$__holes__");
+ log_assert(holes_module);
+
+ int port_id = 1;
+ int box_count = 0;
+ for (auto cell : box_list) {
+ RTLIL::Module* box_module = module->design->module(cell->type);
+ int box_inputs = 0, box_outputs = 0;
+ Cell *holes_cell = nullptr;
+ if (box_module->get_bool_attribute("\\whitebox")) {
+ holes_cell = holes_module->addCell(cell->name, cell->type);
+ holes_cell->parameters = cell->parameters;
+ }
+
+ // NB: Assume box_module->ports are sorted alphabetically
+ // (as RTLIL::Module::fixup_ports() would do)
+ for (const auto &port_name : box_module->ports) {
+ RTLIL::Wire *w = box_module->wire(port_name);
+ log_assert(w);
+ RTLIL::Wire *holes_wire;
+ RTLIL::SigSpec port_wire;
+ if (w->port_input) {
+ for (int i = 0; i < GetSize(w); i++) {
+ box_inputs++;
+ holes_wire = holes_module->wire(stringf("\\i%d", box_inputs));
+ if (!holes_wire) {
+ holes_wire = holes_module->addWire(stringf("\\i%d", box_inputs));
+ holes_wire->port_input = true;
+ holes_wire->port_id = port_id++;
+ holes_module->ports.push_back(holes_wire->name);
+ }
+ if (holes_cell)
+ port_wire.append(holes_wire);
+ }
+ if (!port_wire.empty())
+ holes_cell->setPort(w->name, port_wire);
+ }
+ if (w->port_output) {
+ box_outputs += GetSize(w);
+ for (int i = 0; i < GetSize(w); i++) {
+ if (GetSize(w) == 1)
+ holes_wire = holes_module->addWire(stringf("%s.%s", cell->name.c_str(), w->name.c_str()));
+ else
+ holes_wire = holes_module->addWire(stringf("%s.%s[%d]", cell->name.c_str(), w->name.c_str(), i));
+ holes_wire->port_output = true;
+ holes_wire->port_id = port_id++;
+ holes_module->ports.push_back(holes_wire->name);
+ if (holes_cell)
+ port_wire.append(holes_wire);
+ else
+ holes_module->connect(holes_wire, State::S0);
+ }
+ if (!port_wire.empty())
+ holes_cell->setPort(w->name, port_wire);
+ }
+ }
+
+ write_h_buffer(box_inputs);
+ write_h_buffer(box_outputs);
+ write_h_buffer(box_module->attributes.at("\\abc_box_id").as_int());
+ write_h_buffer(box_count++);
+ }
+
+ std::stringstream r_buffer;
+ auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
+ write_r_buffer(0);
+ f << "r";
+ std::string buffer_str = r_buffer.str();
+ int32_t buffer_size_be = to_big_endian(buffer_str.size());
+ f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ f.write(buffer_str.data(), buffer_str.size());
+
+ if (holes_module) {
+ log_push();
+
+ // NB: fixup_ports() will sort ports by name
+ //holes_module->fixup_ports();
+ holes_module->check();
+
+ holes_module->design->selection_stack.emplace_back(false);
+ RTLIL::Selection& sel = holes_module->design->selection_stack.back();
+ sel.select(holes_module);
+
+ // TODO: Should not need to opt_merge if we only instantiate
+ // each box type once...
+ Pass::call(holes_module->design, "opt_merge -share_all");
+
+ Pass::call(holes_module->design, "flatten -wb");
+
+ // TODO: Should techmap/aigmap/check all lib_whitebox-es just once,
+ // instead of per write_xaiger call
+ Pass::call(holes_module->design, "techmap");
+ Pass::call(holes_module->design, "aigmap");
+ for (auto cell : holes_module->cells())
+ if (!cell->type.in("$_NOT_", "$_AND_"))
+ log_error("Whitebox contents cannot be represented as AIG. Please verify whiteboxes are synthesisable.\n");
+
+ holes_module->design->selection_stack.pop_back();
+
+ // Move into a new (temporary) design so that "clean" will only
+ // operate (and run checks on) this one module
+ RTLIL::Design *holes_design = new RTLIL::Design;
+ holes_module->design->modules_.erase(holes_module->name);
+ holes_design->add(holes_module);
+ Pass::call(holes_design, "clean -purge");
+
+ std::stringstream a_buffer;
+ XAigerWriter writer(holes_module, true /* holes_mode */);
+ writer.write_aiger(a_buffer, false /*ascii_mode*/);
+
+ delete holes_design;
+
+ f << "a";
+ std::string buffer_str = a_buffer.str();
+ int32_t buffer_size_be = to_big_endian(buffer_str.size());
+ f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ f.write(buffer_str.data(), buffer_str.size());
+
+ log_pop();
+ }
+ }
+
+ f << "h";
+ std::string buffer_str = h_buffer.str();
+ int32_t buffer_size_be = to_big_endian(buffer_str.size());
+ f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ f.write(buffer_str.data(), buffer_str.size());
+
+ f << "i";
+ buffer_str = i_buffer.str();
+ buffer_size_be = to_big_endian(buffer_str.size());
+ f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ f.write(buffer_str.data(), buffer_str.size());
+ //f << "o";
+ //buffer_str = o_buffer.str();
+ //buffer_size_be = to_big_endian(buffer_str.size());
+ //f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+ //f.write(buffer_str.data(), buffer_str.size());
+
+ f << stringf("Generated by %s\n", yosys_version_str);
+ }
+
+ void write_map(std::ostream &f, bool verbose_map)
+ {
+ dict<int, string> input_lines;
+ dict<int, string> output_lines;
+ dict<int, string> wire_lines;
+
+ for (auto wire : module->wires())
+ {
+ //if (!verbose_map && wire->name[0] == '$')
+ // continue;
+
+ SigSpec sig = sigmap(wire);
+
+ for (int i = 0; i < GetSize(wire); i++)
+ {
+ RTLIL::SigBit b(wire, i);
+ if (input_bits.count(b)) {
+ int a = aig_map.at(b);
+ log_assert((a & 1) == 0);
+ input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire));
+ }
+
+ if (output_bits.count(b)) {
+ int o = ordered_outputs.at(b);
+ output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), i, log_id(wire));
+ continue;
+ }
+
+ if (verbose_map) {
+ if (aig_map.count(sig[i]) == 0)
+ continue;
+
+ int a = aig_map.at(sig[i]);
+ wire_lines[a] += stringf("wire %d %d %s\n", a, i, log_id(wire));
+ }
+ }
+ }
+
+ input_lines.sort();
+ for (auto &it : input_lines)
+ f << it.second;
+ log_assert(input_lines.size() == input_bits.size());
+
+ int box_count = 0;
+ for (auto cell : box_list)
+ f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name));
+
+ output_lines.sort();
+ if (omode)
+ output_lines[State::S0] = "output 0 0 $__dummy__\n";
+ for (auto &it : output_lines)
+ f << it.second;
+ log_assert(output_lines.size() == output_bits.size());
+
+ wire_lines.sort();
+ for (auto &it : wire_lines)
+ f << it.second;
+ }
+};
+
+struct XAigerBackend : public Backend {
+ XAigerBackend() : Backend("xaiger", "write design to XAIGER file") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" write_xaiger [options] [filename]\n");
+ log("\n");
+ log("Write the current design to an XAIGER file. The design must be flattened and\n");
+ log("all unsupported cells will be converted into psuedo-inputs and pseudo-outputs.\n");
+ log("\n");
+ log(" -ascii\n");
+ log(" write ASCII version of AIGER format\n");
+ log("\n");
+ log(" -map <filename>\n");
+ log(" write an extra file with port and latch symbols\n");
+ log("\n");
+ log(" -vmap <filename>\n");
+ log(" like -map, but more verbose\n");
+ log("\n");
+ }
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ bool ascii_mode = false;
+ bool verbose_map = false;
+ std::string map_filename;
+
+ log_header(design, "Executing XAIGER backend.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-ascii") {
+ ascii_mode = true;
+ continue;
+ }
+ if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) {
+ map_filename = args[++argidx];
+ continue;
+ }
+ if (map_filename.empty() && args[argidx] == "-vmap" && argidx+1 < args.size()) {
+ map_filename = args[++argidx];
+ verbose_map = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(f, filename, args, argidx);
+
+ Module *top_module = design->top_module();
+
+ if (top_module == nullptr)
+ log_error("Can't find top module in current design!\n");
+
+ XAigerWriter writer(top_module);
+ writer.write_aiger(*f, ascii_mode);
+
+ if (!map_filename.empty()) {
+ std::ofstream mapf;
+ mapf.open(map_filename.c_str(), std::ofstream::trunc);
+ if (mapf.fail())
+ log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
+ writer.write_map(mapf, verbose_map);
+ }
+ }
+} XAigerBackend;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index e4509e0d0..b6e38c16c 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;
@@ -327,6 +327,13 @@ struct BlifDumper
goto internal_cell;
}
+ if (!config->icells_mode && cell->type == "$_NMUX_") {
+ f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n",
+ cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
+ cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
+ goto internal_cell;
+ }
+
if (!config->icells_mode && cell->type == "$_FF_") {
f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
cstr_init(cell->getPort("\\Q")));
@@ -370,7 +377,7 @@ struct BlifDumper
f << stringf("\n");
RTLIL::SigSpec mask = cell->parameters.at("\\LUT");
for (int i = 0; i < (1 << width); i++)
- if (mask[i] == RTLIL::S1) {
+ if (mask[i] == State::S1) {
for (int j = width-1; j >= 0; j--) {
f << ((i>>j)&1 ? '1' : '0');
}
@@ -409,12 +416,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");
@@ -464,7 +485,7 @@ struct BlifDumper
struct BlifBackend : public Backend {
BlifBackend() : Backend("blif", "write design to BLIF file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -534,7 +555,7 @@ struct BlifBackend : public Backend {
log(" do not write definitions for the $true, $false and $undef wires.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::string top_module_name;
std::string buf_type, buf_in, buf_out;
@@ -640,7 +661,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 61a2f8ba3..4472993d4 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());
@@ -449,7 +496,7 @@ struct BtorWorker
goto okay;
}
- if (cell->type.in("$mux", "$_MUX_"))
+ if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
{
SigSpec sig_a = sigmap(cell->getPort("\\A"));
SigSpec sig_b = sigmap(cell->getPort("\\B"));
@@ -464,6 +511,12 @@ struct BtorWorker
int nid = next_nid++;
btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
+ if (cell->type == "$_NMUX_") {
+ int tmp = nid;
+ nid = next_nid++;
+ btorf("%d not %d %d\n", nid, sid, tmp);
+ }
+
add_nid_sig(nid, sig_y);
goto okay;
}
@@ -506,6 +559,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 +579,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));
@@ -559,8 +616,8 @@ struct BtorWorker
if (initstate_nid < 0)
{
int sid = get_bv_sid(1);
- int one_nid = get_sig_nid(Const(1, 1));
- int zero_nid = get_sig_nid(Const(0, 1));
+ int one_nid = get_sig_nid(State::S1);
+ int zero_nid = get_sig_nid(State::S0);
initstate_nid = next_nid++;
btorf("%d state %d\n", initstate_nid, sid);
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
@@ -575,6 +632,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 +659,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
+ {
+ 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 +713,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 +886,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 +1021,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)));
}
@@ -1076,7 +1204,7 @@ struct BtorWorker
struct BtorBackend : public Backend {
BtorBackend() : Backend("btor", "write design to BTOR file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -1091,7 +1219,7 @@ struct BtorBackend : public Backend {
log(" Output only a single bad property for all asserts\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
bool verbose = false, single_bad = false;
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index a6534b911..6d9469538 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -90,7 +90,7 @@ struct EdifNames
struct EdifBackend : public Backend {
EdifBackend() : Backend("edif", "write design to EDIF netlist file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -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");
@@ -116,13 +123,14 @@ struct EdifBackend : public Backend {
log("is targeted.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
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 06cbc9b2b..87db0edf7 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
@@ -32,6 +36,28 @@ pool<string> used_names;
dict<IdString, string> namecache;
int autoid_counter;
+typedef unsigned FDirection;
+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)
+{
+ Wire *wire = module->wires_.at(id);
+ FDirection direction = FD_NODIRECTION;
+ if (wire && wire->port_id)
+ {
+ if (wire->port_input)
+ direction |= FD_IN;
+ if (wire->port_output)
+ direction |= FD_OUT;
+ }
+ return direction;
+}
+
string next_id()
{
string new_id;
@@ -77,6 +103,127 @@ struct FirrtlWorker
dict<SigBit, pair<string, int>> reverse_wire_map;
string unconn_id;
+ 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(State::S0);
+ if (!ena.is_fully_def())
+ this->ena = SigSpec(State::S1);
+ }
+ 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)
{
@@ -84,11 +231,11 @@ struct FirrtlWorker
reverse_wire_map[sig[i]] = make_pair(id, i);
}
- FirrtlWorker(Module *module, std::ostream &f) : module(module), f(f)
+ FirrtlWorker(Module *module, std::ostream &f, RTLIL::Design *theDesign) : module(module), f(f), design(theDesign), indent(" ")
{
}
- string make_expr(SigSpec sig)
+ static string make_expr(const SigSpec &sig)
{
string expr;
@@ -135,6 +282,117 @@ struct FirrtlWorker
return expr;
}
+ std::string fid(RTLIL::IdString internal_id)
+ {
+ return make_id(internal_id);
+ }
+
+ std::string cellname(RTLIL::Cell *cell)
+ {
+ return fid(cell->name).c_str();
+ }
+
+ 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.begins_with("$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;
+ if (cell_name != fid(cell->name))
+ cell_name_comment = " /* " + fid(cell->name) + " */ ";
+ else
+ cell_name_comment = "";
+ // Find the module corresponding to this instance.
+ auto instModule = design->module(cell->type);
+ // 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 secondExpr = make_expr(secondSig);
+ // Find the direction for this port.
+ FDirection dir = getPortFDirection(it->first, instModule);
+ 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", cell_type.c_str(), log_signal(it->second));
+ /* FALLTHRU */
+ case FD_OUT:
+ sourceExpr = firstName;
+ sinkExpr = secondExpr;
+ sinkSig = &secondSig;
+ break;
+ case FD_NODIRECTION:
+ 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:
+ sourceExpr = secondExpr;
+ sinkExpr = firstName;
+ break;
+ default:
+ log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", cell_type.c_str(), log_signal(it->second), dir);
+ break;
+ }
+ // Check for subfield assignment.
+ std::string bitsString = "bits(";
+ if (sinkExpr.compare(0, bitsString.length(), bitsString) == 0) {
+ 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_width)
+ {
+ string result = b_expr;
+ if (b_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));
@@ -142,58 +400,90 @@ 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)
log_error("Module port %s.%s is inout!\n", log_id(module), log_id(wire));
port_decls.push_back(stringf(" %s %s: UInt<%d>\n", wire->port_input ? "input" : "output",
- make_id(wire->name), wire->width));
+ wireName, wire->width));
}
else
{
- wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", make_id(wire->name), wire->width));
+ wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", wireName, wire->width));
}
}
for (auto cell : module->cells())
{
+ static Const ndef(0, 0);
+
+ // Is this cell is a module instance?
+ if (cell->type[0] != '$')
+ {
+ process_instance(cell, wire_exprs);
+ continue;
+ }
+ // Not a module instance. Set up cell properties
+ bool extract_y_bits = false; // Assume no extraction of final bits will be required.
+ int a_width = cell->parameters.at("\\A_WIDTH", ndef).as_int(); // The width of "A"
+ int b_width = cell->parameters.at("\\B_WIDTH", ndef).as_int(); // The width of "A"
+ const int y_width = cell->parameters.at("\\Y_WIDTH", ndef).as_int(); // The width of the result
+ const bool a_signed = cell->parameters.at("\\A_SIGNED", ndef).as_bool();
+ const bool b_signed = cell->parameters.at("\\B_SIGNED", ndef).as_bool();
+ bool firrtl_is_signed = a_signed; // The result is signed (subsequent code may change this).
+ int firrtl_width = 0;
+ string primop;
+ bool always_uint = false;
+ string y_id = make_id(cell->name);
+
if (cell->type.in("$not", "$logic_not", "$neg", "$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_bool", "$reduce_xnor"))
{
- 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"));
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
- if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+ if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
}
- a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ // Don't use the results of logical operations (a single bit) to control padding
+ if (!(cell->type.in("$eq", "$eqx", "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$reduce_bool", "$logic_not") && y_width == 1) ) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ }
- string primop;
- bool always_uint = false;
+ // Assume the FIRRTL width is a single bit.
+ firrtl_width = 1;
if (cell->type == "$not") primop = "not";
- if (cell->type == "$neg") primop = "neg";
- if (cell->type == "$logic_not") {
+ else if (cell->type == "$neg") {
+ primop = "neg";
+ firrtl_is_signed = true; // Result of "neg" is signed (an SInt).
+ firrtl_width = a_width;
+ } 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") {
- primop = "neq";
- a_expr = stringf("%s, UInt(0)", a_expr.c_str());
- }
+ 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.
+ a_expr = stringf("%s, %cInt<%d>(0)", a_expr.c_str(), a_signed ? 'S' : 'U', a_width);
+ }
string expr = stringf("%s(%s)", primop.c_str(), a_expr.c_str());
- if ((is_signed && !always_uint))
+ if ((firrtl_is_signed && !always_uint))
expr = stringf("asUInt(%s)", expr.c_str());
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
@@ -201,99 +491,226 @@ 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"))
+ if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or", "$eq", "$eqx",
+ "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
+ "$logic_and", "$logic_or", "$pow"))
{
- 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"));
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
- if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+ if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
+ // Expand the "A" operand to the result width
+ if (a_width < y_width) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ a_width = y_width;
+ }
}
- if (cell->parameters.at("\\A_SIGNED").as_bool() & (cell->type != "$shr")) {
+ // Shift amount is always unsigned, and needn't be padded to result width,
+ // otherwise, we need to cast the b_expr appropriately
+ if (b_signed && !cell->type.in("$shr", "$sshr", "$shl", "$sshl", "$pow")) {
b_expr = "asSInt(" + b_expr + ")";
+ // Expand the "B" operand to the result width
+ if (b_width < y_width) {
+ b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+ b_width = y_width;
+ }
}
- a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
-
- if ((cell->type != "$shl") && (cell->type != "$sshl")) {
- b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
- }
-
- if (cell->parameters.at("\\A_SIGNED").as_bool() & (cell->type == "$shr")) {
- a_expr = "asUInt(" + a_expr + ")";
+ // For the arithmetic ops, expand operand widths to result widths befor performing the operation.
+ // This corresponds (according to iverilog) to what verilog compilers implement.
+ if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or"))
+ {
+ if (a_width < y_width) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ a_width = y_width;
+ }
+ if (b_width < y_width) {
+ b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+ b_width = y_width;
+ }
+ }
+ // Assume the FIRRTL width is the width of "A"
+ firrtl_width = a_width;
+ auto a_sig = cell->getPort("\\A");
+
+ if (cell->type == "$add") {
+ primop = "add";
+ firrtl_is_signed = a_signed | b_signed;
+ firrtl_width = max(a_width, b_width);
+ } else if (cell->type == "$sub") {
+ primop = "sub";
+ firrtl_is_signed = true;
+ int a_widthInc = (!a_signed && b_signed) ? 2 : (a_signed && !b_signed) ? 1 : 0;
+ int b_widthInc = (a_signed && !b_signed) ? 2 : (!a_signed && b_signed) ? 1 : 0;
+ firrtl_width = max(a_width + a_widthInc, b_width + b_widthInc);
+ } else if (cell->type == "$mul") {
+ primop = "mul";
+ firrtl_is_signed = a_signed | b_signed;
+ firrtl_width = a_width + b_width;
+ } else if (cell->type == "$div") {
+ primop = "div";
+ firrtl_is_signed = a_signed | b_signed;
+ firrtl_width = a_width;
+ } else if (cell->type == "$mod") {
+ primop = "rem";
+ firrtl_width = min(a_width, b_width);
+ } else if (cell->type == "$and") {
+ primop = "and";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
+ else if (cell->type == "$or" ) {
+ primop = "or";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
+ else if (cell->type == "$xor") {
+ primop = "xor";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
+ else if (cell->type == "$xnor") {
+ primop = "xnor";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
+ else if ((cell->type == "$eq") | (cell->type == "$eqx")) {
+ primop = "eq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if ((cell->type == "$ne") | (cell->type == "$nex")) {
+ primop = "neq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if (cell->type == "$gt") {
+ primop = "gt";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if (cell->type == "$ge") {
+ primop = "geq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if (cell->type == "$lt") {
+ primop = "lt";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if (cell->type == "$le") {
+ primop = "leq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ 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";
+ int shift_amount = b_sig.as_int();
+ b_expr = std::to_string(shift_amount);
+ firrtl_width = a_width + shift_amount;
+ } else {
+ primop = "dshl";
+ // Convert from FIRRTL left shift semantics.
+ b_expr = gen_dshl(b_expr, b_width);
+ firrtl_width = a_width + (1 << b_width) - 1;
+ }
+ }
+ 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";
+ int shift_amount = b_sig.as_int();
+ b_expr = std::to_string(shift_amount);
+ firrtl_width = max(1, a_width - shift_amount);
+ } else {
+ primop = "dshr";
+ firrtl_width = a_width;
+ }
+ // We'll need to do some special fixups if the source (and thus result) is signed.
+ if (firrtl_is_signed) {
+ // If this is a "logical" shift right, pretend the source is unsigned.
+ if (cell->type == "$shr") {
+ a_expr = "asUInt(" + a_expr + ")";
+ }
+ }
+ }
+ 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;
+ firrtl_width = 1;
+ }
+ else if ((cell->type == "$logic_or")) {
+ primop = "or";
+ a_expr = "neq(" + a_expr + ", UInt(0))";
+ b_expr = "neq(" + b_expr + ", UInt(0))";
+ always_uint = true;
+ firrtl_width = 1;
+ }
+ else if ((cell->type == "$pow")) {
+ if (a_sig.is_fully_const() && a_sig.as_int() == 2) {
+ // We'll convert this to a shift. To simplify things, change the a_expr to "1"
+ // so we can use b_expr directly as a shift amount.
+ // Only support 2 ** N (i.e., shift left)
+ // 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.
+ a_expr = firrtl_is_signed ? "SInt(1)" : "UInt(1)";
+ extract_y_bits = true;
+ // Is the shift amount constant?
+ auto b_sig = cell->getPort("\\B");
+ if (b_sig.is_fully_const()) {
+ primop = "shl";
+ int shiftAmount = b_sig.as_int();
+ if (shiftAmount < 0) {
+ log_error("Negative power exponent - %d: %s.%s\n", shiftAmount, log_id(module), log_id(cell));
+ }
+ b_expr = std::to_string(shiftAmount);
+ firrtl_width = a_width + shiftAmount;
+ } else {
+ primop = "dshl";
+ // Convert from FIRRTL left shift semantics.
+ b_expr = gen_dshl(b_expr, b_width);
+ firrtl_width = a_width + (1 << b_width) - 1;
+ }
+ } else {
+ log_error("Non power 2: %s.%s\n", log_id(module), log_id(cell));
+ }
}
-
- string primop;
- 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") {
- primop = "and";
- always_uint = true;
- }
- if (cell->type == "$or" ) {
- primop = "or";
- always_uint = true;
- }
- if (cell->type == "$xor") {
- primop = "xor";
- always_uint = true;
- }
- if ((cell->type == "$eq") | (cell->type == "$eqx")) {
- primop = "eq";
- always_uint = true;
- }
- if ((cell->type == "$ne") | (cell->type == "$nex")) {
- primop = "neq";
- always_uint = true;
- }
- if (cell->type == "$gt") {
- primop = "gt";
- always_uint = true;
- }
- if (cell->type == "$ge") {
- primop = "geq";
- always_uint = true;
- }
- if (cell->type == "$lt") {
- primop = "lt";
- always_uint = true;
- }
- 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")) {
- primop = "and";
- a_expr = "neq(" + a_expr + ", UInt(0))";
- b_expr = "neq(" + b_expr + ", UInt(0))";
- always_uint = true;
- }
- if ((cell->type == "$logic_or")) {
- primop = "or";
- a_expr = "neq(" + a_expr + ", UInt(0))";
- b_expr = "neq(" + b_expr + ", UInt(0))";
- always_uint = true;
- }
if (!cell->parameters.at("\\B_SIGNED").as_bool()) {
b_expr = "asUInt(" + b_expr + ")";
}
- string expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+ string expr;
+ // Deal with $xnor == ~^ (not xor)
+ if (primop == "xnor") {
+ expr = stringf("not(xor(%s, %s))", a_expr.c_str(), b_expr.c_str());
+ } else {
+ expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+ }
+
+ // Deal with FIRRTL's "shift widens" semantics, or the need to widen the FIRRTL result.
+ // If the operation is signed, the FIRRTL width will be 1 one bit larger.
+ if (extract_y_bits) {
+ expr = stringf("bits(%s, %d, 0)", expr.c_str(), y_width - 1);
+ } else if (firrtl_is_signed && (firrtl_width + 1) < y_width) {
+ expr = stringf("pad(%s, %d)", expr.c_str(), y_width);
+ }
- if ((is_signed && !always_uint) || cell->type.in("$sub"))
+ if ((firrtl_is_signed && !always_uint))
expr = stringf("asUInt(%s)", expr.c_str());
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
@@ -304,7 +721,6 @@ struct FirrtlWorker
if (cell->type.in("$mux"))
{
- string y_id = make_id(cell->name);
int width = cell->parameters.at("\\WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
string b_expr = make_expr(cell->getPort("\\B"));
@@ -325,6 +741,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();
@@ -341,33 +758,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++)
@@ -378,9 +786,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]);
@@ -389,13 +804,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;
}
@@ -405,19 +864,85 @@ struct FirrtlWorker
if (clkpol == false)
log_error("Negative edge clock on FF %s.%s.\n", log_id(module), log_id(cell));
- string q_id = make_id(cell->name);
int width = cell->parameters.at("\\WIDTH").as_int();
string expr = make_expr(cell->getPort("\\D"));
string clk_expr = "asClock(" + make_expr(cell->getPort("\\CLK")) + ")";
- wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s\n", q_id.c_str(), width, clk_expr.c_str()));
+ wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s\n", y_id.c_str(), width, clk_expr.c_str()));
- cell_exprs.push_back(stringf(" %s <= %s\n", q_id.c_str(), expr.c_str()));
- register_reverse_wire_map(q_id, cell->getPort("\\Q"));
+ cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
+ register_reverse_wire_map(y_id, cell->getPort("\\Q"));
continue;
}
+ // This may be a parameterized module - paramod.
+ if (cell->type.begins_with("$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 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 a_expr = make_expr(cell->getPort("\\A"));
+ string b_expr = make_expr(cell->getPort("\\B"));
+ auto b_string = b_expr.c_str();
+ 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_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;
+ }
+ if (cell->type == "$pos") {
+ // assign y = a;
+// printCell(cell);
+ string a_expr = make_expr(cell->getPort("\\A"));
+ // Verilog appears to treat the result as signed, so if the result is wider than "A",
+ // we need to pad.
+ if (a_width < y_width) {
+ a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+ }
+ wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+ cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), a_expr.c_str()));
+ register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+ continue;
+ }
log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
}
@@ -494,14 +1019,14 @@ struct FirrtlWorker
if (is_valid) {
if (make_unconn_id) {
wire_decls.push_back(stringf(" wire %s: UInt<1>\n", unconn_id.c_str()));
- cell_exprs.push_back(stringf(" %s is invalid\n", unconn_id.c_str()));
+ wire_decls.push_back(stringf(" %s is invalid\n", unconn_id.c_str()));
}
wire_exprs.push_back(stringf(" %s <= %s\n", make_id(wire->name), expr.c_str()));
} else {
if (make_unconn_id) {
unconn_id.clear();
}
- wire_exprs.push_back(stringf(" %s is invalid\n", make_id(wire->name)));
+ wire_decls.push_back(stringf(" %s is invalid\n", make_id(wire->name)));
}
}
@@ -515,6 +1040,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;
@@ -527,50 +1070,65 @@ struct FirrtlWorker
struct FirrtlBackend : public Backend {
FirrtlBackend() : Backend("firrtl", "write design to a FIRRTL file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
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");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ 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())
{
- FirrtlWorker worker(module, *f);
+ FirrtlWorker worker(module, *f, design);
worker.run();
}
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 1f7f12361..e06786220 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -40,8 +40,8 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
for (int i = 0; i < width; i++) {
log_assert(offset+i < (int)data.bits.size());
switch (data.bits[offset+i]) {
- case RTLIL::S0: break;
- case RTLIL::S1: val |= 1 << i; break;
+ case State::S0: break;
+ case State::S1: val |= 1 << i; break;
default: val = -1; break;
}
}
@@ -54,8 +54,8 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
for (int i = offset+width-1; i >= offset; i--) {
log_assert(i < (int)data.bits.size());
switch (data.bits[i]) {
- case RTLIL::S0: f << stringf("0"); break;
- case RTLIL::S1: f << stringf("1"); break;
+ case State::S0: f << stringf("0"); break;
+ case State::S1: f << stringf("1"); break;
case RTLIL::Sx: f << stringf("x"); break;
case RTLIL::Sz: f << stringf("z"); break;
case RTLIL::Sa: f << stringf("-"); break;
@@ -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");
@@ -382,7 +390,7 @@ PRIVATE_NAMESPACE_BEGIN
struct IlangBackend : public Backend {
IlangBackend() : Backend("ilang", "write design to ilang file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -395,7 +403,7 @@ struct IlangBackend : public Backend {
log(" only write selected parts of the design.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
bool selected = false;
@@ -422,7 +430,7 @@ struct IlangBackend : public Backend {
struct DumpPass : public Pass {
DumpPass() : Pass("dump", "print parts of the design in ilang format") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -445,7 +453,7 @@ struct DumpPass : public Pass {
log(" like -outfile but append instead of overwrite\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::string filename;
bool flag_m = false, flag_n = false, append = false;
@@ -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 34cb52fb4..809a0fa09 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -46,7 +46,7 @@ static std::string netname(std::set<std::string> &conntypes_code, std::set<std::
struct IntersynthBackend : public Backend {
IntersynthBackend() : Backend("intersynth", "write design to InterSynth netlist file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -71,7 +71,7 @@ struct IntersynthBackend : public Backend {
log("http://www.clifford.at/intersynth/\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
log_header(design, "Executing INTERSYNTH backend.\n");
log_push();
@@ -108,7 +108,7 @@ struct IntersynthBackend : public Backend {
if (f.fail())
log_error("Can't open lib file `%s'.\n", filename.c_str());
RTLIL::Design *lib = new RTLIL::Design;
- Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.substr(filename.size()-3) == ".il") ? "ilang" : "verilog");
+ Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "ilang" : "verilog"));
libs.push_back(lib);
}
@@ -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;
@@ -183,7 +183,7 @@ struct IntersynthBackend : public Backend {
if (param.second.bits.size() != 32) {
node_code += stringf(" %s '", RTLIL::id2cstr(param.first));
for (int i = param.second.bits.size()-1; i >= 0; i--)
- node_code += param.second.bits[i] == RTLIL::S1 ? "1" : "0";
+ node_code += param.second.bits[i] == State::S1 ? "1" : "0";
} else
node_code += stringf(" %s 0x%x", RTLIL::id2cstr(param.first), param.second.as_int());
}
diff --git a/backends/json/json.cc b/backends/json/json.cc
index d3b7077a2..107009ee4 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -83,18 +83,43 @@ struct JsonWriter
return str + " ]";
}
+ void write_parameter_value(const Const &value)
+ {
+ if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
+ string str = value.decode_string();
+ int state = 0;
+ for (char c : str) {
+ if (state == 0) {
+ if (c == '0' || c == '1' || c == 'x' || c == 'z')
+ state = 0;
+ else if (c == ' ')
+ state = 1;
+ else
+ state = 2;
+ } else if (state == 1 && c != ' ')
+ state = 2;
+ }
+ if (state < 2)
+ str += " ";
+ f << get_string(str);
+ } else
+ if (GetSize(value) == 32 && value.is_fully_def()) {
+ if ((value.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
+ f << stringf("%d", value.as_int());
+ else
+ f << stringf("%u", value.as_int());
+ } else {
+ f << get_string(value.as_string());
+ }
+ }
+
void write_parameters(const dict<IdString, Const> &parameters, bool for_module=false)
{
bool first = true;
for (auto &param : parameters) {
f << stringf("%s\n", first ? "" : ",");
f << stringf(" %s%s: ", for_module ? "" : " ", get_name(param.first).c_str());
- if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0)
- f << get_string(param.second.decode_string());
- else if (GetSize(param.second.bits) > 32)
- f << get_string(param.second.as_string());
- else
- f << stringf("%d", param.second.as_int());
+ write_parameter_value(param.second);
first = false;
}
}
@@ -124,6 +149,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;
@@ -187,6 +216,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");
@@ -250,7 +283,7 @@ struct JsonWriter
struct JsonBackend : public Backend {
JsonBackend() : Backend("json", "write design to a JSON file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -332,12 +365,13 @@ struct JsonBackend : public Backend {
log("Module and cell ports and nets can be single bit wide or vectors of multiple\n");
log("bits. Each individual signal bit is assigned a unique integer. The <bit_vector>\n");
log("values referenced above are vectors of this integers. Signal bits that are\n");
- log("connected to a constant driver are denoted as string \"0\" or \"1\" instead of\n");
- log("a number.\n");
+ log("connected to a constant driver are denoted as string \"0\", \"1\", \"x\", or\n");
+ log("\"z\" instead of a number.\n");
log("\n");
- log("Numeric parameter and attribute values up to 32 bits are written as decimal\n");
- log("values. Numbers larger than that are written as string holding the binary\n");
- log("representation of the value.\n");
+ log("Numeric 32-bit parameter and attribute values are written as decimal values.\n");
+ log("Bit verctors of different sizes, or ones containing 'x' or 'z' bits, are written\n");
+ log("as string holding the binary representation of the value. Strings are written\n");
+ log("as strings, with an appended blank in cases of strings of the form /[01xz]* */.\n");
log("\n");
log("For example the following Verilog code:\n");
log("\n");
@@ -458,7 +492,7 @@ struct JsonBackend : public Backend {
log("format. A program processing this format must ignore all unknown fields.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
bool aig_mode = false;
@@ -482,7 +516,7 @@ struct JsonBackend : public Backend {
struct JsonPass : public Pass {
JsonPass() : Pass("json", "write design in JSON format") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -499,7 +533,7 @@ struct JsonPass : public Pass {
log("See 'help write_json' for a description of the JSON format used.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::string filename;
bool aig_mode = false;
@@ -523,6 +557,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 9a6fedee7..fff110bb0 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;
@@ -231,7 +231,7 @@ struct ProtobufDesignSerializer
struct ProtobufBackend : public Backend {
ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -249,7 +249,7 @@ struct ProtobufBackend : public Backend {
log("Yosys source code distribution.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
bool aig_mode = false;
bool text_mode = false;
@@ -286,7 +286,7 @@ struct ProtobufBackend : public Backend {
struct ProtobufPass : public Pass {
ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -307,7 +307,7 @@ struct ProtobufPass : public Pass {
log("Yosys source code distribution.\n");
log("\n");
}
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::string filename;
bool aig_mode = false;
@@ -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/simplec.cc b/backends/simplec/simplec.cc
index c9656caff..54dbb84af 100644
--- a/backends/simplec/simplec.cc
+++ b/backends/simplec/simplec.cc
@@ -472,7 +472,7 @@ struct SimplecWorker
return;
}
- if (cell->type == "$_MUX_")
+ if (cell->type.in("$_MUX_", "$_NMUX_"))
{
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
@@ -484,7 +484,9 @@ struct SimplecWorker
string s_expr = s.wire ? util_get_bit(work->prefix + cid(s.wire->name), s.wire->width, s.offset) : s.data ? "1" : "0";
// casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933)
- string expr = stringf("%s ? (bool)%s : (bool)%s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
+ string expr = stringf("%s ? %s(bool)%s : %s(bool)%s", s_expr.c_str(),
+ cell->type == "$_NMUX_" ? "!" : "", b_expr.c_str(),
+ cell->type == "$_NMUX_" ? "!" : "", a_expr.c_str());
log_assert(y.wire);
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
@@ -742,13 +744,13 @@ struct SimplecWorker
struct SimplecBackend : public Backend {
SimplecBackend() : Backend("simplec", "convert design to simple C code") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" write_simplec [options] [filename]\n");
log("\n");
- log("Write simple C code for simulating the design. The C code writen can be used to\n");
+ log("Write simple C code for simulating the design. The C code written can be used to\n");
log("simulate the design in a C environment, but the purpose of this command is to\n");
log("generate code that works well with C-based formal verification.\n");
log("\n");
@@ -761,7 +763,7 @@ struct SimplecBackend : public Backend {
log("THIS COMMAND IS UNDER CONSTRUCTION\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
reserved_cids.clear();
id2cid.clear();
diff --git a/backends/simplec/test00_uut.v b/backends/simplec/test00_uut.v
index 744dbe9e3..92329a6f9 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 eacda2734..68394a909 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) $(CXX) -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 += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
+ $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.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 ca1ceacc7..081dcda99 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;
@@ -509,6 +510,7 @@ struct Smt2Worker
if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
+ if (cell->type == "$_NMUX_") return export_gate(cell, "(not (ite S B A))");
if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
@@ -554,7 +556,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');
}
@@ -597,7 +601,7 @@ struct Smt2Worker
if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
- if (cell->type == "$mux" || cell->type == "$pmux")
+ if (cell->type.in("$mux", "$pmux"))
{
int width = GetSize(cell->getPort("\\Y"));
std::string processed_expr = get_bv(cell->getPort("\\A"));
@@ -885,8 +889,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 +1105,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));
}
}
}
@@ -1251,7 +1262,7 @@ struct Smt2Worker
struct Smt2Backend : public Backend {
Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -1407,7 +1418,7 @@ struct Smt2Backend : public Backend {
log("from non-zero to zero in the test design.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::ifstream template_f;
bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
@@ -1465,7 +1476,7 @@ struct Smt2Backend : public Backend {
int indent = 0;
while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
indent++;
- if (line.substr(indent, 2) == "%%")
+ if (line.compare(indent, 2, "%%") == 0)
break;
*f << line << std::endl;
}
@@ -1533,7 +1544,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 6af2a5ac1..445a42e0d 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 1a8d2484c..bac68ac70 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -17,7 +17,9 @@
#
import sys, re, os, signal
-import resource, subprocess
+import subprocess
+if os.name == "posix":
+ import resource
from copy import deepcopy
from select import select
from time import time
@@ -27,12 +29,25 @@ from threading import Thread
# This is needed so that the recursive SMT2 S-expression parser
# does not run out of stack frames when parsing large expressions
-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))
+if os.name == "posix":
+ smtio_reclimit = 64 * 1024
+ if sys.getrecursionlimit() < smtio_reclimit:
+ sys.setrecursionlimit(smtio_reclimit)
+
+ 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:
+ try:
+ resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
+ except ValueError:
+ # couldn't get more stack, just run with what we have
+ pass
# currently running solvers (so we can kill them)
@@ -51,8 +66,9 @@ def force_shutdown(signum, frame):
os.kill(p.pid, signal.SIGTERM)
sys.exit(1)
+if os.name == "posix":
+ signal.signal(signal.SIGHUP, force_shutdown)
signal.signal(signal.SIGINT, force_shutdown)
-signal.signal(signal.SIGHUP, force_shutdown)
signal.signal(signal.SIGTERM, force_shutdown)
def except_hook(exctype, value, traceback):
@@ -154,19 +170,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":
@@ -763,7 +788,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])
@@ -1002,6 +1027,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)
@@ -1020,7 +1047,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":
@@ -1053,4 +1083,3 @@ class MkVcd:
print("b0 %s" % self.nets[path][0], file=self.f)
else:
print("b1 %s" % self.nets[path][0], file=self.f)
-
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 768969e6b..f755307bf 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()
{
@@ -61,7 +61,7 @@ struct SmvWorker
{
string name = stringf("_%s", id.c_str());
- if (name.substr(0, 2) == "_\\")
+ if (name.compare(0, 2, "_\\") == 0)
name = "_" + name.substr(2);
for (auto &c : name) {
@@ -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,56 @@ 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 == "$_NMUX_")
+ {
+ 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 +575,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 +665,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()) {
@@ -675,7 +701,7 @@ struct SmvWorker
struct SmvBackend : public Backend {
SmvBackend() : Backend("smv", "write design to SMV file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -693,7 +719,7 @@ struct SmvBackend : public Backend {
log("THIS COMMAND IS UNDER CONSTRUCTION\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::ifstream template_f;
bool verbose = false;
@@ -720,7 +746,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 4101cbf98..6738a4bbd 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -132,7 +132,7 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
struct SpiceBackend : public Backend {
SpiceBackend() : Backend("spice", "write design to SPICE netlist file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -161,7 +161,7 @@ struct SpiceBackend : public Backend {
log(" set the specified module as design top module\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::string top_module_name;
RTLIL::Module *top_module = NULL;
@@ -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 27b7edfff..796f18059 100644
--- a/backends/table/table.cc
+++ b/backends/table/table.cc
@@ -29,7 +29,7 @@ PRIVATE_NAMESPACE_BEGIN
struct TableBackend : public Backend {
TableBackend() : Backend("table", "write design as connectivity table") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -48,7 +48,7 @@ struct TableBackend : public Backend {
log("module inputs and outputs are output using cell type and port '-' and with\n");
log("'pi' (primary input) or 'po' (primary output) or 'pio' as direction.\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
log_header(design, "Executing TABLE backend.\n");
@@ -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);
@@ -109,7 +109,7 @@ struct TableBackend : public Backend {
else if (cell->output(conn.first))
*f << "out" << "\t";
else
- *f << "unkown" << "\t";
+ *f << "unknown" << "\t";
*f << log_signal(sigmap(conn.second)) << "\n";
}
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index b50dc12af..7b1db4776 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,16 @@ 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) {
+ // See IEEE 1364-2005 Clause 5.1.14.
+ f << "{0{1'b0}}";
+ return;
+ }
if (nostr)
goto dump_hex;
if ((data.flags & RTLIL::CONST_FLAG_STRING) == 0 || width != (int)data.bits.size()) {
@@ -167,9 +200,9 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
int32_t val = 0;
for (int i = offset+width-1; i >= offset; i--) {
log_assert(i < (int)data.bits.size());
- if (data.bits[i] != RTLIL::S0 && data.bits[i] != RTLIL::S1)
+ if (data.bits[i] != State::S0 && data.bits[i] != State::S1)
goto dump_hex;
- if (data.bits[i] == RTLIL::S1)
+ if (data.bits[i] == State::S1)
val |= 1 << (i - offset);
}
if (decimal)
@@ -186,11 +219,11 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
for (int i = offset; i < offset+width; i++) {
log_assert(i < (int)data.bits.size());
switch (data.bits[i]) {
- case RTLIL::S0: bin_digits.push_back('0'); break;
- case RTLIL::S1: bin_digits.push_back('1'); break;
+ case State::S0: bin_digits.push_back('0'); break;
+ case State::S1: bin_digits.push_back('1'); break;
case RTLIL::Sx: bin_digits.push_back('x'); break;
case RTLIL::Sz: bin_digits.push_back('z'); break;
- case RTLIL::Sa: bin_digits.push_back('z'); break;
+ case RTLIL::Sa: bin_digits.push_back('?'); break;
case RTLIL::Sm: log_error("Found marker state in final netlist.");
}
}
@@ -219,6 +252,12 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
hex_digits.push_back('z');
continue;
}
+ if (bit_3 == '?' || bit_2 == '?' || bit_1 == '?' || bit_0 == '?') {
+ if (bit_3 != '?' || bit_2 != '?' || bit_1 != '?' || bit_0 != '?')
+ goto dump_bin;
+ hex_digits.push_back('?');
+ continue;
+ }
int val = 8*(bit_3 - '0') + 4*(bit_2 - '0') + 2*(bit_1 - '0') + (bit_0 - '0');
hex_digits.push_back(val < 10 ? '0' + val : 'a' + val - 10);
}
@@ -234,17 +273,18 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
for (int i = offset+width-1; i >= offset; i--) {
log_assert(i < (int)data.bits.size());
switch (data.bits[i]) {
- case RTLIL::S0: f << stringf("0"); break;
- case RTLIL::S1: f << stringf("1"); break;
+ case State::S0: f << stringf("0"); break;
+ case State::S1: f << stringf("1"); break;
case RTLIL::Sx: f << stringf("x"); break;
case RTLIL::Sz: f << stringf("z"); break;
- case RTLIL::Sa: f << stringf("z"); break;
+ case RTLIL::Sa: f << stringf("?"); break;
case RTLIL::Sm: log_error("Found marker state in final netlist.");
}
}
}
} 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 +302,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 +354,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 +371,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)))
+ if (modattr && (it->second == State::S0 || it->second == Const(0)))
f << stringf(" 0 ");
- else if (modattr && (it->second == Const(1, 1) || it->second == Const(1)))
+ else if (modattr && (it->second == State::S1 || 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 +435,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)
@@ -511,6 +558,20 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type == "$_NMUX_") {
+ f << stringf("%s" "assign ", indent.c_str());
+ dump_sigspec(f, cell->getPort("\\Y"));
+ f << stringf(" = !(");
+ dump_cell_expr_port(f, cell, "S", false);
+ f << stringf(" ? ");
+ dump_attributes(f, "", cell->attributes, ' ');
+ dump_cell_expr_port(f, cell, "B", false);
+ f << stringf(" : ");
+ dump_cell_expr_port(f, cell, "A", false);
+ f << stringf(");\n");
+ return true;
+ }
+
if (cell->type.in("$_AOI3_", "$_OAI3_")) {
f << stringf("%s" "assign ", indent.c_str());
dump_sigspec(f, cell->getPort("\\Y"));
@@ -543,7 +604,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
- if (cell->type.substr(0, 6) == "$_DFF_")
+ if (cell->type.begins_with("$_DFF_"))
{
std::string reg_name = cellname(cell);
bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
@@ -584,7 +645,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
- if (cell->type.substr(0, 8) == "$_DFFSR_")
+ if (cell->type.begins_with("$_DFFSR_"))
{
char pol_c = cell->type[8], pol_s = cell->type[9], pol_r = cell->type[10];
@@ -678,13 +739,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"));
@@ -710,7 +803,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
- if (cell->type == "$pmux" || cell->type == "$pmux_safe")
+ if (cell->type == "$pmux")
{
int width = cell->parameters["\\WIDTH"].as_int();
int s_width = cell->getPort("\\S").size();
@@ -722,18 +815,17 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf("%s" " input [%d:0] s;\n", indent.c_str(), s_width-1);
dump_attributes(f, indent + " ", cell->attributes);
- if (cell->type != "$pmux_safe" && !noattr)
+ if (!noattr)
f << stringf("%s" " (* parallel_case *)\n", indent.c_str());
f << stringf("%s" " casez (s)", indent.c_str());
- if (cell->type != "$pmux_safe")
- f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+ f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
for (int i = 0; i < s_width; i++)
{
f << stringf("%s" " %d'b", indent.c_str(), s_width);
for (int j = s_width-1; j >= 0; j--)
- f << stringf("%c", j == i ? '1' : cell->type == "$pmux_safe" ? '0' : '?');
+ f << stringf("%c", j == i ? '1' : '?');
f << stringf(":\n");
f << stringf("%s" " %s = b[%d:%d];\n", indent.c_str(), func_name.c_str(), (i+1)*width-1, i*width);
@@ -757,6 +849,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());
@@ -779,6 +883,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
+ if (cell->type == "$lut")
+ {
+ f << stringf("%s" "assign ", indent.c_str());
+ dump_sigspec(f, cell->getPort("\\Y"));
+ f << stringf(" = ");
+ dump_const(f, cell->parameters.at("\\LUT"));
+ f << stringf(" >> ");
+ dump_attributes(f, "", cell->attributes, ' ');
+ dump_sigspec(f, cell->getPort("\\A"));
+ f << stringf(";\n");
+ return true;
+ }
+
if (cell->type == "$dffsr")
{
SigSpec sig_clk = cell->getPort("\\CLK");
@@ -832,7 +949,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}
- if (cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffe")
+ if (cell->type.in("$dff", "$adff", "$dffe"))
{
RTLIL::SigSpec sig_clk, sig_arst, sig_en, val_arst;
bool pol_clk, pol_arst = false, pol_en = false;
@@ -939,6 +1056,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());
@@ -947,7 +1065,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());
@@ -980,43 +1098,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()) );
{
- os << stringf("if (");
- dump_sigspec(os, sig_rd_en);
- os << stringf(") ");
+ 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());
+ }
+ {
+ 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)
@@ -1036,15 +1157,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);
}
}
@@ -1146,6 +1267,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
@@ -1168,8 +1401,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());
@@ -1216,12 +1448,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)
@@ -1274,12 +1514,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;
@@ -1338,6 +1580,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)
@@ -1398,14 +1642,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 proccesses. RTLIL processes\n"
+ 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)
@@ -1441,7 +1686,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++) {
@@ -1482,7 +1727,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
struct VerilogBackend : public Backend {
VerilogBackend() : Backend("verilog", "write design to Verilog file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
@@ -1508,9 +1753,13 @@ 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 decativates this feature and instead\n");
+ log(" not bit pattern. This option deactivates this feature and instead\n");
log(" will write out all constants in binary.\n");
log("\n");
log(" -decimal\n");
@@ -1518,13 +1767,13 @@ struct VerilogBackend : public Backend {
log("\n");
log(" -nohex\n");
log(" constant values that are compatible with hex output are usually\n");
- log(" dumped as hex values. This option decativates this feature and\n");
+ log(" dumped as hex values. This option deactivates this feature and\n");
log(" instead will write out all constants in binary.\n");
log("\n");
log(" -nostr\n");
log(" Parameters and attributes that are specified as strings in the\n");
log(" original input will be output as strings by this back-end. This\n");
- log(" decativates this feature and instead will write string constants\n");
+ log(" deactivates this feature and instead will write string constants\n");
log(" as binary numbers.\n");
log("\n");
log(" -defparam\n");
@@ -1550,7 +1799,7 @@ struct VerilogBackend : public Backend {
log("this command is called on a design with RTLIL processes.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
log_header(design, "Executing Verilog backend.\n");
@@ -1564,11 +1813,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");
@@ -1640,6 +1892,10 @@ struct VerilogBackend : public Backend {
decimal = true;
continue;
}
+ if (arg == "-siminit") {
+ siminit = true;
+ continue;
+ }
if (arg == "-blackboxes") {
blackboxes = true;
continue;
@@ -1660,7 +1916,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))
@@ -1671,6 +1927,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 2025-04-21 14:47:49 +0000