aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/aiger.cc25
-rw-r--r--backends/aiger/xaiger.cc31
-rw-r--r--backends/btor/btor.cc13
-rw-r--r--backends/cxxrtl/cxxrtl.h86
-rw-r--r--backends/cxxrtl/cxxrtl_backend.cc182
-rw-r--r--backends/firrtl/firrtl.cc6
-rw-r--r--backends/jny/Makefile.inc2
-rw-r--r--backends/jny/jny.cc554
-rw-r--r--backends/json/json.cc19
-rw-r--r--backends/rtlil/rtlil_backend.cc26
-rw-r--r--backends/smt2/smt2.cc40
-rw-r--r--backends/smt2/smtbmc.py202
-rw-r--r--backends/smt2/smtio.py22
-rw-r--r--backends/smv/smv.cc7
-rw-r--r--backends/verilog/verilog_backend.cc136
15 files changed, 1084 insertions, 267 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 35935b847..547d131ee 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -606,7 +606,7 @@ struct AigerWriter
f << stringf("c\nGenerated by %s\n", yosys_version_str);
}
- void write_map(std::ostream &f, bool verbose_map)
+ void write_map(std::ostream &f, bool verbose_map, bool no_startoffset)
{
dict<int, string> input_lines;
dict<int, string> init_lines;
@@ -627,32 +627,33 @@ struct AigerWriter
continue;
int a = aig_map.at(sig[i]);
+ int index = no_startoffset ? i : (wire->start_offset+i);
if (verbose_map)
- wire_lines[a] += stringf("wire %d %d %s\n", a, wire->start_offset+i, log_id(wire));
+ wire_lines[a] += stringf("wire %d %d %s\n", a, index, log_id(wire));
if (wire->port_input) {
log_assert((a & 1) == 0);
- input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
+ input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, index, log_id(wire));
}
if (wire->port_output) {
int o = ordered_outputs.at(sig[i]);
- output_lines[o] += stringf("output %d %d %s\n", o, wire->start_offset+i, log_id(wire));
+ output_lines[o] += stringf("output %d %d %s\n", o, index, log_id(wire));
}
if (init_inputs.count(sig[i])) {
int a = init_inputs.at(sig[i]);
log_assert((a & 1) == 0);
- init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire));
+ init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, index, log_id(wire));
}
if (ordered_latches.count(sig[i])) {
int l = ordered_latches.at(sig[i]);
if (zinit_mode && (aig_latchinit.at(l) == 1))
- latch_lines[l] += stringf("invlatch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
+ latch_lines[l] += stringf("invlatch %d %d %s\n", l, index, log_id(wire));
else
- latch_lines[l] += stringf("latch %d %d %s\n", l, wire->start_offset+i, log_id(wire));
+ latch_lines[l] += stringf("latch %d %d %s\n", l, index, log_id(wire));
}
}
}
@@ -713,6 +714,9 @@ struct AigerBackend : public Backend {
log(" -vmap <filename>\n");
log(" like -map, but more verbose\n");
log("\n");
+ log(" -no-startoffset\n");
+ log(" make indexes zero based, enable using map files with smt solvers.\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");
@@ -730,6 +734,7 @@ struct AigerBackend : public Backend {
bool omode = false;
bool bmode = false;
bool lmode = false;
+ bool no_startoffset = false;
std::string map_filename;
log_header(design, "Executing AIGER backend.\n");
@@ -762,6 +767,10 @@ struct AigerBackend : public Backend {
verbose_map = true;
continue;
}
+ if (args[argidx] == "-no-startoffset") {
+ no_startoffset = true;
+ continue;
+ }
if (args[argidx] == "-I") {
imode = true;
continue;
@@ -804,7 +813,7 @@ struct AigerBackend : public Backend {
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);
+ writer.write_map(mapf, verbose_map, no_startoffset);
}
}
} AigerBackend;
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 66955d88e..e223f185e 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -261,26 +261,27 @@ struct XAigerWriter
if (!timing.count(inst_module->name))
timing.setup_module(inst_module);
- auto &t = timing.at(inst_module->name).arrival;
- for (const auto &conn : cell->connections()) {
- auto port_wire = inst_module->wire(conn.first);
- if (!port_wire->port_output)
+
+ for (auto &i : timing.at(inst_module->name).arrival) {
+ if (!cell->hasPort(i.first.name))
continue;
- for (int i = 0; i < GetSize(conn.second); i++) {
- auto d = t.at(TimingInfo::NameBit(conn.first,i), 0);
- if (d == 0)
- continue;
+ auto port_wire = inst_module->wire(i.first.name);
+ log_assert(port_wire->port_output);
+
+ auto d = i.second.first;
+ if (d == 0)
+ continue;
+ auto offset = i.first.offset;
#ifndef NDEBUG
- if (ys_debug(1)) {
- static std::set<std::tuple<IdString,IdString,int>> seen;
- if (seen.emplace(inst_module->name, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
- log_id(cell->type), log_id(conn.first), i, d);
- }
-#endif
- arrival_times[conn.second[i]] = d;
+ if (ys_debug(1)) {
+ static pool<std::pair<IdString,TimingInfo::NameBit>> seen;
+ if (seen.emplace(inst_module->name, i.first).second) log("%s.%s[%d] abc9_arrival = %d\n",
+ log_id(cell->type), log_id(i.first.name), offset, d);
}
+#endif
+ arrival_times[cell->getPort(i.first.name)[offset]] = d;
}
if (abc9_flop)
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 6370b53bd..7de5deadd 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -678,7 +678,7 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
- btorf("%d state %d\n", nid, sid);
+ btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
@@ -699,7 +699,7 @@ struct BtorWorker
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 state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
}
@@ -865,7 +865,7 @@ struct BtorWorker
log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
- if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") {
+ if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") {
log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -1220,6 +1220,8 @@ struct BtorWorker
int this_nid = next_nid++;
btorf("%d uext %d %d %d%s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
+ if (info_clocks.count(nid))
+ info_clocks[this_nid] |= info_clocks[nid];
btorf_pop(stringf("wire %s", log_id(wire)));
continue;
@@ -1399,6 +1401,11 @@ struct BtorBackend : public Backend {
log_header(design, "Executing BTOR backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h
index 4552a0125..b4ffa87cd 100644
--- a/backends/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/cxxrtl.h
@@ -457,6 +457,42 @@ struct value : public expr_base<value<Bits>> {
return shr<AmountBits, /*Signed=*/true>(amount);
}
+ template<size_t ResultBits, size_t SelBits>
+ value<ResultBits> bmux(const value<SelBits> &sel) const {
+ static_assert(ResultBits << SelBits == Bits, "invalid sizes used in bmux()");
+ size_t amount = sel.data[0] * ResultBits;
+ size_t shift_chunks = amount / chunk::bits;
+ size_t shift_bits = amount % chunk::bits;
+ value<ResultBits> result;
+ chunk::type carry = 0;
+ if (ResultBits % chunk::bits + shift_bits > chunk::bits)
+ carry = data[result.chunks + shift_chunks] << (chunk::bits - shift_bits);
+ for (size_t n = 0; n < result.chunks; n++) {
+ result.data[result.chunks - 1 - n] = carry | (data[result.chunks + shift_chunks - 1 - n] >> shift_bits);
+ carry = (shift_bits == 0) ? 0
+ : data[result.chunks + shift_chunks - 1 - n] << (chunk::bits - shift_bits);
+ }
+ return result;
+ }
+
+ template<size_t ResultBits, size_t SelBits>
+ value<ResultBits> demux(const value<SelBits> &sel) const {
+ static_assert(Bits << SelBits == ResultBits, "invalid sizes used in demux()");
+ size_t amount = sel.data[0] * Bits;
+ size_t shift_chunks = amount / chunk::bits;
+ size_t shift_bits = amount % chunk::bits;
+ value<ResultBits> result;
+ chunk::type carry = 0;
+ for (size_t n = 0; n < chunks; n++) {
+ result.data[shift_chunks + n] = (data[n] << shift_bits) | carry;
+ carry = (shift_bits == 0) ? 0
+ : data[n] >> (chunk::bits - shift_bits);
+ }
+ if (Bits % chunk::bits + shift_bits > chunk::bits)
+ result.data[shift_chunks + chunks] = carry;
+ return result;
+ }
+
size_t ctpop() const {
size_t count = 0;
for (size_t n = 0; n < chunks; n++) {
@@ -722,50 +758,32 @@ std::ostream &operator<<(std::ostream &os, const wire<Bits> &val) {
template<size_t Width>
struct memory {
- std::vector<value<Width>> data;
-
- size_t depth() const {
- return data.size();
- }
+ const size_t depth;
+ std::unique_ptr<value<Width>[]> data;
- memory() = delete;
- explicit memory(size_t depth) : data(depth) {}
+ explicit memory(size_t depth) : depth(depth), data(new value<Width>[depth]) {}
memory(const memory<Width> &) = delete;
memory<Width> &operator=(const memory<Width> &) = delete;
memory(memory<Width> &&) = default;
- memory<Width> &operator=(memory<Width> &&) = default;
-
- // The only way to get the compiler to put the initializer in .rodata and do not copy it on stack is to stuff it
- // into a plain array. You'd think an std::initializer_list would work here, but it doesn't, because you can't
- // construct an initializer_list in a constexpr (or something) and so if you try to do that the whole thing is
- // first copied on the stack (probably overflowing it) and then again into `data`.
- template<size_t Size>
- struct init {
- size_t offset;
- value<Width> data[Size];
- };
-
- template<size_t... InitSize>
- explicit memory(size_t depth, const init<InitSize> &...init) : data(depth) {
- data.resize(depth);
- // This utterly reprehensible construct is the most reasonable way to apply a function to every element
- // of a parameter pack, if the elements all have different types and so cannot be cast to an initializer list.
- auto _ = {std::move(std::begin(init.data), std::end(init.data), data.begin() + init.offset)...};
- (void)_;
+ memory<Width> &operator=(memory<Width> &&other) {
+ assert(depth == other.depth);
+ data = std::move(other.data);
+ write_queue = std::move(other.write_queue);
+ return *this;
}
// An operator for direct memory reads. May be used at any time during the simulation.
const value<Width> &operator [](size_t index) const {
- assert(index < data.size());
+ assert(index < depth);
return data[index];
}
// An operator for direct memory writes. May only be used before the simulation is started. If used
// after the simulation is started, the design may malfunction.
value<Width> &operator [](size_t index) {
- assert(index < data.size());
+ assert(index < depth);
return data[index];
}
@@ -790,7 +808,7 @@ struct memory {
std::vector<write> write_queue;
void update(size_t index, const value<Width> &val, const value<Width> &mask, int priority = 0) {
- assert(index < data.size());
+ assert(index < depth);
// Queue up the write while keeping the queue sorted by priority.
write_queue.insert(
std::upper_bound(write_queue.begin(), write_queue.end(), priority,
@@ -947,9 +965,9 @@ struct debug_item : ::cxxrtl_object {
flags = 0;
width = Width;
lsb_at = 0;
- depth = item.data.size();
+ depth = item.depth;
zero_at = zero_offset;
- curr = item.data.empty() ? nullptr : item.data[0].data;
+ curr = item.data ? item.data[0].data : nullptr;
next = nullptr;
outline = nullptr;
}
@@ -1051,9 +1069,9 @@ struct debug_items {
}
};
-// Tag class to disambiguate module move constructor and module constructor that takes black boxes
-// out of another instance of the module.
-struct adopt {};
+// Tag class to disambiguate the default constructor used by the toplevel module that calls reset(),
+// and the constructor of interior modules that should not call it.
+struct interior {};
struct module {
module() {}
diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index 40e61e5af..404755b1e 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -198,7 +198,7 @@ bool is_extending_cell(RTLIL::IdString type)
bool is_inlinable_cell(RTLIL::IdString type)
{
return is_unary_cell(type) || is_binary_cell(type) || type.in(
- ID($mux), ID($concat), ID($slice), ID($pmux));
+ ID($mux), ID($concat), ID($slice), ID($pmux), ID($bmux), ID($demux));
}
bool is_ff_cell(RTLIL::IdString type)
@@ -206,6 +206,7 @@ bool is_ff_cell(RTLIL::IdString type)
return type.in(
ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce),
ID($adff), ID($adffe), ID($dffsr), ID($dffsre),
+ ID($aldff), ID($aldffe),
ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr));
}
@@ -933,11 +934,6 @@ struct CxxrtlWorker {
f << "}";
}
- void dump_const_init(const RTLIL::Const &data)
- {
- dump_const_init(data, data.size());
- }
-
void dump_const(const RTLIL::Const &data, int width, int offset = 0, bool fixed_width = false)
{
f << "value<" << width << ">";
@@ -1158,6 +1154,22 @@ struct CxxrtlWorker {
for (int part = 0; part < s_width; part++) {
f << ")";
}
+ // Big muxes
+ } else if (cell->type == ID($bmux)) {
+ dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
+ f << ".bmux<";
+ f << cell->getParam(ID::WIDTH).as_int();
+ f << ">(";
+ dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
+ f << ").val()";
+ // Demuxes
+ } else if (cell->type == ID($demux)) {
+ dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
+ f << ".demux<";
+ f << GetSize(cell->getPort(ID::Y));
+ f << ">(";
+ dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
+ f << ").val()";
// Concats
} else if (cell->type == ID($concat)) {
dump_sigspec_rhs(cell->getPort(ID::B), for_debug);
@@ -1267,6 +1279,20 @@ struct CxxrtlWorker {
dec_indent();
f << indent << "}\n";
}
+ if (cell->hasPort(ID::ALOAD)) {
+ // Asynchronous load
+ f << indent << "if (";
+ dump_sigspec_rhs(cell->getPort(ID::ALOAD));
+ f << " == value<1> {" << cell->getParam(ID::ALOAD_POLARITY).as_bool() << "u}) {\n";
+ inc_indent();
+ f << indent;
+ dump_sigspec_lhs(cell->getPort(ID::Q));
+ f << " = ";
+ dump_sigspec_rhs(cell->getPort(ID::AD));
+ f << ";\n";
+ dec_indent();
+ f << indent << "}\n";
+ }
if (cell->hasPort(ID::SET)) {
// Asynchronous set (for individual bits)
f << indent;
@@ -1770,20 +1796,10 @@ struct CxxrtlWorker {
} else {
f << "<" << wire->width << ">";
}
- f << " " << mangle(wire);
- if (wire_init.count(wire)) {
- f << " ";
- dump_const_init(wire_init.at(wire));
- }
- f << ";\n";
+ f << " " << mangle(wire) << ";\n";
if (edge_wires[wire]) {
if (!wire_type.is_buffered()) {
- f << indent << "value<" << wire->width << "> prev_" << mangle(wire);
- if (wire_init.count(wire)) {
- f << " ";
- dump_const_init(wire_init.at(wire));
- }
- f << ";\n";
+ f << indent << "value<" << wire->width << "> prev_" << mangle(wire) << ";\n";
}
for (auto edge_type : edge_types) {
if (edge_type.first.wire == wire) {
@@ -1833,38 +1849,67 @@ struct CxxrtlWorker {
f << "value<" << wire->width << "> " << mangle(wire) << ";\n";
}
- void dump_memory(Mem *mem)
+ void dump_reset_method(RTLIL::Module *module)
{
- dump_attrs(mem);
- f << indent << "memory<" << mem->width << "> " << mangle(mem)
- << " { " << mem->size << "u";
- if (!GetSize(mem->inits)) {
- f << " };\n";
- } else {
- f << ",\n";
- inc_indent();
- for (auto &init : mem->inits) {
+ int mem_init_idx = 0;
+ inc_indent();
+ for (auto wire : module->wires()) {
+ const auto &wire_type = wire_types[wire];
+ if (!wire_type.is_named() || wire_type.is_local()) continue;
+ if (!wire_init.count(wire)) continue;
+
+ f << indent << mangle(wire) << " = ";
+ if (wire_types[wire].is_buffered()) {
+ f << "wire<" << wire->width << ">";
+ } else {
+ f << "value<" << wire->width << ">";
+ }
+ dump_const_init(wire_init.at(wire), wire->width);
+ f << ";\n";
+
+ if (edge_wires[wire] && !wire_types[wire].is_buffered()) {
+ f << indent << "prev_" << mangle(wire) << " = ";
+ dump_const(wire_init.at(wire), wire->width);
+ f << ";\n";
+ }
+ }
+ for (auto &mem : mod_memories[module]) {
+ for (auto &init : mem.inits) {
if (init.removed)
continue;
dump_attrs(&init);
- int words = GetSize(init.data) / mem->width;
- f << indent << "memory<" << mem->width << ">::init<" << words << "> { "
- << stringf("%#x", init.addr.as_int()) << ", {";
+ int words = GetSize(init.data) / mem.width;
+ f << indent << "static const value<" << mem.width << "> ";
+ f << "mem_init_" << ++mem_init_idx << "[" << words << "] {";
inc_indent();
for (int n = 0; n < words; n++) {
if (n % 4 == 0)
f << "\n" << indent;
else
f << " ";
- dump_const(init.data, mem->width, n * mem->width, /*fixed_width=*/true);
+ dump_const(init.data, mem.width, n * mem.width, /*fixed_width=*/true);
f << ",";
}
dec_indent();
- f << "\n" << indent << "}},\n";
+ f << "\n";
+ f << indent << "};\n";
+ f << indent << "std::copy(std::begin(mem_init_" << mem_init_idx << "), ";
+ f << "std::end(mem_init_" << mem_init_idx << "), ";
+ f << "&" << mangle(&mem) << ".data[" << stringf("%#x", init.addr.as_int()) << "]);\n";
}
- dec_indent();
- f << indent << "};\n";
- }
+ }
+ for (auto cell : module->cells()) {
+ if (is_internal_cell(cell->type))
+ continue;
+ f << indent << mangle(cell);
+ RTLIL::Module *cell_module = module->design->module(cell->type);
+ if (cell_module->get_bool_attribute(ID(cxxrtl_blackbox))) {
+ f << "->reset();\n";
+ } else {
+ f << ".reset();\n";
+ }
+ }
+ dec_indent();
}
void dump_eval_method(RTLIL::Module *module)
@@ -2185,6 +2230,10 @@ struct CxxrtlWorker {
dump_wire(wire, /*is_local=*/false);
}
f << "\n";
+ f << indent << "void reset() override {\n";
+ dump_reset_method(module);
+ f << indent << "}\n";
+ f << "\n";
f << indent << "bool eval() override {\n";
dump_eval_method(module);
f << indent << "}\n";
@@ -2233,7 +2282,9 @@ struct CxxrtlWorker {
dump_debug_wire(wire, /*is_local=*/false);
bool has_memories = false;
for (auto &mem : mod_memories[module]) {
- dump_memory(&mem);
+ dump_attrs(&mem);
+ f << indent << "memory<" << mem.width << "> " << mangle(&mem)
+ << " { " << mem.size << "u };\n";
has_memories = true;
}
if (has_memories)
@@ -2254,52 +2305,20 @@ struct CxxrtlWorker {
dump_metadata_map(cell->attributes);
f << ");\n";
} else {
- f << indent << mangle(cell_module) << " " << mangle(cell) << ";\n";
+ f << indent << mangle(cell_module) << " " << mangle(cell) << " {interior()};\n";
}
has_cells = true;
}
if (has_cells)
f << "\n";
- f << indent << mangle(module) << "() {}\n";
- if (has_cells) {
- f << indent << mangle(module) << "(adopt, " << mangle(module) << " other) :\n";
- bool first = true;
- for (auto cell : module->cells()) {
- if (is_internal_cell(cell->type))
- continue;
- if (first) {
- first = false;
- } else {
- f << ",\n";
- }
- RTLIL::Module *cell_module = module->design->module(cell->type);
- if (cell_module->get_bool_attribute(ID(cxxrtl_blackbox))) {
- f << indent << " " << mangle(cell) << "(std::move(other." << mangle(cell) << "))";
- } else {
- f << indent << " " << mangle(cell) << "(adopt {}, std::move(other." << mangle(cell) << "))";
- }
- }
- f << " {\n";
- inc_indent();
- for (auto cell : module->cells()) {
- if (is_internal_cell(cell->type))
- continue;
- RTLIL::Module *cell_module = module->design->module(cell->type);
- if (cell_module->get_bool_attribute(ID(cxxrtl_blackbox)))
- f << indent << mangle(cell) << "->reset();\n";
- }
- dec_indent();
- f << indent << "}\n";
- } else {
- f << indent << mangle(module) << "(adopt, " << mangle(module) << " other) {}\n";
- }
- f << "\n";
- f << indent << "void reset() override {\n";
+ f << indent << mangle(module) << "(interior) {}\n";
+ f << indent << mangle(module) << "() {\n";
inc_indent();
- f << indent << "*this = " << mangle(module) << "(adopt {}, std::move(*this));\n";
+ f << indent << "reset();\n";
dec_indent();
- f << indent << "}\n";
+ f << indent << "};\n";
f << "\n";
+ f << indent << "void reset() override;\n";
f << indent << "bool eval() override;\n";
f << indent << "bool commit() override;\n";
if (debug_info) {
@@ -2326,6 +2345,10 @@ struct CxxrtlWorker {
{
if (module->get_bool_attribute(ID(cxxrtl_blackbox)))
return;
+ f << indent << "void " << mangle(module) << "::reset() {\n";
+ dump_reset_method(module);
+ f << indent << "}\n";
+ f << "\n";
f << indent << "bool " << mangle(module) << "::eval() {\n";
dump_eval_method(module);
f << indent << "}\n";
@@ -2573,7 +2596,7 @@ struct CxxrtlWorker {
flow.add_node(cell);
// Various DFF cells are treated like posedge/negedge processes, see above for details.
- if (cell->type.in(ID($dff), ID($dffe), ID($adff), ID($adffe), ID($dffsr), ID($dffsre), ID($sdff), ID($sdffe), ID($sdffce))) {
+ if (cell->type.in(ID($dff), ID($dffe), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre), ID($sdff), ID($sdffe), ID($sdffce))) {
if (is_valid_clock(cell->getPort(ID::CLK)))
register_edge_signal(sigmap, cell->getPort(ID::CLK),
cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn);
@@ -2883,15 +2906,16 @@ struct CxxrtlWorker {
debug_wire_type = {WireType::INLINE, node->cell}; // wire replaced with cell
break;
case FlowGraph::Node::Type::CONNECT:
- debug_wire_type = {WireType::INLINE, node->connect.second}; // wire replaced with sig
+ debug_wire_type = {WireType::INLINE, node->connect.second}; // wire replaced with sig
break;
default: continue;
}
debug_live_nodes.erase(node);
- } else if (wire_type.is_member() || wire_type.is_local()) {
+ } else if (wire_type.is_member() || wire_type.type == WireType::LOCAL) {
debug_wire_type = wire_type; // wire not inlinable
} else {
- log_assert(wire_type.type == WireType::UNUSED);
+ log_assert(wire_type.type == WireType::INLINE ||
+ wire_type.type == WireType::UNUSED);
if (flow.wire_comb_defs[wire].size() == 0) {
if (wire_init.count(wire)) { // wire never modified
debug_wire_type = {WireType::CONST, wire_init.at(wire)};
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 7abe584c9..85c44824f 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -1188,6 +1188,8 @@ struct FirrtlBackend : public Backend {
log("Write a FIRRTL netlist of the current design.\n");
log("The following commands are executed by this command:\n");
log(" pmuxtree\n");
+ log(" bmuxmap\n");
+ log(" demuxmap\n");
log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
@@ -1210,7 +1212,9 @@ struct FirrtlBackend : public Backend {
log_header(design, "Executing FIRRTL backend.\n");
log_push();
- Pass::call(design, stringf("pmuxtree"));
+ Pass::call(design, "pmuxtree");
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
namecache.clear();
autoid_counter = 0;
diff --git a/backends/jny/Makefile.inc b/backends/jny/Makefile.inc
new file mode 100644
index 000000000..5e417128e
--- /dev/null
+++ b/backends/jny/Makefile.inc
@@ -0,0 +1,2 @@
+
+OBJS += backends/jny/jny.o
diff --git a/backends/jny/jny.cc b/backends/jny/jny.cc
new file mode 100644
index 000000000..d801b144c
--- /dev/null
+++ b/backends/jny/jny.cc
@@ -0,0 +1,554 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Aki "lethalbit" Van Ness <aki@yosyshq.com> <aki@lethalbit.net>
+ *
+ * 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.
+ *
+ */
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/cellaigs.h"
+#include "kernel/log.h"
+#include <string>
+#include <algorithm>
+#include <unordered_map>
+#include <vector>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+
+struct JnyWriter
+{
+ private:
+ std::ostream &f;
+ bool _use_selection;
+
+ // XXX(aki): TODO: this needs to be updated to us
+ // dict<T, V> and then coalesce_cells needs to be updated
+ // but for now for the PoC this looks to be sufficient
+ std::unordered_map<std::string, std::vector<Cell*>> _cells{};
+
+ bool _include_connections;
+ bool _include_attributes;
+ bool _include_properties;
+
+ string escape_string(string str) {
+ std::string newstr;
+
+ auto itr = str.begin();
+
+ for(; itr != str.end(); ++itr) {
+ switch (*itr) {
+ case '\\': {
+ newstr += "\\\\";
+ break;
+ } case '\n': {
+ newstr += "\\n";
+ break;
+ } case '\f': {
+ newstr += "\\f";
+ break;
+ } case '\t': {
+ newstr += "\\t";
+ break;
+ } case '\r': {
+ newstr += "\\r";
+ break;
+ } case '\"': {
+ newstr += "\\\"";
+ break;
+ } case '\b': {
+ newstr += "\\b";
+ break;
+ } default: {
+ newstr += *itr;
+ }
+ }
+ }
+
+ return newstr;
+ }
+
+ // XXX(aki): I know this is far from ideal but i'm out of spoons and cant focus so
+ // it'll have to do for now,
+ void coalesce_cells(Module* mod)
+ {
+ _cells.clear();
+ for (auto cell : mod->cells()) {
+ const auto cell_type = escape_string(RTLIL::unescape_id(cell->type));
+
+ if (_cells.find(cell_type) == _cells.end())
+ _cells.emplace(cell_type, std::vector<Cell*>());
+
+ _cells.at(cell_type).push_back(cell);
+ }
+ }
+
+ // XXX(aki): this is a lazy way to do this i know,,,
+ std::string gen_indent(const uint16_t level)
+ {
+ std::stringstream s;
+ for (uint16_t i = 0; i <= level; ++i)
+ {
+ s << " ";
+ }
+ return s.str();
+ }
+
+ public:
+ JnyWriter(std::ostream &f, bool use_selection, bool connections, bool attributes, bool properties) noexcept:
+ f(f), _use_selection(use_selection),
+ _include_connections(connections), _include_attributes(attributes), _include_properties(properties)
+ { }
+
+ void write_metadata(Design *design, uint16_t indent_level = 0)
+ {
+ log_assert(design != nullptr);
+
+ design->sort();
+
+ f << "{\n";
+ f << stringf(" \"generator\": \"%s\",\n", escape_string(yosys_version_str).c_str());
+ // XXX(aki): Replace this with a proper version info eventually:tm:
+ f << " \"version\": \"0.0.0\",\n";
+
+ f << " \"features\": [";
+
+ size_t fnum{0};
+ if (_include_connections) {
+ ++fnum;
+ f << "\"connections\"";
+ }
+
+ if (_include_attributes) {
+ if (fnum > 0)
+ f << ", ";
+ ++fnum;
+ f << "\"attributes\"";
+ }
+
+ if (_include_properties) {
+ if (fnum > 0)
+ f << ", ";
+ ++fnum;
+ f << "\"properties\"";
+ }
+
+ f << "],\n";
+
+ f << " \"modules\": [\n";
+
+ bool first{true};
+ for (auto mod : _use_selection ? design->selected_modules() : design->modules()) {
+ if (!first)
+ f << ",\n";
+ write_module(mod, indent_level + 2);
+ first = false;
+ }
+
+ f << "\n";
+ f << " ]\n";
+ f << "}\n";
+ }
+
+ void write_sigspec(const RTLIL::SigSpec& sig, uint16_t indent_level = 0) {
+ const auto _indent = gen_indent(indent_level);
+
+ f << _indent << " {\n";
+ f << _indent << " \"width\": \"" << sig.size() << "\",\n";
+ f << _indent << " \"type\": \"";
+
+ if (sig.is_wire()) {
+ f << "wire";
+ } else if (sig.is_chunk()) {
+ f << "chunk";
+ } else if (sig.is_bit()) {
+ f << "bit";
+ } else {
+ f << "unknown";
+ }
+ f << "\",\n";
+
+ f << _indent << " \"const\": ";
+ if (sig.has_const()) {
+ f << "true";
+ } else {
+ f << "false";
+ }
+
+ f << "\n";
+
+ f << _indent << " }";
+ }
+
+ void write_mod_conn(const std::pair<RTLIL::SigSpec, RTLIL::SigSpec>& conn, uint16_t indent_level = 0) {
+ const auto _indent = gen_indent(indent_level);
+ f << _indent << " {\n";
+ f << _indent << " \"signals\": [\n";
+
+ write_sigspec(conn.first, indent_level + 2);
+ f << ",\n";
+ write_sigspec(conn.second, indent_level + 2);
+ f << "\n";
+
+ f << _indent << " ]\n";
+ f << _indent << " }";
+ }
+
+ void write_cell_conn(const std::pair<RTLIL::IdString, RTLIL::SigSpec>& sig, uint16_t indent_level = 0) {
+ const auto _indent = gen_indent(indent_level);
+ f << _indent << " {\n";
+ f << _indent << " \"name\": \"" << escape_string(RTLIL::unescape_id(sig.first)) << "\",\n";
+ f << _indent << " \"signals\": [\n";
+
+ write_sigspec(sig.second, indent_level + 2);
+ f << "\n";
+
+ f << _indent << " ]\n";
+ f << _indent << " }";
+ }
+
+ void write_module(Module* mod, uint16_t indent_level = 0) {
+ log_assert(mod != nullptr);
+
+ coalesce_cells(mod);
+
+ const auto _indent = gen_indent(indent_level);
+
+ f << _indent << "{\n";
+ f << stringf(" %s\"name\": \"%s\",\n", _indent.c_str(), escape_string(RTLIL::unescape_id(mod->name)).c_str());
+ f << _indent << " \"cell_sorts\": [\n";
+
+ bool first_sort{true};
+ for (auto& sort : _cells) {
+ if (!first_sort)
+ f << ",\n";
+ write_cell_sort(sort, indent_level + 2);
+ first_sort = false;
+ }
+ f << "\n";
+
+ f << _indent << " ]";
+ if (_include_connections) {
+ f << ",\n" << _indent << " \"connections\": [\n";
+
+ bool first_conn{true};
+ for (const auto& conn : mod->connections()) {
+ if (!first_conn)
+ f << ",\n";
+
+ write_mod_conn(conn, indent_level + 2);
+
+ first_conn = false;
+ }
+
+ f << _indent << " ]";
+ }
+ if (_include_attributes) {
+ f << ",\n" << _indent << " \"attributes\": {\n";
+
+ write_prams(mod->attributes, indent_level + 2);
+
+ f << "\n";
+ f << _indent << " }";
+ }
+ f << "\n" << _indent << "}";
+ }
+
+ void write_cell_ports(RTLIL::Cell* port_cell, uint64_t indent_level = 0) {
+ const auto _indent = gen_indent(indent_level);
+
+ bool first_port{true};
+ for (auto con : port_cell->connections()) {
+ if (!first_port)
+ f << ",\n";
+
+ f << _indent << " {\n";
+ f << stringf(" %s\"name\": \"%s\",\n", _indent.c_str(), escape_string(RTLIL::unescape_id(con.first)).c_str());
+ f << _indent << " \"direction\": \"";
+ if (port_cell->input(con.first))
+ f << "i";
+ if (port_cell->input(con.first))
+ f << "o";
+ f << "\",\n";
+ if (con.second.size() == 1)
+ f << _indent << " \"range\": [0, 0]\n";
+ else
+ f << stringf(" %s\"range\": [%d, %d]\n", _indent.c_str(), con.second.size(), 0);
+ f << _indent << " }";
+
+ first_port = false;
+ }
+ f << "\n";
+ }
+
+
+ void write_cell_sort(std::pair<const std::string, std::vector<Cell*>>& sort, uint16_t indent_level = 0) {
+ const auto port_cell = sort.second.front();
+ const auto _indent = gen_indent(indent_level);
+
+ f << _indent << "{\n";
+ f << stringf(" %s\"type\": \"%s\",\n", _indent.c_str(), sort.first.c_str());
+ f << _indent << " \"ports\": [\n";
+
+ write_cell_ports(port_cell, indent_level + 2);
+
+ f << _indent << " ],\n" << _indent << " \"cells\": [\n";
+
+ bool first_cell{true};
+ for (auto& cell : sort.second) {
+ if (!first_cell)
+ f << ",\n";
+
+ write_cell(cell, indent_level + 2);
+
+ first_cell = false;
+ }
+
+ f << "\n";
+ f << _indent << " ]\n";
+ f << _indent << "}";
+ }
+
+ void write_param_val(const Const& v) {
+ if ((v.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) == RTLIL::ConstFlags::CONST_FLAG_STRING) {
+ const auto str = v.decode_string();
+
+ // XXX(aki): TODO, uh, yeah
+
+ f << "\"" << escape_string(str) << "\"";
+ } else if ((v.flags & RTLIL::ConstFlags::CONST_FLAG_SIGNED) == RTLIL::ConstFlags::CONST_FLAG_SIGNED) {
+ f << stringf("\"%dsd %d\"", v.size(), v.as_int(true));
+ } else if ((v.flags & RTLIL::ConstFlags::CONST_FLAG_REAL) == RTLIL::ConstFlags::CONST_FLAG_REAL) {
+
+ } else {
+ f << "\"" << escape_string(v.as_string()) << "\"";
+ }
+ }
+
+ void write_prams(dict<RTLIL::IdString, RTLIL::Const>& params, uint16_t indent_level = 0) {
+ const auto _indent = gen_indent(indent_level);
+
+ bool first_param{true};
+ for (auto& param : params) {
+ if (!first_param)
+ f << stringf(",\n");
+ const auto param_val = param.second;
+ if (!param_val.empty()) {
+ f << stringf(" %s\"%s\": ", _indent.c_str(), escape_string(RTLIL::unescape_id(param.first)).c_str());
+ write_param_val(param_val);
+ } else {
+ f << stringf(" %s\"%s\": true", _indent.c_str(), escape_string(RTLIL::unescape_id(param.first)).c_str());
+ }
+
+ first_param = false;
+ }
+ }
+
+ void write_cell(Cell* cell, uint16_t indent_level = 0) {
+ const auto _indent = gen_indent(indent_level);
+ log_assert(cell != nullptr);
+
+ f << _indent << " {\n";
+ f << stringf(" %s\"name\": \"%s\"", _indent.c_str(), escape_string(RTLIL::unescape_id(cell->name)).c_str());
+
+ if (_include_connections) {
+ f << ",\n" << _indent << " \"connections\": [\n";
+
+ bool first_conn{true};
+ for (const auto& conn : cell->connections()) {
+ if (!first_conn)
+ f << ",\n";
+
+ write_cell_conn(conn, indent_level + 2);
+
+ first_conn = false;
+ }
+
+ f << "\n";
+ f << _indent << " ]";
+ }
+
+ if (_include_attributes) {
+ f << ",\n" << _indent << " \"attributes\": {\n";
+
+ write_prams(cell->attributes, indent_level + 2);
+
+ f << "\n";
+ f << _indent << " }";
+ }
+
+ if (_include_properties) {
+ f << ",\n" << _indent << " \"parameters\": {\n";
+
+ write_prams(cell->parameters, indent_level + 2);
+
+ f << "\n";
+ f << _indent << " }";
+ }
+
+ f << "\n" << _indent << " }";
+ }
+};
+
+struct JnyBackend : public Backend {
+ JnyBackend() : Backend("jny", "generate design metadata") { }
+ void help() override {
+ // XXX(aki): TODO: explicitly document the JSON schema
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" jny [options] [selection]\n");
+ log("\n");
+ log(" -no-connections\n");
+ log(" Don't include connection information in the netlist output.\n");
+ log("\n");
+ log(" -no-attributes\n");
+ log(" Don't include attributed information in the netlist output.\n");
+ log("\n");
+ log(" -no-properties\n");
+ log(" Don't include property information in the netlist output.\n");
+ log("\n");
+ log("Write a JSON metadata for the current design\n");
+ log("\n");
+ log("\n");
+ }
+
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override {
+
+ bool connections{true};
+ bool attributes{true};
+ bool properties{true};
+
+ size_t argidx{1};
+ for (; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-no-connections") {
+ connections = false;
+ continue;
+ }
+
+ if (args[argidx] == "-no-attributes") {
+ attributes = false;
+ continue;
+ }
+
+ if (args[argidx] == "-no-properties") {
+ properties = false;
+ continue;
+ }
+
+ break;
+ }
+ extra_args(f, filename, args, argidx);
+
+ log_header(design, "Executing jny backend.\n");
+
+ JnyWriter jny_writer(*f, false, connections, attributes, properties);
+ jny_writer.write_metadata(design);
+ }
+
+} JnyBackend;
+
+
+struct JnyPass : public Pass {
+ JnyPass() : Pass("jny", "write design and metadata") { }
+
+ void help() override {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" jny [options] [selection]\n");
+ log("\n");
+ log("Write a JSON netlist metadata for the current design\n");
+ log("\n");
+ log(" -o <filename>\n");
+ log(" write to the specified file.\n");
+ log("\n");
+ log(" -no-connections\n");
+ log(" Don't include connection information in the netlist output.\n");
+ log("\n");
+ log(" -no-attributes\n");
+ log(" Don't include attributed information in the netlist output.\n");
+ log("\n");
+ log(" -no-properties\n");
+ log(" Don't include property information in the netlist output.\n");
+ log("\n");
+ log("See 'help write_jny' for a description of the JSON format used.\n");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override {
+ std::string filename{};
+
+ bool connections{true};
+ bool attributes{true};
+ bool properties{true};
+
+ size_t argidx{1};
+ for (; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-o" && argidx+1 < args.size()) {
+ filename = args[++argidx];
+ continue;
+ }
+
+ if (args[argidx] == "-no-connections") {
+ connections = false;
+ continue;
+ }
+
+ if (args[argidx] == "-no-attributes") {
+ attributes = false;
+ continue;
+ }
+
+ if (args[argidx] == "-no-properties") {
+ properties = false;
+ continue;
+ }
+
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ std::ostream *f;
+ 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()) {
+ delete ff;
+ log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
+ }
+ f = ff;
+ } else {
+ f = &buf;
+ }
+
+
+ JnyWriter jny_writer(*f, false, connections, attributes, properties);
+ jny_writer.write_metadata(design);
+
+ if (!filename.empty()) {
+ delete f;
+ } else {
+ log("%s", buf.str().c_str());
+ }
+ }
+
+} JnyPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 4aa8046d6..270d762ee 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -52,8 +52,23 @@ struct JsonWriter
string newstr = "\"";
for (char c : str) {
if (c == '\\')
+ newstr += "\\\\";
+ else if (c == '"')
+ newstr += "\\\"";
+ else if (c == '\b')
+ newstr += "\\b";
+ else if (c == '\f')
+ newstr += "\\f";
+ else if (c == '\n')
+ newstr += "\\n";
+ else if (c == '\r')
+ newstr += "\\r";
+ else if (c == '\t')
+ newstr += "\\t";
+ else if (c < 0x20)
+ newstr += stringf("\\u%04X", c);
+ else
newstr += c;
- newstr += c;
}
return newstr + "\"";
}
@@ -379,6 +394,7 @@ struct JsonBackend : public Backend {
log(" \"bits\": <bit_vector>\n");
log(" \"offset\": <the lowest bit index in use, if non-0>\n");
log(" \"upto\": <1 if the port bit indexing is MSB-first>\n");
+ log(" \"signed\": <1 if the port is signed>\n");
log(" }\n");
log("\n");
log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.");
@@ -428,6 +444,7 @@ struct JsonBackend : public Backend {
log(" \"bits\": <bit_vector>\n");
log(" \"offset\": <the lowest bit index in use, if non-0>\n");
log(" \"upto\": <1 if the port bit indexing is MSB-first>\n");
+ log(" \"signed\": <1 if the port is signed>\n");
log(" }\n");
log("\n");
log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n");
diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc
index a6e45b2f2..1b11de5ec 100644
--- a/backends/rtlil/rtlil_backend.cc
+++ b/backends/rtlil/rtlil_backend.cc
@@ -51,15 +51,19 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
}
}
f << stringf("%d'", width);
- for (int i = offset+width-1; i >= offset; i--) {
- log_assert(i < (int)data.bits.size());
- switch (data.bits[i]) {
- 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;
- case RTLIL::Sm: f << stringf("m"); break;
+ if (data.is_fully_undef()) {
+ f << "x";
+ } else {
+ for (int i = offset+width-1; i >= offset; i--) {
+ log_assert(i < (int)data.bits.size());
+ switch (data.bits[i]) {
+ 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;
+ case RTLIL::Sm: f << stringf("m"); break;
+ }
}
}
} else {
@@ -354,8 +358,8 @@ void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
bool first_conn_line = true;
for (auto it = module->connections().begin(); it != module->connections().end(); ++it) {
- bool show_conn = !only_selected;
- if (only_selected) {
+ bool show_conn = !only_selected || design->selected_whole_module(module->name);
+ if (!show_conn) {
RTLIL::SigSpec sigs = it->first;
sigs.append(it->second);
for (auto &c : sigs.chunks()) {
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index f44827942..ed6f3aff9 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -649,6 +649,27 @@ struct Smt2Worker
return export_bvop(cell, "(bvurem A B)", 'd');
}
}
+ // "div" = flooring division
+ if (cell->type == ID($divfloor)) {
+ if (cell->getParam(ID::A_SIGNED).as_bool()) {
+ // bvsdiv is truncating division, so we can't use it here.
+ int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
+ width = max(width, GetSize(cell->getPort(ID::Y)));
+ auto expr = stringf("(let ("
+ "(a_neg (bvslt A #b%0*d)) "
+ "(b_neg (bvslt B #b%0*d))) "
+ "(let ((abs_a (ite a_neg (bvneg A) A)) "
+ "(abs_b (ite b_neg (bvneg B) B))) "
+ "(let ((u (bvudiv abs_a abs_b)) "
+ "(adj (ite (= #b%0*d (bvurem abs_a abs_b)) #b%0*d #b%0*d))) "
+ "(ite (= a_neg b_neg) u "
+ "(bvneg (bvadd u adj))))))",
+ width, 0, width, 0, width, 0, width, 0, width, 1);
+ return export_bvop(cell, expr, 'd');
+ } else {
+ return export_bvop(cell, "(bvudiv A B)", 'd');
+ }
+ }
if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
@@ -860,7 +881,7 @@ struct Smt2Worker
log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
- if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") {
+ if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") {
log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -985,8 +1006,10 @@ struct Smt2Worker
string name_a = get_bool(cell->getPort(ID::A));
string name_en = get_bool(cell->getPort(ID::EN));
- string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::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->name[0] == '$' && cell->attributes.count(ID::src))
+ decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str()));
+ else
+ decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell)));
if (cell->type == ID($cover))
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1183,10 +1206,12 @@ struct Smt2Worker
data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
+ string empty_mask(mem->width, '0');
+
decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
- "(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+ "(ite (= %s #b%s) (|%s#%d#%d| state) (store (|%s#%d#%d| state) %s %s))) ; %s\n",
get_id(module), arrayid, i+1, get_id(module), abits, mem->width,
- get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
+ mask.c_str(), empty_mask.c_str(), get_id(module), arrayid, i, get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
}
}
@@ -1531,6 +1556,11 @@ struct Smt2Backend : public Backend {
log_header(design, "Executing SMT2 backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index e5cfcdc08..137182f33 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -50,6 +50,7 @@ smtcinit = False
smtctop = None
noinit = False
binarymode = False
+keep_going = False
so = SmtOpts()
@@ -143,7 +144,7 @@ def usage():
--dump-all
when using -g or -i, create a dump file for each
- step. The character '%' is replaces in all dump
+ step. The character '%' is replaced in all dump
filenames with the step number.
--append <num_steps>
@@ -153,6 +154,13 @@ def usage():
--binary
dump anyconst values as raw bit strings
+
+ --keep-going
+ continue BMC after the first failed assertion and report
+ further failed assertions. To output multiple traces
+ covering all found failed assertions, the character '%' is
+ replaced in all dump filenames with an increasing number.
+
""" + so.helpmsg())
sys.exit(1)
@@ -161,7 +169,7 @@ try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["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", "binary"])
+ "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"])
except:
usage()
@@ -234,6 +242,8 @@ for o, a in opts:
topmod = a
elif o == "--binary":
binarymode = True
+ elif o == "--keep-going":
+ keep_going = True
elif so.handle(o, a):
pass
else:
@@ -341,13 +351,13 @@ for fn in inconstr:
assert False
-def get_constr_expr(db, state, final=False, getvalues=False):
+def get_constr_expr(db, state, final=False, getvalues=False, individual=False):
if final:
if ("final-%d" % state) not in db:
- return ([], [], []) if getvalues else "true"
+ return ([], [], []) if getvalues or individual else "true"
else:
if state not in db:
- return ([], [], []) if getvalues else "true"
+ return ([], [], []) if getvalues or individual else "true"
netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
@@ -368,15 +378,18 @@ def get_constr_expr(db, state, final=False, getvalues=False):
expr_list = list()
for loc, expr in db[("final-%d" % state) if final else state]:
actual_expr = netref_regex.sub(replace_netref, expr)
- if getvalues:
+ if getvalues or individual:
expr_list.append((loc, expr, actual_expr))
else:
expr_list.append(actual_expr)
- if getvalues:
- loc_list, expr_list, acual_expr_list = zip(*expr_list)
- value_list = smt.get_list(acual_expr_list)
- return loc_list, expr_list, value_list
+ if getvalues or individual:
+ loc_list, expr_list, actual_expr_list = zip(*expr_list)
+ if individual:
+ return loc_list, expr_list, actual_expr_list
+ else:
+ value_list = smt.get_list(actual_expr_list)
+ return loc_list, expr_list, value_list
if len(expr_list) == 0:
return "true"
@@ -492,7 +505,7 @@ if aimfile is not None:
got_state = True
for entry in f.read().splitlines():
- if len(entry) == 0 or entry[0] in "bcjfu.":
+ if len(entry) == 0 or entry[0] in "bcjfu.#":
continue
if not got_state:
@@ -583,7 +596,10 @@ if aimfile is not None:
if not got_topt:
skip_steps = max(skip_steps, step)
- num_steps = max(num_steps, step+1)
+ # some solvers optimize the properties so that they fail one cycle early,
+ # thus we check the properties in the cycle the aiger witness ends, and
+ # if that doesn't work, we check the cycle after that as well.
+ num_steps = max(num_steps, step+2)
step += 1
if btorwitfile is not None:
@@ -826,7 +842,7 @@ def char_ok_in_verilog(c,i):
return False
def escape_identifier(identifier):
- if type(identifier) is list:
+ if type(identifier) is list:
return map(escape_identifier, identifier)
if "." in identifier:
return ".".join(escape_identifier(identifier.split(".")))
@@ -1068,7 +1084,7 @@ def write_trace(steps_start, steps_stop, index):
write_constr_trace(steps_start, steps_stop, index)
-def print_failed_asserts_worker(mod, state, path, extrainfo):
+def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()):
assert mod in smt.modinfo
found_failed_assert = False
@@ -1076,29 +1092,31 @@ def print_failed_asserts_worker(mod, state, path, extrainfo):
return
for cellname, celltype in smt.modinfo[mod].cells.items():
- if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
+ cell_infokey = (mod, cellname, infokey)
+ if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo, infomap, cell_infokey):
found_failed_assert = True
for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
- print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
+ assert_key = (assertfun, infokey)
+ print_msg("Assert failed in %s: %s%s%s" % (path, assertinfo, extrainfo, infomap.get(assert_key, '')))
found_failed_assert = True
return found_failed_assert
-def print_failed_asserts(state, final=False, extrainfo=""):
+def print_failed_asserts(state, final=False, extrainfo="", infomap={}):
if noinfo: return
loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
found_failed_assert = False
for loc, expr, value in zip(loc_list, expr_list, value_list):
if smt.bv2int(value) == 0:
- print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
+ print_msg("Assert %s failed: %s%s%s" % (loc, expr, extrainfo, infomap.get(loc, '')))
found_failed_assert = True
if not final:
- if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
+ if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo, infomap):
found_failed_assert = True
return found_failed_assert
@@ -1145,6 +1163,43 @@ def get_cover_list(mod, base):
return cover_expr, cover_desc
+
+def get_assert_map(mod, base, path, key_base=()):
+ assert mod in smt.modinfo
+
+ assert_map = dict()
+
+ for expr, desc in smt.modinfo[mod].asserts.items():
+ assert_map[(expr, key_base)] = ("(|%s| %s)" % (expr, base), path, desc)
+
+ for cell, submod in smt.modinfo[mod].cells.items():
+ assert_map.update(get_assert_map(submod, "(|%s_h %s| %s)" % (mod, cell, base), path + "." + cell, (mod, cell, key_base)))
+
+ return assert_map
+
+
+def get_assert_keys():
+ keys = set()
+ keys.update(get_assert_map(topmod, 'state', topmod).keys())
+ for step_constr_asserts in constr_asserts.values():
+ keys.update(loc for loc, expr in step_constr_asserts)
+
+ return keys
+
+
+def get_active_assert_map(step, active):
+ assert_map = dict()
+ for key, assert_data in get_assert_map(topmod, "s%s" % step, topmod).items():
+ if key in active:
+ assert_map[key] = assert_data
+
+ for loc, expr, actual_expr in zip(*get_constr_expr(constr_asserts, step, individual=True)):
+ if loc in active:
+ assert_map[loc] = (actual_expr, None, (expr, loc))
+
+ return assert_map
+
+
states = list()
asserts_antecedent_cache = [list()]
asserts_consequent_cache = [list()]
@@ -1454,6 +1509,10 @@ elif covermode:
print_msg("Unreached cover statement at %s." % cover_desc[i])
else: # not tempind, covermode
+ active_assert_keys = get_assert_keys()
+ failed_assert_infomap = dict()
+ traceidx = 0
+
step = 0
retstatus = "PASSED"
while step < num_steps:
@@ -1507,44 +1566,83 @@ else: # not tempind, covermode
break
if not final_only:
- if last_check_step == step:
- print_msg("Checking assertions in step %d.." % (step))
- else:
- print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
- smt_push()
-
- smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
- [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
-
- if smt_check_sat() == "sat":
- print("%s BMC failed!" % smt.timestamp())
- if append_steps > 0:
- for i in range(last_check_step+1, last_check_step+1+append_steps):
- print_msg("Appending additional step %d." % i)
- smt_state(i)
- smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
- smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
- 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))
- print_msg("Re-solving with appended steps..")
- if smt_check_sat() == "unsat":
- print("%s Cannot append steps without violating assumptions!" % smt.timestamp())
- retstatus = "FAILED"
- break
- print_anyconsts(step)
+ recheck_current_step = True
+ while recheck_current_step:
+ recheck_current_step = False
+ if last_check_step == step:
+ print_msg("Checking assertions in step %d.." % (step))
+ else:
+ print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
+ smt_push()
+
+ active_assert_maps = dict()
+ active_assert_exprs = list()
for i in range(step, last_check_step+1):
- print_failed_asserts(i)
- write_trace(0, last_check_step+1+append_steps, '%')
- retstatus = "FAILED"
- break
+ assert_expr_map = get_active_assert_map(i, active_assert_keys)
+ active_assert_maps[i] = assert_expr_map
+ active_assert_exprs.extend(assert_data[0] for assert_data in assert_expr_map.values())
- smt_pop()
+ if active_assert_exprs:
+ if len(active_assert_exprs) == 1:
+ active_assert_expr = active_assert_exprs[0]
+ else:
+ active_assert_expr = "(and %s)" % " ".join(active_assert_exprs)
+
+ smt_assert("(not %s)" % active_assert_expr)
+ else:
+ smt_assert("false")
+
+
+ if smt_check_sat() == "sat":
+ if retstatus != "FAILED":
+ print("%s BMC failed!" % smt.timestamp())
+
+ if append_steps > 0:
+ for i in range(last_check_step+1, last_check_step+1+append_steps):
+ print_msg("Appending additional step %d." % i)
+ smt_state(i)
+ smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
+ smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
+ 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))
+ print_msg("Re-solving with appended steps..")
+ if smt_check_sat() == "unsat":
+ print("%s Cannot append steps without violating assumptions!" % smt.timestamp())
+ retstatus = "FAILED"
+ break
+ print_anyconsts(step)
+
+ for i in range(step, last_check_step+1):
+ print_failed_asserts(i, infomap=failed_assert_infomap)
+
+ if keep_going:
+ for i in range(step, last_check_step+1):
+ for key, (expr, path, desc) in active_assert_maps[i].items():
+ if key in active_assert_keys and not smt.bv2int(smt.get(expr)):
+ failed_assert_infomap[key] = " [failed before]"
+
+ active_assert_keys.remove(key)
+
+ if active_assert_keys:
+ recheck_current_step = True
+
+ write_trace(0, last_check_step+1+append_steps, "%d" % traceidx if keep_going else '%')
+ traceidx += 1
+ retstatus = "FAILED"
+
+ smt_pop()
+ if recheck_current_step:
+ print_msg("Checking remaining assertions..")
+
+ if retstatus == "FAILED" and not (keep_going and active_assert_keys):
+ break
if (constr_final_start is not None) or (last_check_step+1 != num_steps):
for i in range(step, last_check_step+1):
- smt_assert("(|%s_a| s%d)" % (topmod, i))
- smt_assert(get_constr_expr(constr_asserts, i))
+ assert_expr_map = get_active_assert_map(i, active_assert_keys)
+ for assert_data in assert_expr_map.values():
+ smt_assert(assert_data[0])
if constr_final_start is not None:
for i in range(step, last_check_step+1):
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index d73a875ba..14feec30d 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -20,7 +20,7 @@ import sys, re, os, signal
import subprocess
if os.name == "posix":
import resource
-from copy import deepcopy
+from copy import copy
from select import select
from time import time
from queue import Queue, Empty
@@ -301,7 +301,7 @@ class SmtIo:
key = tuple(stmt)
if key not in self.unroll_cache:
- decl = deepcopy(self.unroll_decls[key[0]])
+ decl = copy(self.unroll_decls[key[0]])
self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
decl[1] = self.unroll_cache[key]
@@ -442,10 +442,10 @@ class SmtIo:
if stmt == "(push 1)":
self.unroll_stack.append((
- deepcopy(self.unroll_sorts),
- deepcopy(self.unroll_objs),
- deepcopy(self.unroll_decls),
- deepcopy(self.unroll_cache),
+ copy(self.unroll_sorts),
+ copy(self.unroll_objs),
+ copy(self.unroll_decls),
+ copy(self.unroll_cache),
))
if stmt == "(pop 1)":
@@ -536,10 +536,16 @@ class SmtIo:
self.modinfo[self.curmod].clocks[fields[2]] = "event"
if fields[1] == "yosys-smt2-assert":
- self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
+ if len(fields) > 4:
+ self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+ else:
+ self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-cover":
- self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
+ if len(fields) > 4:
+ self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+ else:
+ self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-maximize":
self.modinfo[self.curmod].maximize.add(fields[2])
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index f4723d2a6..7d4f94adc 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -578,7 +578,7 @@ struct SmvWorker
log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
- if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") {
+ if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") {
log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -741,6 +741,11 @@ struct SmvBackend : public Backend {
log_header(design, "Executing SMV backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 47b48a460..aa1d4558c 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -44,6 +44,7 @@ std::string auto_prefix, extmem_prefix;
RTLIL::Module *active_module;
dict<RTLIL::SigBit, RTLIL::State> active_initdata;
SigMap active_sigmap;
+IdString initial_id;
void reset_auto_counter_id(RTLIL::IdString id, bool may_rename)
{
@@ -357,7 +358,8 @@ 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 << "\"\"";
+ // See IEEE 1364-2005 Clause 5.1.14.
+ f << "{0{1'b0}}";
return;
}
if (sig.is_chunk()) {
@@ -430,7 +432,7 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
dump_const(f, wire->attributes.at(ID::init));
}
f << stringf(";\n");
- } else if (!wire->port_input && !wire->port_output)
+ } else
f << stringf("%s" "wire%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
#endif
}
@@ -1398,7 +1400,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
FfData ff(nullptr, cell);
// $ff / $_FF_ cell: not supported.
- if (ff.has_d && !ff.has_clk && !ff.has_en)
+ if (ff.has_gclk)
return false;
std::string reg_name = cellname(cell);
@@ -1419,17 +1421,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
for (int i = 0; i < chunks; i++)
{
- SigSpec sig_d;
+ SigSpec sig_d, sig_ad;
Const val_arst, val_srst;
- std::string reg_bit_name, sig_set_name, sig_clr_name, sig_arst_name;
+ std::string reg_bit_name, sig_set_name, sig_clr_name, sig_arst_name, sig_aload_name;
if (chunky) {
reg_bit_name = stringf("%s[%d]", reg_name.c_str(), i);
- if (ff.has_d)
+ if (ff.has_gclk || ff.has_clk)
sig_d = ff.sig_d[i];
+ if (ff.has_aload)
+ sig_ad = ff.sig_ad[i];
} else {
reg_bit_name = reg_name;
- if (ff.has_d)
- sig_d = ff.sig_d;
+ sig_d = ff.sig_d;
+ sig_ad = ff.sig_ad;
}
if (ff.has_arst)
val_arst = chunky ? ff.val_arst[i] : ff.val_arst;
@@ -1437,28 +1441,38 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
val_srst = chunky ? ff.val_srst[i] : ff.val_srst;
// If there are constants in the sensitivity list, replace them with an intermediate wire
- if (ff.has_sr) {
- if (ff.sig_set[i].wire == NULL)
- {
- sig_set_name = next_auto_id();
- f << stringf("%s" "wire %s = ", indent.c_str(), sig_set_name.c_str());
- dump_const(f, ff.sig_set[i].data);
- f << stringf(";\n");
- }
- if (ff.sig_clr[i].wire == NULL)
- {
- sig_clr_name = next_auto_id();
- f << stringf("%s" "wire %s = ", indent.c_str(), sig_clr_name.c_str());
- dump_const(f, ff.sig_clr[i].data);
- f << stringf(";\n");
- }
- } else if (ff.has_arst) {
- if (ff.sig_arst[i].wire == NULL)
- {
- sig_arst_name = next_auto_id();
- f << stringf("%s" "wire %s = ", indent.c_str(), sig_arst_name.c_str());
- dump_const(f, ff.sig_arst[i].data);
- f << stringf(";\n");
+ if (ff.has_clk) {
+ if (ff.has_sr) {
+ if (ff.sig_set[i].wire == NULL)
+ {
+ sig_set_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_set_name.c_str());
+ dump_const(f, ff.sig_set[i].data);
+ f << stringf(";\n");
+ }
+ if (ff.sig_clr[i].wire == NULL)
+ {
+ sig_clr_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_clr_name.c_str());
+ dump_const(f, ff.sig_clr[i].data);
+ f << stringf(";\n");
+ }
+ } else if (ff.has_arst) {
+ if (ff.sig_arst[0].wire == NULL)
+ {
+ sig_arst_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_arst_name.c_str());
+ dump_const(f, ff.sig_arst[0].data);
+ f << stringf(";\n");
+ }
+ } else if (ff.has_aload) {
+ if (ff.sig_aload[0].wire == NULL)
+ {
+ sig_aload_name = next_auto_id();
+ f << stringf("%s" "wire %s = ", indent.c_str(), sig_aload_name.c_str());
+ dump_const(f, ff.sig_aload[0].data);
+ f << stringf(";\n");
+ }
}
}
@@ -1480,13 +1494,18 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf("%s", sig_clr_name.c_str());
else
dump_sigspec(f, ff.sig_clr[i]);
-
} else if (ff.has_arst) {
f << stringf(", %sedge ", ff.pol_arst ? "pos" : "neg");
- if (ff.sig_arst[i].wire == NULL)
+ if (ff.sig_arst[0].wire == NULL)
f << stringf("%s", sig_arst_name.c_str());
else
dump_sigspec(f, ff.sig_arst);
+ } else if (ff.has_aload) {
+ f << stringf(", %sedge ", ff.pol_aload ? "pos" : "neg");
+ if (ff.sig_aload[0].wire == NULL)
+ f << stringf("%s", sig_aload_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_aload);
}
f << stringf(")\n");
@@ -1507,7 +1526,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf("%s" " else ", indent.c_str());
} else if (ff.has_arst) {
f << stringf("if (%s", ff.pol_arst ? "" : "!");
- if (ff.sig_arst[i].wire == NULL)
+ if (ff.sig_arst[0].wire == NULL)
f << stringf("%s", sig_arst_name.c_str());
else
dump_sigspec(f, ff.sig_arst);
@@ -1515,11 +1534,21 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
dump_sigspec(f, val_arst);
f << stringf(";\n");
f << stringf("%s" " else ", indent.c_str());
+ } else if (ff.has_aload) {
+ f << stringf("if (%s", ff.pol_aload ? "" : "!");
+ if (ff.sig_aload[0].wire == NULL)
+ f << stringf("%s", sig_aload_name.c_str());
+ else
+ dump_sigspec(f, ff.sig_aload);
+ f << stringf(") %s <= ", reg_bit_name.c_str());
+ dump_sigspec(f, sig_ad);
+ f << stringf(";\n");
+ f << stringf("%s" " else ", indent.c_str());
}
- if (ff.has_srst && ff.has_en && ff.ce_over_srst) {
- f << stringf("if (%s", ff.pol_en ? "" : "!");
- dump_sigspec(f, ff.sig_en);
+ if (ff.has_srst && ff.has_ce && ff.ce_over_srst) {
+ f << stringf("if (%s", ff.pol_ce ? "" : "!");
+ dump_sigspec(f, ff.sig_ce);
f << stringf(")\n");
f << stringf("%s" " if (%s", indent.c_str(), ff.pol_srst ? "" : "!");
dump_sigspec(f, ff.sig_srst);
@@ -1536,9 +1565,9 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf(";\n");
f << stringf("%s" " else ", indent.c_str());
}
- if (ff.has_en) {
- f << stringf("if (%s", ff.pol_en ? "" : "!");
- dump_sigspec(f, ff.sig_en);
+ if (ff.has_ce) {
+ f << stringf("if (%s", ff.pol_ce ? "" : "!");
+ dump_sigspec(f, ff.sig_ce);
f << stringf(") ");
}
}
@@ -1560,7 +1589,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf("%s" " else if (%s", indent.c_str(), ff.pol_set ? "" : "!");
dump_sigspec(f, ff.sig_set[i]);
f << stringf(") %s = 1'b1;\n", reg_bit_name.c_str());
- if (ff.has_d)
+ if (ff.has_aload)
f << stringf("%s" " else ", indent.c_str());
} else if (ff.has_arst) {
f << stringf("if (%s", ff.pol_arst ? "" : "!");
@@ -1568,14 +1597,14 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf(") %s = ", reg_bit_name.c_str());
dump_sigspec(f, val_arst);
f << stringf(";\n");
- if (ff.has_d)
+ if (ff.has_aload)
f << stringf("%s" " else ", indent.c_str());
}
- if (ff.has_d) {
- f << stringf("if (%s", ff.pol_en ? "" : "!");
- dump_sigspec(f, ff.sig_en);
+ if (ff.has_aload) {
+ f << stringf("if (%s", ff.pol_aload ? "" : "!");
+ dump_sigspec(f, ff.sig_aload);
f << stringf(") %s = ", reg_bit_name.c_str());
- dump_sigspec(f, sig_d);
+ dump_sigspec(f, sig_ad);
f << stringf(";\n");
}
}
@@ -1916,7 +1945,7 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo
f << stringf("%s" "always%s begin\n", indent.c_str(), systemverilog ? "_comb" : " @*");
if (!systemverilog)
- f << indent + " " << "if (" << id("\\initial") << ") begin end\n";
+ f << indent + " " << "if (" << id(initial_id) << ") begin end\n";
dump_case_body(f, indent, &proc->root_case, true);
std::string backup_indent = indent;
@@ -2035,6 +2064,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
dump_attributes(f, indent, module->attributes, '\n', /*modattr=*/true);
f << stringf("%s" "module %s(", indent.c_str(), id(module->name, false).c_str());
bool keep_running = true;
+ int cnt = 0;
for (int port_id = 1; keep_running; port_id++) {
keep_running = false;
for (auto wire : module->wires()) {
@@ -2043,14 +2073,16 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
f << stringf(", ");
f << stringf("%s", id(wire->name).c_str());
keep_running = true;
+ if (cnt==20) { f << stringf("\n"); cnt = 0; } else cnt++;
continue;
}
}
}
f << stringf(");\n");
-
- if (!systemverilog && !module->processes.empty())
- f << indent + " " << "reg " << id("\\initial") << " = 0;\n";
+ if (!systemverilog && !module->processes.empty()) {
+ initial_id = NEW_ID;
+ f << indent + " " << "reg " << id(initial_id) << " = 0;\n";
+ }
for (auto w : module->wires())
dump_wire(f, indent + " ", w);
@@ -2268,6 +2300,12 @@ struct VerilogBackend : public Backend {
extmem_prefix = filename.substr(0, filename.rfind('.'));
}
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ Pass::call(design, "clean_zerowidth");
+ log_pop();
+
design->sort();
*f << stringf("/* Generated by %s */\n", yosys_version_str);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-26 13:29:26 +0000