aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/bugpoint.cc1
-rw-r--r--passes/cmds/chformal.cc19
-rw-r--r--passes/cmds/design.cc5
-rw-r--r--passes/cmds/setundef.cc10
-rw-r--r--passes/cmds/show.cc139
-rw-r--r--passes/cmds/splitcells.cc172
-rw-r--r--passes/cmds/stat.cc3
-rw-r--r--passes/cmds/xprop.cc3
-rw-r--r--passes/equiv/equiv_make.cc92
-rw-r--r--passes/fsm/fsm_detect.cc29
-rw-r--r--passes/opt/opt_ffinv.cc3
-rw-r--r--passes/proc/proc_dff.cc2
-rw-r--r--passes/sat/formalff.cc216
-rw-r--r--passes/sat/sim.cc515
-rw-r--r--passes/techmap/bmuxmap.cc39
15 files changed, 1057 insertions, 191 deletions
diff --git a/passes/cmds/bugpoint.cc b/passes/cmds/bugpoint.cc
index e666023fa..c398afffa 100644
--- a/passes/cmds/bugpoint.cc
+++ b/passes/cmds/bugpoint.cc
@@ -393,6 +393,7 @@ struct BugpointPass : public Pass {
}
}
}
+ delete design_copy;
return nullptr;
}
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc
index 66044b161..da97ff71d 100644
--- a/passes/cmds/chformal.cc
+++ b/passes/cmds/chformal.cc
@@ -55,6 +55,14 @@ struct ChformalPass : public Pass {
log(" -skip <N>\n");
log(" ignore activation of the constraint in the first <N> clock cycles\n");
log("\n");
+ log(" -coverenable\n");
+ log(" add cover statements for the enable signals of the constraints\n");
+ log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+ log(" Note: For the Verific frontend it is currently not guaranteed that a\n");
+ log(" reachable SVA statement corresponds to an active enable signal.\n");
+ log("\n");
+#endif
log(" -assert2assume\n");
log(" -assume2assert\n");
log(" -live2fair\n");
@@ -114,6 +122,10 @@ struct ChformalPass : public Pass {
mode_arg = atoi(args[++argidx].c_str());
continue;
}
+ if (mode == 0 && args[argidx] == "-coverenable") {
+ mode = 'p';
+ continue;
+ }
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
assert2assume = true;
mode = 'c';
@@ -263,6 +275,13 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN)));
}
else
+ if (mode =='p')
+ {
+ for (auto cell : constr_cells)
+ module->addCover(NEW_ID_SUFFIX("coverenable"),
+ cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
+ }
+ else
if (mode == 'c')
{
for (auto cell : constr_cells)
diff --git a/passes/cmds/design.cc b/passes/cmds/design.cc
index 169f7cc4a..168d38563 100644
--- a/passes/cmds/design.cc
+++ b/passes/cmds/design.cc
@@ -118,6 +118,9 @@ struct DesignPass : public Pass {
std::string save_name, load_name, as_name, delete_name;
std::vector<RTLIL::Module*> copy_src_modules;
+ if (!design)
+ log_cmd_error("No default design.\n");
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
@@ -280,7 +283,7 @@ struct DesignPass : public Pass {
done[mod->name] = prefix;
}
- while (!queue.empty())
+ while (!queue.empty() && copy_from_design)
{
pool<Module*> old_queue;
old_queue.swap(queue);
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index 590a7eb1d..7293002f3 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -502,7 +502,15 @@ struct SetundefPass : public Pass {
}
}
- module->rewrite_sigspecs(worker);
+ for (auto &it : module->cells_)
+ if (!it.second->get_bool_attribute(ID::xprop_decoder))
+ it.second->rewrite_sigspecs(worker);
+ for (auto &it : module->processes)
+ it.second->rewrite_sigspecs(worker);
+ for (auto &it : module->connections_) {
+ worker(it.first);
+ worker(it.second);
+ }
if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
{
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index b186e5db2..dd7de8273 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -233,77 +233,101 @@ struct ShowWorker
return std::string();
}
+ // Return the pieces of a label joined by a '|' separator
+ std::string join_label_pieces(std::vector<std::string> pieces)
+ {
+ std::string ret = "";
+ bool first_piece = true;
+
+ for (auto &piece : pieces) {
+ if (!first_piece)
+ ret += "|";
+ ret += piece;
+ first_piece = false;
+ }
+
+ return ret;
+ }
+
std::string gen_portbox(std::string port, RTLIL::SigSpec sig, bool driver, std::string *node = nullptr)
{
std::string code;
std::string net = gen_signode_simple(sig);
if (net.empty())
{
- std::string label_string;
- int pos = sig.size()-1;
- int idx = single_idx_count++;
- for (int rep, i = int(sig.chunks().size())-1; i >= 0; i -= rep) {
- const RTLIL::SigChunk &c = sig.chunks().at(i);
+ int dot_idx = single_idx_count++;
+ std::vector<std::string> label_pieces;
+ int bitpos = sig.size()-1;
+
+ for (int rep, chunk_idx = ((int) sig.chunks().size()) - 1; chunk_idx >= 0; chunk_idx -= rep) {
+ const RTLIL::SigChunk &c = sig.chunks().at(chunk_idx);
+
+ // Find the number of times this chunk is repeating
+ for (rep = 1; chunk_idx - rep >= 0 && c == sig.chunks().at(chunk_idx - rep); rep++);
+
int cl, cr;
- if (c.wire) {
+ cl = c.offset + c.width - 1;
+ cr = c.offset;
+
+ if (c.is_wire()) {
if (c.wire->upto) {
- cr = c.wire->start_offset + (c.wire->width - c.offset - 1);
+ cr = (c.wire->width - 1) - c.offset;
cl = cr - (c.width - 1);
- } else {
- cr = c.wire->start_offset + c.offset;
- cl = cr + c.width - 1;
}
- } else {
- cl = c.offset + c.width - 1;
- cr = c.offset;
+
+ cl += c.wire->start_offset;
+ cr += c.wire->start_offset;
}
- if (!driver && c.wire == nullptr) {
- RTLIL::State s1 = c.data.front();
- for (auto s2 : c.data)
- if (s1 != s2)
- goto not_const_stream;
- net.clear();
- } else {
- not_const_stream:
+
+ // Is this chunk a constant filled with one kind of bit state?
+ bool no_signode = !driver && !c.is_wire() \
+ && std::equal(c.data.begin() + 1, c.data.end(), c.data.begin());
+
+ if (!no_signode) {
net = gen_signode_simple(c, false);
log_assert(!net.empty());
}
- for (rep = 1; i-rep >= 0 && c == sig.chunks().at(i-rep); rep++) {}
+
std::string repinfo = rep > 1 ? stringf("%dx ", rep) : "";
+ std::string portside = stringf("%d:%d", bitpos, bitpos - rep*c.width + 1);
+ std::string remoteside = stringf("%s%d:%d", repinfo.c_str(), cl, cr);
+
if (driver) {
log_assert(!net.empty());
- label_string += stringf("<s%d> %d:%d - %s%d:%d |", i, pos, pos-c.width+1, repinfo.c_str(), cl, cr);
- net_conn_map[net].in.insert({stringf("x%d:s%d", idx, i), rep*c.width});
+ label_pieces.push_back(stringf("<s%d> %s - %s ", chunk_idx, portside.c_str(), remoteside.c_str()));
+ net_conn_map[net].in.insert({stringf("x%d:s%d", dot_idx, chunk_idx), rep*c.width});
net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
- } else
- if (net.empty()) {
- log_assert(rep == 1);
- label_string += stringf("%c -&gt; %d:%d |",
- c.data.front() == State::S0 ? '0' :
- c.data.front() == State::S1 ? '1' :
- c.data.front() == State::Sx ? 'X' :
- c.data.front() == State::Sz ? 'Z' : '?',
- pos, pos-rep*c.width+1);
} else {
- label_string += stringf("<s%d> %s%d:%d - %d:%d |", i, repinfo.c_str(), cl, cr, pos, pos-rep*c.width+1);
- net_conn_map[net].out.insert({stringf("x%d:s%d", idx, i), rep*c.width});
- net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
+ if (no_signode) {
+ log_assert(rep == 1);
+ label_pieces.push_back(stringf("%c -&gt; %d:%d ",
+ c.data.front() == State::S0 ? '0' :
+ c.data.front() == State::S1 ? '1' :
+ c.data.front() == State::Sx ? 'X' :
+ c.data.front() == State::Sz ? 'Z' : '?',
+ bitpos, bitpos-rep*c.width+1));
+ } else {
+ label_pieces.push_back(stringf("<s%d> %s - %s ", chunk_idx, remoteside.c_str(), portside.c_str()));
+ net_conn_map[net].out.insert({stringf("x%d:s%d", dot_idx, chunk_idx), rep*c.width});
+ net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
+ }
}
- pos -= rep * c.width;
+
+ bitpos -= rep * c.width;
}
- if (label_string[label_string.size()-1] == '|')
- label_string = label_string.substr(0, label_string.size()-1);
- code += stringf("x%d [ shape=record, style=rounded, label=\"%s\" ];\n", idx, label_string.c_str());
+
+ code += stringf("x%d [ shape=record, style=rounded, label=\"", dot_idx) \
+ + join_label_pieces(label_pieces) + "\" ];\n";
+
if (!port.empty()) {
currentColor = xorshift32(currentColor);
- log_warning("WIDTHLABEL %s %d\n", log_signal(sig), GetSize(sig));
if (driver)
- code += stringf("%s:e -> x%d:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", port.c_str(), idx, nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
+ code += stringf("%s:e -> x%d:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", port.c_str(), dot_idx, nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
else
- code += stringf("x%d:e -> %s:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", idx, port.c_str(), nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
+ code += stringf("x%d:e -> %s:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", dot_idx, port.c_str(), nextColor(sig).c_str(), widthLabel(sig.size()).c_str());
}
if (node != nullptr)
- *node = stringf("x%d", idx);
+ *node = stringf("x%d", dot_idx);
}
else
{
@@ -418,6 +442,7 @@ struct ShowWorker
for (auto cell : module->selected_cells())
{
std::vector<RTLIL::IdString> in_ports, out_ports;
+ std::vector<std::string> in_label_pieces, out_label_pieces;
for (auto &conn : cell->connections()) {
if (!ct.cell_output(cell->type, conn.first))
@@ -429,23 +454,23 @@ struct ShowWorker
std::sort(in_ports.begin(), in_ports.end(), RTLIL::sort_by_id_str());
std::sort(out_ports.begin(), out_ports.end(), RTLIL::sort_by_id_str());
- std::string label_string = "{{";
+ for (auto &p : in_ports) {
+ bool signed_suffix = genSignedLabels && cell->hasParam(p.str() + "_SIGNED")
+ && cell->getParam(p.str() + "_SIGNED").as_bool();
- for (auto &p : in_ports)
- label_string += stringf("<p%d> %s%s|", id2num(p), escape(p.str()),
- genSignedLabels && cell->hasParam(p.str() + "_SIGNED") &&
- cell->getParam(p.str() + "_SIGNED").as_bool() ? "*" : "");
- if (label_string[label_string.size()-1] == '|')
- label_string = label_string.substr(0, label_string.size()-1);
-
- label_string += stringf("}|%s\\n%s|{", findLabel(cell->name.str()), escape(cell->type.str()));
+ in_label_pieces.push_back(stringf("<p%d> %s%s", id2num(p), escape(p.str()),
+ signed_suffix ? "*" : ""));
+ }
for (auto &p : out_ports)
- label_string += stringf("<p%d> %s|", id2num(p), escape(p.str()));
- if (label_string[label_string.size()-1] == '|')
- label_string = label_string.substr(0, label_string.size()-1);
+ out_label_pieces.push_back(stringf("<p%d> %s", id2num(p), escape(p.str())));
+
+ std::string in_label = join_label_pieces(in_label_pieces);
+ std::string out_label = join_label_pieces(out_label_pieces);
- label_string += "}}";
+ std::string label_string = stringf("{{%s}|%s\\n%s|{%s}}", in_label.c_str(),
+ findLabel(cell->name.str()), escape(cell->type.str()),
+ out_label.c_str());
std::string code;
for (auto &conn : cell->connections()) {
diff --git a/passes/cmds/splitcells.cc b/passes/cmds/splitcells.cc
index de6df6142..82ed49074 100644
--- a/passes/cmds/splitcells.cc
+++ b/passes/cmds/splitcells.cc
@@ -68,70 +68,132 @@ struct SplitcellsWorker
int split(Cell *cell, const std::string &format)
{
- if (!cell->type.in("$and", "$mux", "$not", "$or", "$pmux", "$xnor", "$xor")) return 0;
+ if (cell->type.in("$and", "$mux", "$not", "$or", "$pmux", "$xnor", "$xor"))
+ {
+ SigSpec outsig = sigmap(cell->getPort(ID::Y));
+ if (GetSize(outsig) <= 1) return 0;
+
+ std::vector<int> slices;
+ slices.push_back(0);
+
+ int width = GetSize(outsig);
+ width = std::min(width, GetSize(cell->getPort(ID::A)));
+ if (cell->hasPort(ID::B))
+ width = std::min(width, GetSize(cell->getPort(ID::B)));
+
+ for (int i = 1; i < width; i++) {
+ auto &last_users = bit_users_db[outsig[slices.back()]];
+ auto &this_users = bit_users_db[outsig[i]];
+ if (last_users != this_users) slices.push_back(i);
+ }
+ if (GetSize(slices) <= 1) return 0;
+ slices.push_back(GetSize(outsig));
+
+ log("Splitting %s cell %s/%s into %d slices:\n", log_id(cell->type), log_id(module), log_id(cell), GetSize(slices)-1);
+ for (int i = 1; i < GetSize(slices); i++)
+ {
+ int slice_msb = slices[i]-1;
+ int slice_lsb = slices[i-1];
- SigSpec outsig = sigmap(cell->getPort(ID::Y));
- if (GetSize(outsig) <= 1) return 0;
+ IdString slice_name = module->uniquify(cell->name.str() + (slice_msb == slice_lsb ?
+ stringf("%c%d%c", format[0], slice_lsb, format[1]) :
+ stringf("%c%d%c%d%c", format[0], slice_msb, format[2], slice_lsb, format[1])));
+
+ Cell *slice = module->addCell(slice_name, cell);
+
+ auto slice_signal = [&](SigSpec old_sig) -> SigSpec {
+ SigSpec new_sig;
+ for (int i = 0; i < GetSize(old_sig); i += GetSize(outsig)) {
+ int offset = i+slice_lsb;
+ int length = std::min(GetSize(old_sig)-offset, slice_msb-slice_lsb+1);
+ new_sig.append(old_sig.extract(offset, length));
+ }
+ return new_sig;
+ };
+
+ slice->setPort(ID::A, slice_signal(slice->getPort(ID::A)));
+ if (slice->hasParam(ID::A_WIDTH))
+ slice->setParam(ID::A_WIDTH, GetSize(slice->getPort(ID::A)));
+
+ if (slice->hasPort(ID::B)) {
+ slice->setPort(ID::B, slice_signal(slice->getPort(ID::B)));
+ if (slice->hasParam(ID::B_WIDTH))
+ slice->setParam(ID::B_WIDTH, GetSize(slice->getPort(ID::B)));
+ }
- std::vector<int> slices;
- slices.push_back(0);
+ slice->setPort(ID::Y, slice_signal(slice->getPort(ID::Y)));
+ if (slice->hasParam(ID::Y_WIDTH))
+ slice->setParam(ID::Y_WIDTH, GetSize(slice->getPort(ID::Y)));
+ if (slice->hasParam(ID::WIDTH))
+ slice->setParam(ID::WIDTH, GetSize(slice->getPort(ID::Y)));
- int width = GetSize(outsig);
- width = std::min(width, GetSize(cell->getPort(ID::A)));
- if (cell->hasPort(ID::B))
- width = std::min(width, GetSize(cell->getPort(ID::B)));
+ log(" slice %d: %s => %s\n", i, log_id(slice_name), log_signal(slice->getPort(ID::Y)));
+ }
- for (int i = 1; i < width; i++) {
- auto &last_users = bit_users_db[outsig[slices.back()]];
- auto &this_users = bit_users_db[outsig[i]];
- if (last_users != this_users) slices.push_back(i);
+ module->remove(cell);
+ return GetSize(slices)-1;
}
- if (GetSize(slices) <= 1) return 0;
- slices.push_back(GetSize(outsig));
- log("Splitting %s cell %s/%s into %d slices:\n", log_id(cell->type), log_id(module), log_id(cell), GetSize(slices)-1);
- for (int i = 1; i < GetSize(slices); i++)
+ if (cell->type.in("$ff", "$dff", "$dffe", "$dffsr", "$dffsre", "$adff", "$adffe", "$aldffe",
+ "$sdff", "$sdffce", "$sdffe", "$dlatch", "$dlatchsr", "$adlatch"))
{
- int slice_msb = slices[i]-1;
- int slice_lsb = slices[i-1];
+ auto splitports = {ID::D, ID::Q, ID::AD, ID::SET, ID::CLR};
+ auto splitparams = {ID::ARST_VALUE, ID::SRST_VALUE};
+
+ SigSpec outsig = sigmap(cell->getPort(ID::Q));
+ if (GetSize(outsig) <= 1) return 0;
+ int width = GetSize(outsig);
+
+ std::vector<int> slices;
+ slices.push_back(0);
+
+ for (int i = 1; i < width; i++) {
+ auto &last_users = bit_users_db[outsig[slices.back()]];
+ auto &this_users = bit_users_db[outsig[i]];
+ if (last_users != this_users) slices.push_back(i);
+ }
+
+ if (GetSize(slices) <= 1) return 0;
+ slices.push_back(GetSize(outsig));
- IdString slice_name = module->uniquify(cell->name.str() + (slice_msb == slice_lsb ?
- stringf("%c%d%c", format[0], slice_lsb, format[1]) :
- stringf("%c%d%c%d%c", format[0], slice_msb, format[2], slice_lsb, format[1])));
+ log("Splitting %s cell %s/%s into %d slices:\n", log_id(cell->type), log_id(module), log_id(cell), GetSize(slices)-1);
+ for (int i = 1; i < GetSize(slices); i++)
+ {
+ int slice_msb = slices[i]-1;
+ int slice_lsb = slices[i-1];
- Cell *slice = module->addCell(slice_name, cell);
+ IdString slice_name = module->uniquify(cell->name.str() + (slice_msb == slice_lsb ?
+ stringf("%c%d%c", format[0], slice_lsb, format[1]) :
+ stringf("%c%d%c%d%c", format[0], slice_msb, format[2], slice_lsb, format[1])));
- auto slice_signal = [&](SigSpec old_sig) -> SigSpec {
- SigSpec new_sig;
- for (int i = 0; i < GetSize(old_sig); i += GetSize(outsig)) {
- int offset = i+slice_lsb;
- int length = std::min(GetSize(old_sig)-offset, slice_msb-slice_lsb+1);
- new_sig.append(old_sig.extract(offset, length));
+ Cell *slice = module->addCell(slice_name, cell);
+
+ for (IdString portname : splitports) {
+ if (slice->hasPort(portname)) {
+ SigSpec sig = slice->getPort(portname);
+ sig = sig.extract(slice_lsb, slice_msb-slice_lsb+1);
+ slice->setPort(portname, sig);
+ }
}
- return new_sig;
- };
- slice->setPort(ID::A, slice_signal(slice->getPort(ID::A)));
- if (slice->hasParam(ID::A_WIDTH))
- slice->setParam(ID::A_WIDTH, GetSize(slice->getPort(ID::A)));
+ for (IdString paramname : splitparams) {
+ if (slice->hasParam(paramname)) {
+ Const val = slice->getParam(paramname);
+ val = val.extract(slice_lsb, slice_msb-slice_lsb+1);
+ slice->setParam(paramname, val);
+ }
+ }
- if (slice->hasPort(ID::B)) {
- slice->setPort(ID::B, slice_signal(slice->getPort(ID::B)));
- if (slice->hasParam(ID::B_WIDTH))
- slice->setParam(ID::B_WIDTH, GetSize(slice->getPort(ID::B)));
- }
+ slice->setParam(ID::WIDTH, GetSize(slice->getPort(ID::Q)));
- slice->setPort(ID::Y, slice_signal(slice->getPort(ID::Y)));
- if (slice->hasParam(ID::Y_WIDTH))
- slice->setParam(ID::Y_WIDTH, GetSize(slice->getPort(ID::Y)));
- if (slice->hasParam(ID::WIDTH))
- slice->setParam(ID::WIDTH, GetSize(slice->getPort(ID::Y)));
+ log(" slice %d: %s => %s\n", i, log_id(slice_name), log_signal(slice->getPort(ID::Q)));
+ }
- log(" slice %d: %s => %s\n", i, log_id(slice_name), log_signal(slice->getPort(ID::Y)));
+ module->remove(cell);
+ return GetSize(slices)-1;
}
- module->remove(cell);
- return GetSize(slices)-1;
+ return 0;
}
};
@@ -179,14 +241,20 @@ struct SplitcellsPass : public Pass {
for (auto module : design->selected_modules())
{
- SplitcellsWorker worker(module);
int count_split_pre = 0;
int count_split_post = 0;
- for (auto cell : module->selected_cells()) {
- int n = worker.split(cell, format);
- count_split_pre += (n != 0);
- count_split_post += n;
+ while (1) {
+ SplitcellsWorker worker(module);
+ bool did_something = false;
+ for (auto cell : module->selected_cells()) {
+ int n = worker.split(cell, format);
+ did_something |= (n != 0);
+ count_split_pre += (n != 0);
+ count_split_post += n;
+ }
+ if (!did_something)
+ break;
}
if (count_split_pre)
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index 10e98952e..522957f39 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -275,6 +275,9 @@ struct statdata_t
log(" \"num_memory_bits\": %u,\n", num_memory_bits);
log(" \"num_processes\": %u,\n", num_processes);
log(" \"num_cells\": %u,\n", num_cells);
+ if (area != 0) {
+ log(" \"area\": %f,\n", area);
+ }
log(" \"num_cells_by_type\": {\n");
bool first_line = true;
for (auto &it : num_cells_by_type)
diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
index 5dee72e1b..5e78ff9fc 100644
--- a/passes/cmds/xprop.cc
+++ b/passes/cmds/xprop.cc
@@ -252,7 +252,8 @@ struct XpropWorker
}
if (!driven_orig.empty()) {
- module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+ auto decoder = module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+ decoder->set_bool_attribute(ID::xprop_decoder);
}
if (!driven_never_x.first.empty()) {
module->connect(driven_never_x);
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 27cec7549..e15e510be 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -33,6 +33,7 @@ struct EquivMakeWorker
bool inames;
vector<string> blacklists;
vector<string> encfiles;
+ bool make_assert;
pool<IdString> blacklist_names;
dict<IdString, dict<Const, Const>> encdata;
@@ -133,6 +134,12 @@ struct EquivMakeWorker
delete gate_clone;
}
+ void add_eq_assertion(const SigSpec &gold_sig, const SigSpec &gate_sig)
+ {
+ auto eq_wire = equiv_mod->Eqx(NEW_ID, gold_sig, gate_sig);
+ equiv_mod->addAssert(NEW_ID_SUFFIX("assert"), eq_wire, State::S1);
+ }
+
void find_same_wires()
{
SigMap assign_map(equiv_mod);
@@ -231,15 +238,24 @@ struct EquivMakeWorker
if (gold_wire->port_output || gate_wire->port_output)
{
- Wire *wire = equiv_mod->addWire(id, gold_wire->width);
- wire->port_output = true;
gold_wire->port_input = false;
gate_wire->port_input = false;
gold_wire->port_output = false;
gate_wire->port_output = false;
- for (int i = 0; i < wire->width; i++)
- equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+ wire->port_output = true;
+
+ if (make_assert)
+ {
+ add_eq_assertion(gold_wire, gate_wire);
+ equiv_mod->connect(wire, gold_wire);
+ }
+ else
+ {
+ for (int i = 0; i < wire->width; i++)
+ equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ }
rd_signal_map.add(assign_map(gold_wire), wire);
rd_signal_map.add(assign_map(gate_wire), wire);
@@ -259,26 +275,31 @@ struct EquivMakeWorker
}
else
{
- Wire *wire = equiv_mod->addWire(id, gold_wire->width);
- SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+ if (make_assert)
+ add_eq_assertion(gold_wire, gate_wire);
- for (int i = 0; i < wire->width; i++) {
- if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
- log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
- continue;
- }
- if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
- log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
- continue;
+ else {
+ Wire *wire = equiv_mod->addWire(id, gold_wire->width);
+ SigSpec rdmap_gold, rdmap_gate, rdmap_equiv;
+
+ for (int i = 0; i < wire->width; i++) {
+ if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) {
+ log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i);
+ continue;
+ }
+ if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) {
+ log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i);
+ continue;
+ }
+ equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
+ rdmap_gold.append(SigBit(gold_wire, i));
+ rdmap_gate.append(SigBit(gate_wire, i));
+ rdmap_equiv.append(SigBit(wire, i));
}
- equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i));
- rdmap_gold.append(SigBit(gold_wire, i));
- rdmap_gate.append(SigBit(gate_wire, i));
- rdmap_equiv.append(SigBit(wire, i));
- }
- rd_signal_map.add(rdmap_gold, rdmap_equiv);
- rd_signal_map.add(rdmap_gate, rdmap_equiv);
+ rd_signal_map.add(rdmap_gold, rdmap_equiv);
+ rd_signal_map.add(rdmap_gate, rdmap_equiv);
+ }
}
}
@@ -335,12 +356,20 @@ struct EquivMakeWorker
continue;
}
- for (int i = 0; i < GetSize(gold_sig); i++)
- if (gold_sig[i] != gate_sig[i]) {
- Wire *w = equiv_mod->addWire(NEW_ID);
- equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w);
- gold_sig[i] = w;
- }
+ if (make_assert)
+ {
+ if (gold_sig != gate_sig)
+ add_eq_assertion(gold_sig, gate_sig);
+ }
+ else
+ {
+ for (int i = 0; i < GetSize(gold_sig); i++)
+ if (gold_sig[i] != gate_sig[i]) {
+ Wire *w = equiv_mod->addWire(NEW_ID);
+ equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w);
+ gold_sig[i] = w;
+ }
+ }
gold_cell->setPort(gold_conn.first, gold_sig);
}
@@ -417,6 +446,10 @@ struct EquivMakePass : public Pass {
log(" Match FSM encodings using the description from the file.\n");
log(" See 'help fsm_recode' for details.\n");
log("\n");
+ log(" -make_assert\n");
+ log(" Check equivalence with $assert cells instead of $equiv.\n");
+ log(" $eqx (===) is used to compare signals.");
+ log("\n");
log("Note: The circuit created by this command is not a miter (with something like\n");
log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
@@ -427,6 +460,7 @@ struct EquivMakePass : public Pass {
EquivMakeWorker worker;
worker.ct.setup(design);
worker.inames = false;
+ worker.make_assert = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -443,6 +477,10 @@ struct EquivMakePass : public Pass {
worker.encfiles.push_back(args[++argidx]);
continue;
}
+ if (args[argidx] == "-make_assert") {
+ worker.make_assert = true;
+ continue;
+ }
break;
}
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index 5378ec89e..86d654cc4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -118,7 +118,7 @@ static bool check_state_users(RTLIL::SigSpec sig)
return true;
}
-static void detect_fsm(RTLIL::Wire *wire)
+static void detect_fsm(RTLIL::Wire *wire, bool ignore_self_reset=false)
{
bool has_fsm_encoding_attr = wire->attributes.count(ID::fsm_encoding) > 0 && wire->attributes.at(ID::fsm_encoding).decode_string() != "none";
bool has_fsm_encoding_none = wire->attributes.count(ID::fsm_encoding) > 0 && wire->attributes.at(ID::fsm_encoding).decode_string() == "none";
@@ -199,7 +199,7 @@ static void detect_fsm(RTLIL::Wire *wire)
}
SigSpec sig_y = sig_d, sig_undef;
- if (ce.eval(sig_y, sig_undef))
+ if (!ignore_self_reset && ce.eval(sig_y, sig_undef))
is_self_resetting = true;
}
@@ -261,12 +261,15 @@ struct FsmDetectPass : public Pass {
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" fsm_detect [selection]\n");
+ log(" fsm_detect [options] [selection]\n");
log("\n");
log("This pass detects finite state machines by identifying the state signal.\n");
log("The state signal is then marked by setting the attribute 'fsm_encoding'\n");
log("on the state signal to \"auto\".\n");
log("\n");
+ log(" -ignore-self-reset\n");
+ log(" Mark FSMs even if they are self-resetting\n");
+ log("\n");
log("Existing 'fsm_encoding' attributes are not changed by this pass.\n");
log("\n");
log("Signals can be protected from being detected by this pass by setting the\n");
@@ -276,16 +279,28 @@ struct FsmDetectPass : public Pass {
log("before this pass to prepare the design for fsm_detect.\n");
log("\n");
#ifdef YOSYS_ENABLE_VERIFIC
- log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n");
+ log("The Verific frontend may optimize the design in a way that interferes with FSM\n");
log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n");
- log("reading the source, and 'bmuxmap' after 'proc' for best results.\n");
+ log("reading the source, and 'bmuxmap -pmux' after 'proc' for best results.\n");
log("\n");
#endif
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
log_header(design, "Executing FSM_DETECT pass (finding FSMs in design).\n");
- extra_args(args, 1, design);
+
+ bool ignore_self_reset = false;
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-ignore-self-reset") {
+ ignore_self_reset = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
CellTypes ct;
ct.setup_internals();
@@ -321,7 +336,7 @@ struct FsmDetectPass : public Pass {
sig_at_port.add(assign_map(wire));
for (auto wire : module->selected_wires())
- detect_fsm(wire);
+ detect_fsm(wire, ignore_self_reset);
}
assign_map.clear();
diff --git a/passes/opt/opt_ffinv.cc b/passes/opt/opt_ffinv.cc
index 5d989dafd..3f7b4bc4a 100644
--- a/passes/opt/opt_ffinv.cc
+++ b/passes/opt/opt_ffinv.cc
@@ -64,6 +64,7 @@ struct OptFfInvWorker
log_assert(d_inv == nullptr);
d_inv = port.cell;
}
+ if (!d_inv) return false;
if (index.query_is_output(ff.sig_q))
return false;
@@ -140,6 +141,7 @@ struct OptFfInvWorker
log_assert(d_lut == nullptr);
d_lut = port.cell;
}
+ if (!d_lut) return false;
if (index.query_is_output(ff.sig_q))
return false;
@@ -167,6 +169,7 @@ struct OptFfInvWorker
log_assert(q_inv == nullptr);
q_inv = port.cell;
}
+ if (!q_inv) return false;
ff.flip_rst_bits({0});
ff.sig_q = q_inv->getPort(ID::Y);
diff --git a/passes/proc/proc_dff.cc b/passes/proc/proc_dff.cc
index 234671df5..fd56786f2 100644
--- a/passes/proc/proc_dff.cc
+++ b/passes/proc/proc_dff.cc
@@ -302,7 +302,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
ce.assign_map.apply(rstval);
ce.assign_map.apply(sig);
- if (rstval == sig) {
+ if (rstval == sig && sync_level) {
if (sync_level->type == RTLIL::SyncType::ST1)
insig = mod->Mux(NEW_ID, insig, sig, sync_level->signal);
else
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index e36379096..264a9fb3b 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -317,6 +317,172 @@ struct InitValWorker
}
};
+struct ReplacedPort {
+ IdString name;
+ int offset;
+ bool clk_pol;
+};
+
+struct HierarchyWorker
+{
+ Design *design;
+ pool<Module *> pending;
+
+ dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs;
+
+ HierarchyWorker(Design *design) :
+ design(design)
+ {
+ for (auto module : design->modules())
+ pending.insert(module);
+ }
+
+ void propagate();
+
+ const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type);
+};
+
+// Propagates replaced clock signals
+struct PropagateWorker
+{
+ HierarchyWorker &hierarchy;
+
+ Module *module;
+ SigMap sigmap;
+
+ dict<SigBit, bool> replaced_clk_bits;
+ dict<SigBit, SigBit> not_drivers;
+
+ std::vector<ReplacedPort> replaced_clk_inputs;
+ std::vector<std::pair<SigBit, bool>> pending;
+
+ PropagateWorker(Module *module, HierarchyWorker &hierarchy) :
+ hierarchy(hierarchy), module(module), sigmap(module)
+ {
+ hierarchy.pending.erase(module);
+
+ for (auto wire : module->wires())
+ if (wire->has_attribute(ID::replaced_by_gclk))
+ replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false);
+
+ for (auto cell : module->cells()) {
+ if (cell->type.in(ID($not), ID($_NOT_))) {
+ auto sig_a = cell->getPort(ID::A);
+ auto &sig_y = cell->getPort(ID::Y);
+ sig_a.extend_u0(GetSize(sig_y), cell->hasParam(ID::A_SIGNED) && cell->parameters.at(ID::A_SIGNED).as_bool());
+
+ for (int i = 0; i < GetSize(sig_a); i++)
+ if (sig_a[i].is_wire())
+ not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i]));
+ } else {
+ for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type))
+ replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true);
+ }
+ }
+
+ while (!pending.empty()) {
+ auto current = pending.back();
+ pending.pop_back();
+ auto it = not_drivers.find(current.first);
+ if (it == not_drivers.end())
+ continue;
+
+ replace_clk_bit(it->second, !current.second, true);
+ }
+
+ for (auto cell : module->cells()) {
+ if (cell->type.in(ID($not), ID($_NOT_)))
+ continue;
+ for (auto &conn : cell->connections()) {
+ if (!cell->output(conn.first))
+ continue;
+ for (SigBit bit : conn.second) {
+ sigmap.apply(bit);
+ if (replaced_clk_bits.count(bit))
+ log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n",
+ log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module));
+ }
+ }
+ }
+
+ for (auto port : module->ports) {
+ auto wire = module->wire(port);
+ if (!wire->port_input)
+ continue;
+ for (int i = 0; i < GetSize(wire); i++) {
+ SigBit bit(wire, i);
+ sigmap.apply(bit);
+ auto it = replaced_clk_bits.find(bit);
+ if (it == replaced_clk_bits.end())
+ continue;
+ replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second});
+
+ if (it->second) {
+ bit = module->Not(NEW_ID, bit);
+ }
+ }
+ }
+ }
+
+ void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute)
+ {
+ sigmap.apply(bit);
+ if (!bit.is_wire())
+ log_error("XXX todo\n");
+
+ auto it = replaced_clk_bits.find(bit);
+ if (it != replaced_clk_bits.end()) {
+ if (it->second != polarity)
+ log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n",
+ log_signal(bit), log_id(module));
+ return;
+ }
+
+ replaced_clk_bits.emplace(bit, polarity);
+
+ if (add_attribute) {
+ Wire *clk_wire = bit.wire;
+ if (bit.offset != 0 || GetSize(bit.wire) != 1) {
+ clk_wire = module->addWire(NEW_ID);
+ module->connect(RTLIL::SigBit(clk_wire), bit);
+ }
+ clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0;
+ clk_wire->set_bool_attribute(ID::keep);
+ }
+
+ pending.emplace_back(bit, polarity);
+ }
+};
+
+const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type)
+{
+ static const std::vector<ReplacedPort> empty;
+ if (!cell_type.isPublic())
+ return empty;
+
+ Module *module = design->module(cell_type);
+ if (module == nullptr)
+ return empty;
+
+ auto it = replaced_clk_inputs.find(module);
+ if (it != replaced_clk_inputs.end())
+ return it->second;
+
+ if (pending.count(module)) {
+ PropagateWorker worker(module, *this);
+ return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second;
+ }
+
+ return empty;
+}
+
+
+void HierarchyWorker::propagate()
+{
+ while (!pending.empty())
+ PropagateWorker worker(pending.pop(), *this);
+}
+
struct FormalFfPass : public Pass {
FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
void help() override
@@ -362,6 +528,15 @@ struct FormalFfPass : public Pass {
log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
log(" cells that drive wires with private names.\n");
log("\n");
+ log(" -hierarchy\n");
+ log(" Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n");
+ log(" through the design hierarchy towards the toplevel inputs. This option\n");
+ log(" works on the whole design and ignores the selection.\n");
+ log("\n");
+ log(" -assume\n");
+ log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n");
+ log(" attribute to the value they would have before an active clock edge.\n");
+ log("\n");
// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
}
@@ -372,6 +547,8 @@ struct FormalFfPass : public Pass {
bool flag_anyinit2ff = false;
bool flag_fine = false;
bool flag_setundef = false;
+ bool flag_hierarchy = false;
+ bool flag_assume = false;
log_header(design, "Executing FORMALFF pass.\n");
@@ -398,12 +575,20 @@ struct FormalFfPass : public Pass {
flag_setundef = true;
continue;
}
+ if (args[argidx] == "-hierarchy") {
+ flag_hierarchy = true;
+ continue;
+ }
+ if (args[argidx] == "-assume") {
+ flag_assume = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
- if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
- log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
+ if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
+ log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
if (flag_ff2anyinit && flag_anyinit2ff)
log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
@@ -548,6 +733,33 @@ struct FormalFfPass : public Pass {
ff.emit();
}
}
+
+ if (flag_hierarchy) {
+ HierarchyWorker worker(design);
+ worker.propagate();
+ }
+
+ if (flag_assume) {
+ for (auto module : design->selected_modules()) {
+ std::vector<pair<SigBit, bool>> found;
+ for (auto wire : module->wires()) {
+ if (!wire->has_attribute(ID::replaced_by_gclk))
+ continue;
+ bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1;
+
+ found.emplace_back(SigSpec(wire), clk_pol);
+ }
+ for (auto pair : found) {
+ SigBit clk = pair.first;
+
+ if (pair.second)
+ clk = module->Not(NEW_ID, clk);
+
+ module->addAssume(NEW_ID, clk, State::S1);
+
+ }
+ }
+ }
}
} FormalFfPass;
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 0084a1f28..7c209f516 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -23,6 +23,8 @@
#include "kernel/mem.h"
#include "kernel/fstdata.h"
#include "kernel/ff.h"
+#include "kernel/yw.h"
+#include "kernel/json.h"
#include <ctime>
@@ -74,6 +76,17 @@ struct OutputWriter
SimWorker *worker;
};
+struct SimInstance;
+struct TriggeredAssertion {
+ int step;
+ SimInstance *instance;
+ Cell *cell;
+
+ TriggeredAssertion(int step, SimInstance *instance, Cell *cell) :
+ step(step), instance(instance), cell(cell)
+ { }
+};
+
struct SimShared
{
bool debug = false;
@@ -93,6 +106,9 @@ struct SimShared
bool ignore_x = false;
bool date = false;
bool multiclock = false;
+ int next_output_id = 0;
+ int step = 0;
+ std::vector<TriggeredAssertion> triggered_assertions;
};
void zinit(State &v)
@@ -123,6 +139,8 @@ struct SimInstance
dict<SigBit, pool<Cell*>> upd_cells;
dict<SigBit, pool<Wire*>> upd_outports;
+ dict<SigBit, SigBit> in_parent_drivers;
+
pool<SigBit> dirty_bits;
pool<Cell*> dirty_cells;
pool<IdString> dirty_memories;
@@ -152,11 +170,14 @@ struct SimInstance
dict<Cell*, ff_state_t> ff_database;
dict<IdString, mem_state_t> mem_database;
pool<Cell*> formal_database;
+ pool<Cell*> initstate_database;
dict<Cell*, IdString> mem_cells;
std::vector<Mem> memories;
dict<Wire*, pair<int, Const>> signal_database;
+ dict<IdString, std::map<int, pair<int, Const>>> trace_mem_database;
+ dict<std::pair<IdString, int>, Const> trace_mem_init_database;
dict<Wire*, fstHandle> fst_handles;
dict<Wire*, fstHandle> fst_inputs;
dict<IdString, dict<int,fstHandle>> fst_memories;
@@ -199,6 +220,12 @@ struct SimInstance
dirty_bits.insert(sig[i]);
}
}
+
+ if (wire->port_input && instance != nullptr && parent != nullptr) {
+ for (int i = 0; i < GetSize(sig); i++) {
+ in_parent_drivers.emplace(sig[i], parent->sigmap(instance->getPort(wire->name)[i]));
+ }
+ }
}
memories = Mem::get_all_memories(module);
@@ -254,6 +281,8 @@ struct SimInstance
if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
formal_database.insert(cell);
}
+ if (cell->type == ID($initstate))
+ initstate_database.insert(cell);
}
if (shared->zinit)
@@ -300,6 +329,21 @@ struct SimInstance
return log_id(module->name);
}
+ vector<std::string> witness_full_path() const
+ {
+ if (instance != nullptr)
+ return parent->witness_full_path(instance);
+ return vector<std::string>();
+ }
+
+ vector<std::string> witness_full_path(Cell *cell) const
+ {
+ auto result = witness_full_path();
+ auto cell_path = witness_path(cell);
+ result.insert(result.end(), cell_path.begin(), cell_path.end());
+ return result;
+ }
+
Const get_state(SigSpec sig)
{
Const value;
@@ -325,7 +369,7 @@ struct SimInstance
log_assert(GetSize(sig) <= GetSize(value));
for (int i = 0; i < GetSize(sig); i++)
- if (state_nets.at(sig[i]) != value[i]) {
+ if (value[i] != State::Sa && state_nets.at(sig[i]) != value[i]) {
state_nets.at(sig[i]) = value[i];
dirty_bits.insert(sig[i]);
did_something = true;
@@ -336,14 +380,41 @@ struct SimInstance
return did_something;
}
+ void set_state_parent_drivers(SigSpec sig, Const value)
+ {
+ sigmap.apply(sig);
+
+ for (int i = 0; i < GetSize(sig); i++) {
+ auto sigbit = sig[i];
+ auto sigval = value[i];
+
+ auto in_parent_driver = in_parent_drivers.find(sigbit);
+ if (in_parent_driver == in_parent_drivers.end())
+ set_state(sigbit, sigval);
+ else
+ parent->set_state_parent_drivers(in_parent_driver->second, sigval);
+ }
+ }
+
void set_memory_state(IdString memid, Const addr, Const data)
{
+ set_memory_state(memid, addr.as_int(), data);
+ }
+
+ void set_memory_state(IdString memid, int addr, Const data)
+ {
auto &state = mem_database[memid];
- int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
+ bool dirty = false;
+
+ int offset = (addr - state.mem->start_offset) * state.mem->width;
for (int i = 0; i < GetSize(data); i++)
- if (0 <= i+offset && i+offset < state.mem->size * state.mem->width)
- state.data.bits[i+offset] = data.bits[i];
+ if (0 <= i+offset && i+offset < state.mem->size * state.mem->width && data.bits[i] != State::Sa)
+ if (state.data.bits[i+offset] != data.bits[i])
+ dirty = true, state.data.bits[i+offset] = data.bits[i];
+
+ if (dirty)
+ dirty_memories.insert(memid);
}
void set_memory_state_bit(IdString memid, int offset, State data)
@@ -351,7 +422,10 @@ struct SimInstance
auto &state = mem_database[memid];
if (offset >= state.mem->size * state.mem->width)
log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid));
- state.data.bits[offset] = data;
+ if (state.data.bits[offset] != data) {
+ state.data.bits[offset] = data;
+ dirty_memories.insert(memid);
+ }
}
void update_cell(Cell *cell)
@@ -447,9 +521,14 @@ struct SimInstance
log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid));
if (addr.is_fully_def()) {
- int index = addr.as_int() - mem.start_offset;
+ int addr_int = addr.as_int();
+ int index = addr_int - mem.start_offset;
if (index >= 0 && index < mem.size)
data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2);
+
+ for (int offset = 0; offset < 1 << port.wide_log2; offset++) {
+ register_memory_addr(id, addr_int + offset);
+ }
}
set_state(port.data, data);
@@ -604,7 +683,8 @@ struct SimInstance
if (addr.is_fully_def())
{
- int index = addr.as_int() - mem.start_offset;
+ int addr_int = addr.as_int();
+ int index = addr_int - mem.start_offset;
if (index >= 0 && index < mem.size)
for (int i = 0; i < (mem.width << port.wide_log2); i++)
if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) {
@@ -612,6 +692,9 @@ struct SimInstance
dirty_memories.insert(mem.memid);
did_something = true;
}
+
+ for (int i = 0; i < 1 << port.wide_log2; i++)
+ register_memory_addr(it.first, addr_int + i);
}
}
}
@@ -625,7 +708,7 @@ struct SimInstance
return did_something;
}
- void update_ph3()
+ void update_ph3(bool check_assertions)
{
for (auto &it : ff_database)
{
@@ -660,27 +743,42 @@ struct SimInstance
}
}
- for (auto cell : formal_database)
+ if (check_assertions)
{
- string label = log_id(cell);
- if (cell->attributes.count(ID::src))
- label = cell->attributes.at(ID::src).decode_string();
+ for (auto cell : formal_database)
+ {
+ string label = log_id(cell);
+ if (cell->attributes.count(ID::src))
+ label = cell->attributes.at(ID::src).decode_string();
+
+ State a = get_state(cell->getPort(ID::A))[0];
+ State en = get_state(cell->getPort(ID::EN))[0];
- State a = get_state(cell->getPort(ID::A))[0];
- State en = get_state(cell->getPort(ID::EN))[0];
+ if (en == State::S1 && (cell->type == ID($cover) ? a == State::S1 : a != State::S1)) {
+ shared->triggered_assertions.emplace_back(shared->step, this, cell);
+ }
- if (cell->type == ID($cover) && en == State::S1 && a != State::S1)
- log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
+ if (cell->type == ID($cover) && en == State::S1 && a == State::S1)
+ log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
- if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
- log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+ if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
+ log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
- if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
- log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+ if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
+ log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+ }
}
for (auto it : children)
- it.second->update_ph3();
+ it.second->update_ph3(check_assertions);
+ }
+
+ void set_initstate_outputs(State state)
+ {
+ for (auto cell : initstate_database)
+ set_state(cell->getPort(ID::Y), state);
+ for (auto child : children)
+ child.second->set_initstate_outputs(state);
}
void writeback(pool<Module*> &wbmods)
@@ -741,7 +839,7 @@ struct SimInstance
child.second->register_signals(id);
}
- void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, Wire*, int, bool)> register_signal)
+ void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, int, Wire*, int, bool)> register_signal)
{
int exit_scopes = 1;
if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) {
@@ -774,11 +872,45 @@ struct SimInstance
hdlname.pop_back();
for (auto name : hdlname)
enter_scope("\\" + name);
- register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ register_signal(signal_name.c_str(), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0);
for (auto name : hdlname)
exit_scope();
} else
- register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ register_signal(log_id(signal.first->name), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ }
+
+ for (auto &trace_mem : trace_mem_database)
+ {
+ auto memid = trace_mem.first;
+ auto &mdb = mem_database.at(memid);
+ Cell *cell = mdb.mem->cell;
+
+ std::vector<std::string> hdlname;
+ std::string signal_name;
+ bool has_hdlname = shared->hdlname && cell != nullptr && cell->name.isPublic() && cell->has_attribute(ID::hdlname);
+
+ if (has_hdlname) {
+ hdlname = cell->get_hdlname_attribute();
+ log_assert(!hdlname.empty());
+ signal_name = std::move(hdlname.back());
+ hdlname.pop_back();
+ for (auto name : hdlname)
+ enter_scope("\\" + name);
+ } else {
+ signal_name = log_id(memid);
+ }
+
+ for (auto &trace_index : trace_mem.second) {
+ int output_id = trace_index.second.first;
+ int index = trace_index.first;
+ register_signal(
+ stringf("%s[%d]", signal_name.c_str(), (index + mdb.mem->start_offset)).c_str(),
+ mdb.mem->width, nullptr, output_id, true);
+ }
+
+ if (has_hdlname)
+ for (auto name : hdlname)
+ exit_scope();
}
for (auto child : children)
@@ -788,6 +920,30 @@ struct SimInstance
exit_scope();
}
+ void register_memory_addr(IdString memid, int addr)
+ {
+ auto &mdb = mem_database.at(memid);
+ auto &mem = *mdb.mem;
+ int index = addr - mem.start_offset;
+ if (index < 0 || index >= mem.size)
+ return;
+ auto it = trace_mem_database.find(memid);
+ if (it != trace_mem_database.end() && it->second.count(index))
+ return;
+ int output_id = shared->next_output_id++;
+ Const data;
+ if (!shared->output_data.empty()) {
+ auto init_it = trace_mem_init_database.find(std::make_pair(memid, addr));
+ if (init_it != trace_mem_init_database.end())
+ data = init_it->second;
+ else
+ data = mem.get_init_data().extract(index * mem.width, mem.width);
+ shared->output_data.front().second.emplace(output_id, data);
+ }
+ trace_mem_database[memid].emplace(index, make_pair(output_id, data));
+
+ }
+
void register_output_step_values(std::map<int,Const> *data)
{
for (auto &it : signal_database)
@@ -803,6 +959,26 @@ struct SimInstance
data->emplace(id, value);
}
+ for (auto &trace_mem : trace_mem_database)
+ {
+ auto memid = trace_mem.first;
+ auto &mdb = mem_database.at(memid);
+ auto &mem = *mdb.mem;
+ for (auto &trace_index : trace_mem.second)
+ {
+ int output_id = trace_index.second.first;
+ int index = trace_index.first;
+
+ auto value = mdb.data.extract(index * mem.width, mem.width);
+
+ if (trace_index.second.second == value)
+ continue;
+
+ trace_index.second.second = value;
+ data->emplace(output_id, value);
+ }
+ }
+
for (auto child : children)
child.second->register_output_step_values(data);
}
@@ -946,6 +1122,7 @@ struct SimWorker : SimShared
std::string timescale;
std::string sim_filename;
std::string map_filename;
+ std::string summary_filename;
std::string scope;
~SimWorker()
@@ -956,8 +1133,8 @@ struct SimWorker : SimShared
void register_signals()
{
- int id = 1;
- top->register_signals(id);
+ next_output_id = 1;
+ top->register_signals(top->shared->next_output_id);
}
void register_output_step(int t)
@@ -989,6 +1166,9 @@ struct SimWorker : SimShared
void update(bool gclk)
{
+ if (gclk)
+ step += 1;
+
while (1)
{
if (debug)
@@ -1006,7 +1186,7 @@ struct SimWorker : SimShared
if (debug)
log("\n-- ph3 --\n");
- top->update_ph3();
+ top->update_ph3(gclk);
}
void initialize_stable_past()
@@ -1016,7 +1196,7 @@ struct SimWorker : SimShared
top->update_ph1();
if (debug)
log("\n-- ph3 (initialize) --\n");
- top->update_ph3();
+ top->update_ph3(true);
}
void set_inports(pool<IdString> ports, State value)
@@ -1490,6 +1670,242 @@ struct SimWorker : SimShared
write_output_files();
}
+ struct FoundYWPath
+ {
+ SimInstance *instance;
+ Wire *wire;
+ IdString memid;
+ int addr;
+ };
+
+ struct YwHierarchy {
+ dict<IdPath, FoundYWPath> paths;
+ };
+
+ YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw)
+ {
+ YwHierarchy hierarchy;
+ pool<IdPath> paths;
+ dict<IdPath, pool<IdString>> mem_paths;
+
+ for (auto &signal : yw.signals)
+ paths.insert(signal.path);
+
+ for (auto &clock : yw.clocks)
+ paths.insert(clock.path);
+
+ for (auto &path : paths)
+ if (path.has_address())
+ mem_paths[path.prefix()].insert(path.back());
+
+ witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) {
+ if (item.cell != nullptr)
+ return instance->children.at(item.cell);
+ if (item.wire != nullptr) {
+ if (paths.count(path)) {
+ if (debug)
+ log("witness hierarchy: found wire %s\n", path.str().c_str());
+ bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
+ if (!inserted)
+ log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
+ }
+ } else if (item.mem) {
+ auto it = mem_paths.find(path);
+ if (it != mem_paths.end()) {
+ if (debug)
+ log("witness hierarchy: found mem %s\n", path.str().c_str());
+ IdPath word_path = path;
+ word_path.emplace_back();
+ for (auto addr_part : it->second) {
+ word_path.back() = addr_part;
+ int addr;
+ word_path.get_address(addr);
+ if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size)
+ continue;
+ bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
+ if (!inserted)
+ log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
+ }
+ }
+ }
+ return instance;
+ });
+
+ for (auto &path : paths)
+ if (!hierarchy.paths.count(path))
+ log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str());
+
+ dict<IdPath, dict<int, bool>> clock_inputs;
+
+ for (auto &clock : yw.clocks) {
+ if (clock.is_negedge == clock.is_posedge)
+ continue;
+ clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge);
+ }
+ for (auto &signal : yw.signals) {
+ auto it = clock_inputs.find(signal.path);
+ if (it == clock_inputs.end())
+ continue;
+
+ for (auto &clock_input : it->second) {
+ int offset = clock_input.first;
+ if (offset >= signal.offset && (offset - signal.offset) < signal.width) {
+ int clock_bits_offset = signal.bits_offset + (offset - signal.offset);
+
+ State expected = clock_input.second ? State::S0 : State::S1;
+
+ for (int t = 0; t < GetSize(yw.steps); t++) {
+ if (yw.get_bits(t, clock_bits_offset, 1) != expected)
+ log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t);
+ }
+ }
+ }
+ }
+ // TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file
+
+ return hierarchy;
+ }
+
+ void set_yw_state(const ReadWitness &yw, const YwHierarchy &hierarchy, int t)
+ {
+ log_assert(t >= 0 && t < GetSize(yw.steps));
+
+ for (auto &signal : yw.signals) {
+ if (signal.init_only && t >= 1)
+ continue;
+ auto found_path_it = hierarchy.paths.find(signal.path);
+ if (found_path_it == hierarchy.paths.end())
+ continue;
+ auto &found_path = found_path_it->second;
+
+ Const value = yw.get_bits(t, signal.bits_offset, signal.width);
+
+ if (debug)
+ log("yw: set %s to %s\n", signal.path.str().c_str(), log_const(value));
+
+ if (found_path.wire != nullptr) {
+ found_path.instance->set_state_parent_drivers(
+ SigChunk(found_path.wire, signal.offset, signal.width),
+ value);
+ } else if (!found_path.memid.empty()) {
+ if (t >= 1)
+ found_path.instance->register_memory_addr(found_path.memid, found_path.addr);
+ else
+ found_path.instance->trace_mem_init_database.emplace(make_pair(found_path.memid, found_path.addr), value);
+ found_path.instance->set_memory_state(
+ found_path.memid, found_path.addr,
+ value);
+ }
+ }
+ }
+
+ void set_yw_clocks(const ReadWitness &yw, const YwHierarchy &hierarchy, bool active_edge)
+ {
+ for (auto &clock : yw.clocks) {
+ if (clock.is_negedge == clock.is_posedge)
+ continue;
+ auto found_path_it = hierarchy.paths.find(clock.path);
+ if (found_path_it == hierarchy.paths.end())
+ continue;
+ auto &found_path = found_path_it->second;
+
+ if (found_path.wire != nullptr) {
+ found_path.instance->set_state(
+ SigChunk(found_path.wire, clock.offset, 1),
+ active_edge == clock.is_posedge ? State::S1 : State::S0);
+ }
+ }
+ }
+
+ void run_cosim_yw_witness(Module *topmod, int append)
+ {
+ if (!clock.empty())
+ log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n");
+ if (!reset.empty())
+ log_cmd_error("The -reset option is not required nor supported when reading a Yosys witness file.\n");
+ if (multiclock)
+ log_warning("The -multiclock option is not required and ignored when reading a Yosys witness file.\n");
+
+ ReadWitness yw(sim_filename);
+
+ top = new SimInstance(this, scope, topmod);
+ register_signals();
+
+ YwHierarchy hierarchy = prepare_yw_hierarchy(yw);
+
+ if (yw.steps.empty()) {
+ log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str());
+ } else {
+ top->set_initstate_outputs(State::S1);
+ set_yw_state(yw, hierarchy, 0);
+ set_yw_clocks(yw, hierarchy, true);
+ initialize_stable_past();
+ register_output_step(0);
+
+ if (!yw.clocks.empty()) {
+ if (debug)
+ log("Simulating non-active clock edge.\n");
+ set_yw_clocks(yw, hierarchy, false);
+ update(false);
+ register_output_step(5);
+ }
+ top->set_initstate_outputs(State::S0);
+ }
+
+ for (int cycle = 1; cycle < GetSize(yw.steps) + append; cycle++)
+ {
+ if (verbose)
+ log("Simulating cycle %d.\n", cycle);
+ if (cycle < GetSize(yw.steps))
+ set_yw_state(yw, hierarchy, cycle);
+ set_yw_clocks(yw, hierarchy, true);
+ update(true);
+ register_output_step(10 * cycle);
+
+ if (!yw.clocks.empty()) {
+ if (debug)
+ log("Simulating non-active clock edge.\n");
+ set_yw_clocks(yw, hierarchy, false);
+ update(false);
+ register_output_step(5 + 10 * cycle);
+ }
+ }
+
+ register_output_step(10 * (GetSize(yw.steps) + append));
+ write_output_files();
+ }
+
+ void write_summary()
+ {
+ if (summary_filename.empty())
+ return;
+
+ PrettyJson json;
+ if (!json.write_to_file(summary_filename))
+ log_error("Can't open file `%s' for writing: %s\n", summary_filename.c_str(), strerror(errno));
+
+ json.begin_object();
+ json.entry("version", "Yosys sim summary");
+ json.entry("generator", yosys_version_str);
+ json.entry("steps", step);
+ json.entry("top", log_id(top->module->name));
+ json.name("assertions");
+ json.begin_array();
+ for (auto &assertion : triggered_assertions) {
+ json.begin_object();
+ json.entry("step", assertion.step);
+ json.entry("type", log_id(assertion.cell->type));
+ json.entry("path", assertion.instance->witness_full_path(assertion.cell));
+ auto src = assertion.cell->get_string_attribute(ID::src);
+ if (!src.empty()) {
+ json.entry("src", src);
+ }
+ json.end_object();
+ }
+ json.end_array();
+ json.end_object();
+ }
+
std::string define_signal(Wire *wire)
{
std::stringstream f;
@@ -1734,9 +2150,15 @@ struct VCDWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
[this]() { vcdfile << stringf("$upscope $end\n");},
- [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
+ [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) {
if (use_signal.at(id)) {
- vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name);
+ // Works around gtkwave trying to parse everything past the last [ in a signal
+ // name. While the emitted range doesn't necessarily match the wire's range,
+ // this is consistent with the range gtkwave makes up if it doesn't find a
+ // range
+ std::string range = strchr(name, '[') ? stringf("[%d:0]", size - 1) : std::string();
+ vcdfile << stringf("$var %s %d n%d %s%s%s $end\n", is_reg ? "reg" : "wire", size, id, name[0] == '$' ? "\\" : "", name, range.c_str());
+
}
}
);
@@ -1796,9 +2218,9 @@ struct FSTWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
[this]() { fstWriterSetUpscope(fstfile); },
- [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
+ [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) {
if (!use_signal.at(id)) return;
- fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
+ fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, size,
name, 0);
mapping.emplace(id, fst_id);
}
@@ -1881,7 +2303,7 @@ struct AIWWriter : public OutputWriter
worker->top->write_output_header(
[](IdString) {},
[]() {},
- [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; }
+ [this](const char */*name*/, int /*size*/, Wire *wire, int id, bool) { if (wire != nullptr) mapping[wire] = id; }
);
std::map<int, Yosys::RTLIL::Const> current;
@@ -2013,11 +2435,17 @@ struct SimPass : public Pass {
log(" -w\n");
log(" writeback mode: use final simulation state as new init state\n");
log("\n");
- log(" -r\n");
- log(" read simulation results file\n");
- log(" File formats supported: FST, VCD, AIW and WIT\n");
+ log(" -r <filename>\n");
+ log(" read simulation or formal results file\n");
+ log(" File formats supported: FST, VCD, AIW, WIT and .yw\n");
log(" VCD support requires vcd2fst external tool to be present\n");
log("\n");
+ log(" -append <integer>\n");
+ log(" number of extra clock cycles to simulate for a Yosys witness input\n");
+ log("\n");
+ log(" -summary <filename>\n");
+ log(" write a JSON summary to the given file\n");
+ log("\n");
log(" -map <filename>\n");
log(" read file with port and latch symbols, needed for AIGER witness input\n");
log("\n");
@@ -2063,6 +2491,7 @@ struct SimPass : public Pass {
{
SimWorker worker;
int numcycles = 20;
+ int append = 0;
bool start_set = false, stop_set = false, at_set = false;
log_header(design, "Executing SIM pass (simulate the circuit).\n");
@@ -2146,12 +2575,22 @@ struct SimPass : public Pass {
worker.sim_filename = sim_filename;
continue;
}
+ if (args[argidx] == "-append" && argidx+1 < args.size()) {
+ append = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-map" && argidx+1 < args.size()) {
std::string map_filename = args[++argidx];
rewrite_filename(map_filename);
worker.map_filename = map_filename;
continue;
}
+ if (args[argidx] == "-summary" && argidx+1 < args.size()) {
+ std::string summary_filename = args[++argidx];
+ rewrite_filename(summary_filename);
+ worker.summary_filename = summary_filename;
+ continue;
+ }
if (args[argidx] == "-scope" && argidx+1 < args.size()) {
worker.scope = args[++argidx];
continue;
@@ -2235,10 +2674,14 @@ struct SimPass : public Pass {
worker.run_cosim_aiger_witness(top_mod);
} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
worker.run_cosim_btor2_witness(top_mod);
+ } else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) {
+ worker.run_cosim_yw_witness(top_mod, append);
} else {
log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
}
}
+
+ worker.write_summary();
}
} SimPass;
diff --git a/passes/techmap/bmuxmap.cc b/passes/techmap/bmuxmap.cc
index 03673c278..7aa67d3c0 100644
--- a/passes/techmap/bmuxmap.cc
+++ b/passes/techmap/bmuxmap.cc
@@ -33,13 +33,22 @@ struct BmuxmapPass : public Pass {
log("\n");
log("This pass transforms $bmux cells to trees of $mux cells.\n");
log("\n");
+ log(" -pmux\n");
+ log(" transform to $pmux instead of $mux cells.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
+ bool pmux_mode = false;
+
log_header(design, "Executing BMUXMAP pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-pmux") {
+ pmux_mode = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -53,18 +62,36 @@ struct BmuxmapPass : public Pass {
SigSpec sel = cell->getPort(ID::S);
SigSpec data = cell->getPort(ID::A);
int width = GetSize(cell->getPort(ID::Y));
+ int s_width = GetSize(cell->getPort(ID::S));
- for (int idx = 0; idx < GetSize(sel); idx++) {
- SigSpec new_data = module->addWire(NEW_ID, GetSize(data)/2);
- for (int i = 0; i < GetSize(new_data); i += width) {
- RTLIL::Cell *mux = module->addMux(NEW_ID,
+ if(pmux_mode)
+ {
+ int num_cases = 1 << s_width;
+ SigSpec new_a = SigSpec(State::Sx, width);
+ SigSpec new_s = module->addWire(NEW_ID, num_cases);
+ SigSpec new_data = module->addWire(NEW_ID, width);
+ for (int val = 0; val < num_cases; val++)
+ {
+ module->addEq(NEW_ID, sel, SigSpec(val, GetSize(sel)), new_s[val]);
+ }
+ RTLIL::Cell *pmux = module->addPmux(NEW_ID, new_a, data, new_s, new_data);
+ pmux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ data = new_data;
+ }
+ else
+ {
+ for (int idx = 0; idx < GetSize(sel); idx++) {
+ SigSpec new_data = module->addWire(NEW_ID, GetSize(data)/2);
+ for (int i = 0; i < GetSize(new_data); i += width) {
+ RTLIL::Cell *mux = module->addMux(NEW_ID,
data.extract(i*2, width),
data.extract(i*2+width, width),
sel[idx],
new_data.extract(i, width));
- mux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ mux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+ }
+ data = new_data;
}
- data = new_data;
}
module->connect(cell->getPort(ID::Y), data);
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-13 01:10:53 +0000