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.cc53
-rw-r--r--backends/aiger/xaiger.cc841
-rw-r--r--backends/blif/blif.cc9
-rw-r--r--backends/btor/btor.cc42
-rw-r--r--backends/firrtl/firrtl.cc308
-rw-r--r--backends/ilang/ilang_backend.cc13
-rw-r--r--backends/intersynth/intersynth.cc4
-rw-r--r--backends/json/json.cc58
-rw-r--r--backends/simplec/simplec.cc6
-rw-r--r--backends/smt2/smt2.cc5
-rw-r--r--backends/smt2/smtio.py11
-rw-r--r--backends/smv/smv.cc9
-rw-r--r--backends/verilog/verilog_backend.cc72
14 files changed, 1250 insertions, 182 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 d685c5638..7c851bb91 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -70,34 +70,35 @@ 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, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
@@ -685,7 +686,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");
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
new file mode 100644
index 000000000..77d0e94c2
--- /dev/null
+++ b/backends/aiger/xaiger.cc
@@ -0,0 +1,841 @@
+/*
+ * 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;
+
+ 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()) {
+ if (cell->input(conn.first)) {
+ // Ignore inout for the sake of topographical ordering
+ if (cell->output(conn.first)) continue;
+ for (auto bit : sigmap(conn.second))
+ bit_users[bit].insert(cell->name);
+ }
+
+ if (cell->output(conn.first))
+ for (auto bit : sigmap(conn.second))
+ bit_drivers[bit].insert(cell->name);
+ }
+ }
+ }
+ else {
+ bool cell_known = cell->known();
+ for (const auto &c : cell->connections()) {
+ if (c.second.is_fully_const()) continue;
+ auto is_input = !cell_known || cell->input(c.first);
+ auto is_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.bits()) {
+ 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) {
+ for (auto b : c.second.bits()) {
+ 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);
+ }
+ }
+ }
+ }
+
+ //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));
+ }
+
+ for (auto bit : output_bits) {
+ ordered_outputs[bit] = aig_o++;
+ aig_outputs.push_back(bit2aig(bit));
+ }
+
+ if (output_bits.empty()) {
+ aig_o++;
+ aig_outputs.push_back(0);
+ omode = true;
+ }
+ }
+
+ 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";
+
+ if (!box_list.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() + co_bits.size());
+ 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());
+
+ 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++);
+ }
+
+ 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());
+
+ 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";
+ buffer_str = r_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());
+
+ 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 << 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();
+ for (auto &it : output_lines)
+ f << it.second;
+ log_assert(output_lines.size() == output_bits.size());
+ if (omode && output_bits.empty())
+ f << "output " << output_lines.size() << " 0 $__dummy__\n";
+
+ 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 a1761b662..b6e38c16c 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -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');
}
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 511a11942..7c054d655 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"
@@ -491,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"));
@@ -506,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;
}
@@ -605,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);
@@ -875,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));
+ }
}
}
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 1c7a7351f..87db0edf7 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -122,9 +122,9 @@ struct FirrtlWorker
// Current (3/13/2019) conventions:
// generate a constant 0 for clock and a constant 1 for enable if they are undefined.
if (!clk.is_fully_def())
- this->clk = SigSpec(RTLIL::Const(0, 1));
+ this->clk = SigSpec(State::S0);
if (!ena.is_fully_def())
- this->ena = SigSpec(RTLIL::Const(1, 1));
+ this->ena = SigSpec(State::S1);
}
string gen_read(const char * indent) {
string addr_expr = make_expr(addr);
@@ -297,7 +297,7 @@ struct FirrtlWorker
std::string cell_type = fid(cell->type);
std::string instanceOf;
// If this is a parameterized module, its parent module is encoded in the cell type
- if (cell->type.substr(0, 8) == "$paramod")
+ if (cell->type.begins_with("$paramod"))
{
std::string::iterator it;
for (it = cell_type.begin(); it < cell_type.end(); it++)
@@ -363,7 +363,7 @@ struct FirrtlWorker
}
// Check for subfield assignment.
std::string bitsString = "bits(";
- if (sinkExpr.substr(0, bitsString.length()) == bitsString ) {
+ 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.
@@ -381,10 +381,10 @@ struct FirrtlWorker
// Given an expression for a shift amount, and a maximum width,
// generate the FIRRTL expression for equivalent dynamic shift taking into account FIRRTL shift semantics.
- std::string gen_dshl(const string b_expr, const int b_padded_width)
+ std::string gen_dshl(const string b_expr, const int b_width)
{
string result = b_expr;
- if (b_padded_width >= FIRRTL_MAX_DSH_WIDTH_ERROR) {
+ 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
@@ -422,22 +422,33 @@ struct FirrtlWorker
for (auto cell : module->cells())
{
- bool extract_y_bits = false; // Assume no extraction of final bits will be required.
+ 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 + ")";
}
@@ -446,12 +457,13 @@ struct FirrtlWorker
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";
else if (cell->type == "$neg") {
primop = "neg";
- is_signed = true; // Result of "neg" is signed (an SInt).
+ 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());
@@ -466,14 +478,12 @@ struct FirrtlWorker
else if (cell->type == "$reduce_bool") {
primop = "neq";
// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
- bool a_signed = cell->parameters.at("\\A_SIGNED").as_bool();
- int a_width = cell->parameters.at("\\A_WIDTH").as_int();
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()));
@@ -481,81 +491,121 @@ struct FirrtlWorker
continue;
}
- if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$and", "$or", "$eq", "$eqx",
+ 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"))
+ "$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"));
- int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
- if (cell->parameters.at("\\A_SIGNED").as_bool()) {
+ if (a_signed) {
a_expr = "asSInt(" + a_expr + ")";
- }
- // Shift amount is always unsigned, and needn't be padded to result width.
- if (!cell->type.in("$shr", "$sshr", "$shl", "$sshl")) {
- if (cell->parameters.at("\\B_SIGNED").as_bool()) {
- b_expr = "asSInt(" + b_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 (b_padded_width < y_width) {
- auto b_sig = cell->getPort("\\B");
- b_padded_width = y_width;
+ }
+ // 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;
}
}
+ // 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->parameters.at("\\A_SIGNED").as_bool() & (cell->type == "$shr")) {
- a_expr = "asUInt(" + a_expr + ")";
+ 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);
}
-
- string primop;
- bool always_uint = false;
- if (cell->type == "$add") primop = "add";
- else if (cell->type == "$sub") primop = "sub";
- else if (cell->type == "$mul") primop = "mul";
- else if (cell->type == "$div") primop = "div";
- else if (cell->type == "$mod") primop = "rem";
- else if (cell->type == "$and") {
- primop = "and";
- always_uint = true;
- }
else if (cell->type == "$or" ) {
- primop = "or";
- always_uint = true;
- }
+ primop = "or";
+ always_uint = true;
+ firrtl_width = max(a_width, b_width);
+ }
else if (cell->type == "$xor") {
- primop = "xor";
- always_uint = true;
- }
+ 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;
- }
+ primop = "eq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if ((cell->type == "$ne") | (cell->type == "$nex")) {
- primop = "neq";
- always_uint = true;
- }
+ primop = "neq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$gt") {
- primop = "gt";
- always_uint = true;
- }
+ primop = "gt";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$ge") {
- primop = "geq";
- always_uint = true;
- }
+ primop = "geq";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$lt") {
- primop = "lt";
- always_uint = true;
- }
+ primop = "lt";
+ always_uint = true;
+ firrtl_width = 1;
+ }
else if (cell->type == "$le") {
- primop = "leq";
- always_uint = true;
- }
+ 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.
@@ -564,11 +614,14 @@ struct FirrtlWorker
auto b_sig = cell->getPort("\\B");
if (b_sig.is_fully_const()) {
primop = "shl";
- b_expr = std::to_string(b_sig.as_int());
+ 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_padded_width);
+ b_expr = gen_dshl(b_expr, b_width);
+ firrtl_width = a_width + (1 << b_width) - 1;
}
}
else if ((cell->type == "$shr") | (cell->type == "$sshr")) {
@@ -578,36 +631,86 @@ struct FirrtlWorker
auto b_sig = cell->getPort("\\B");
if (b_sig.is_fully_const()) {
primop = "shr";
- b_expr = std::to_string(b_sig.as_int());
+ 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;
- }
+ 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;
- }
+ 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));
+ }
+ }
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
+ // 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()));
@@ -618,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"));
@@ -762,21 +864,20 @@ 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.substr(0, 8) == "$paramod")
+ if (cell->type.begins_with("$paramod"))
{
process_instance(cell, wire_exprs);
continue;
@@ -785,8 +886,6 @@ struct FirrtlWorker
// assign y = a[b +: y_width];
// We'll extract the correct bits as part of the primop.
- string y_id = make_id(cell->name);
- int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
// Get the initial bit selector
string b_expr = make_expr(cell->getPort("\\B"));
@@ -808,18 +907,15 @@ struct FirrtlWorker
// assign y = a >> b;
// where b may be negative
- string y_id = make_id(cell->name);
- int y_width = cell->parameters.at("\\Y_WIDTH").as_int();
string a_expr = make_expr(cell->getPort("\\A"));
string b_expr = make_expr(cell->getPort("\\B"));
auto b_string = b_expr.c_str();
- int b_padded_width = cell->parameters.at("\\B_WIDTH").as_int();
string expr;
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
if (cell->getParam("\\B_SIGNED").as_bool()) {
// We generate a left or right shift based on the sign of b.
- std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_padded_width).c_str(), y_width);
+ std::string 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,
@@ -833,7 +929,21 @@ struct FirrtlWorker
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
continue;
}
- log_warning("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
+ 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));
}
for (auto conn : module->connections())
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index b4ba2b03f..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;
@@ -204,6 +204,11 @@ 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)
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index b0e3cd252..809a0fa09 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -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);
}
@@ -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 5022d5da1..107009ee4 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -83,20 +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 if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) != 0)
- f << stringf("%d", param.second.as_int());
- else
- f << stringf("%u", param.second.as_int());
+ write_parameter_value(param.second);
first = false;
}
}
@@ -126,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;
@@ -189,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");
@@ -334,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");
diff --git a/backends/simplec/simplec.cc b/backends/simplec/simplec.cc
index 6f2ccbe20..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) +
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e318a4051..081dcda99 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -510,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)))");
@@ -600,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"));
@@ -1475,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;
}
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index cea0fc56c..bac68ac70 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -43,7 +43,11 @@ if os.name == "posix":
if current_rlimit_stack[1] != resource.RLIM_INFINITY:
smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
if current_rlimit_stack[0] < smtio_stacksize:
- resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
+ 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)
@@ -1043,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":
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index d75456c1b..f755307bf 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -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) {
@@ -537,6 +537,13 @@ struct SmvWorker
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_")
{
definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 827af5d85..7b1db4776 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -189,7 +189,8 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
if (width < 0)
width = data.bits.size() - offset;
if (width == 0) {
- f << "\"\"";
+ // See IEEE 1364-2005 Clause 5.1.14.
+ f << "{0{1'b0}}";
return;
}
if (nostr)
@@ -199,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)
@@ -218,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.");
}
}
@@ -251,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);
}
@@ -266,11 +273,11 @@ 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.");
}
}
@@ -364,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, attr2comment);
- f << stringf(" %s%c", attr2comment ? "*/" : "*)", term);
+ dump_const(f, it->second, -1, 0, false, as_comment);
+ f << stringf(" %s%c", as_comment ? "*/" : "*)", term);
}
}
@@ -549,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"));
@@ -581,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);
@@ -622,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];
@@ -780,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();
@@ -792,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);
@@ -927,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;
@@ -1492,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;
@@ -1662,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++) {
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 04:51:52 +0000