summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/equiv/Makefile.inc1
-rw-r--r--passes/equiv/equiv_miter.cc343
2 files changed, 344 insertions, 0 deletions
diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc
index 385170c9..c952fae5 100644
--- a/passes/equiv/Makefile.inc
+++ b/passes/equiv/Makefile.inc
@@ -1,5 +1,6 @@
OBJS += passes/equiv/equiv_make.o
+OBJS += passes/equiv/equiv_miter.o
OBJS += passes/equiv/equiv_simple.o
OBJS += passes/equiv/equiv_status.o
OBJS += passes/equiv/equiv_induct.o
diff --git a/passes/equiv/equiv_miter.cc b/passes/equiv/equiv_miter.cc
new file mode 100644
index 00000000..f9f11916
--- /dev/null
+++ b/passes/equiv/equiv_miter.cc
@@ -0,0 +1,343 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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/yosys.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EquivMiterWorker
+{
+ CellTypes ct;
+ SigMap sigmap;
+
+ bool mode_trigger;
+ bool mode_cmp;
+ bool mode_assert;
+ bool mode_undef;
+
+ IdString miter_name;
+ Module *miter_module;
+ Module *source_module;
+
+ dict<SigBit, Cell*> bit_to_driver;
+ pool<Cell*> seed_cells, miter_cells;
+ pool<Wire*> miter_wires;
+
+ void follow_cone(pool<Cell*> &cone, pool<Cell*> &leaves, Cell *c, bool gold_mode)
+ {
+ if (cone.count(c))
+ return;
+
+ if (c->type == "$equiv" && !seed_cells.count(c)) {
+ leaves.insert(c);
+ return;
+ }
+
+ cone.insert(c);
+
+ for (auto &conn : c->connections()) {
+ if (!ct.cell_input(c->type, conn.first))
+ continue;
+ if (c->type == "$equiv" && (conn.first == "\\A") != gold_mode)
+ continue;
+ for (auto bit : sigmap(conn.second))
+ if (bit_to_driver.count(bit))
+ follow_cone(cone, leaves, bit_to_driver.at(bit), gold_mode);
+ }
+ }
+
+ void find_miter_cells_wires()
+ {
+ sigmap.set(source_module);
+
+ // initialize bit_to_driver
+
+ for (auto c : source_module->cells())
+ for (auto &conn : c->connections())
+ if (ct.cell_output(c->type, conn.first))
+ for (auto bit : sigmap(conn.second))
+ if (bit.wire)
+ bit_to_driver[bit] = c;
+
+ // find seed cells
+
+ for (auto c : source_module->selected_cells())
+ if (c->type == "$equiv") {
+ log("Seed $equiv cell: %s\n", log_id(c));
+ seed_cells.insert(c);
+ }
+
+ // follow cone from seed cells to next $equiv
+
+ while (1)
+ {
+ pool<Cell*> gold_cone, gold_leaves;
+ pool<Cell*> gate_cone, gate_leaves;
+
+ for (auto c : seed_cells) {
+ follow_cone(gold_cone, gold_leaves, c, true);
+ follow_cone(gate_cone, gate_leaves, c, false);
+ }
+
+ log("Gold cone: %d cells (%d leaves).\n", GetSize(gold_cone), GetSize(gold_leaves));
+ log("Gate cone: %d cells (%d leaves).\n", GetSize(gate_cone), GetSize(gate_leaves));
+
+ // done if all leaves are shared leaves
+
+ if (gold_leaves == gate_leaves) {
+ miter_cells = gold_cone;
+ miter_cells.insert(gate_cone.begin(), gate_cone.end());
+ log("Selected %d miter cells.\n", GetSize(miter_cells));
+ break;
+ }
+
+ // remove shared leaves
+
+ for (auto it = gold_leaves.begin(); it != gold_leaves.end(); ) {
+ auto it2 = gate_leaves.find(*it);
+ if (it2 != gate_leaves.end()) {
+ it = gold_leaves.erase(it);
+ gate_leaves.erase(it2);
+ } else
+ ++it;
+ }
+
+ // add remaining leaves to seeds and re-run
+
+ log("Adding %d gold and %d gate seed cells.\n", GetSize(gold_leaves), GetSize(gate_leaves));
+ seed_cells.insert(gold_leaves.begin(), gold_leaves.end());
+ seed_cells.insert(gate_leaves.begin(), gate_leaves.end());
+ }
+
+ for (auto c : miter_cells)
+ for (auto &conn : c->connections())
+ for (auto bit : sigmap(conn.second))
+ if (bit.wire)
+ miter_wires.insert(bit.wire);
+ log("Selected %d miter wires.\n", GetSize(miter_wires));
+ }
+
+ void copy_to_miter()
+ {
+ // copy wires and cells
+
+ for (auto w : miter_wires)
+ miter_module->addWire(w->name, w->width);
+ for (auto c : miter_cells) {
+ miter_module->addCell(c->name, c);
+ auto mc = miter_module->cell(c->name);
+ for (auto &conn : mc->connections())
+ mc->setPort(conn.first, sigmap(conn.second));
+ }
+
+ // fixup wire references in cells
+
+ sigmap.clear();
+
+ struct RewriteSigSpecWorker {
+ RTLIL::Module * mod;
+ void operator()(SigSpec &sig) {
+ vector<RTLIL::SigChunk> chunks = sig.chunks();
+ for (auto &c : chunks)
+ if (c.wire != NULL)
+ c.wire = mod->wires_.at(c.wire->name);
+ sig = chunks;
+ }
+ };
+
+ RewriteSigSpecWorker rewriteSigSpecWorker;
+ rewriteSigSpecWorker.mod = miter_module;
+ miter_module->rewrite_sigspecs(rewriteSigSpecWorker);
+
+ // find undriven or unused wires
+
+ pool<SigBit> driven_bits, used_bits;
+
+ for (auto c : miter_module->cells())
+ for (auto &conn : c->connections()) {
+ if (ct.cell_input(c->type, conn.first))
+ for (auto bit : conn.second)
+ if (bit.wire)
+ used_bits.insert(bit);
+ if (ct.cell_output(c->type, conn.first))
+ for (auto bit : conn.second)
+ if (bit.wire)
+ driven_bits.insert(bit);
+ }
+
+ // create ports
+
+ for (auto w : miter_module->wires()) {
+ for (auto bit : SigSpec(w)) {
+ if (driven_bits.count(bit) && !used_bits.count(bit))
+ w->port_output = true;
+ if (!driven_bits.count(bit) && used_bits.count(bit))
+ w->port_input = true;
+ }
+ if (w->port_output && w->port_input)
+ log("Created miter inout port %s.\n", log_id(w));
+ else if (w->port_output)
+ log("Created miter output port %s.\n", log_id(w));
+ else if (w->port_input)
+ log("Created miter input port %s.\n", log_id(w));
+ }
+
+ miter_module->fixup_ports();
+ }
+
+ void make_stuff()
+ {
+ if (!mode_trigger && !mode_cmp && !mode_assert)
+ return;
+
+ SigSpec trigger_signals;
+ vector<Cell*> equiv_cells;
+
+ for (auto c : miter_module->cells())
+ if (c->type == "$equiv" && c->getPort("\\A") != c->getPort("\\B"))
+ equiv_cells.push_back(c);
+
+ for (auto c : equiv_cells)
+ {
+ SigSpec trigger = mode_undef ?
+ miter_module->Mux(NEW_ID, miter_module->Eqx(NEW_ID, c->getPort("\\A"), c->getPort("\\B")),
+ State::S1, miter_module->Eqx(NEW_ID, c->getPort("\\A"), State::Sx)) :
+ miter_module->Eq(NEW_ID, c->getPort("\\A"), c->getPort("\\B"));
+
+ if (mode_cmp) {
+ string cmp_name = string("\\cmp") + log_signal(c->getPort("\\Y"));
+ for (int i = 1; i < GetSize(cmp_name); i++)
+ if (cmp_name[i] == '\\')
+ cmp_name[i] = '_';
+ else if (cmp_name[i] == ' ')
+ cmp_name = cmp_name.substr(0, i) + cmp_name.substr(i+1);
+ auto w = miter_module->addWire(cmp_name);
+ w->port_output = true;
+ miter_module->connect(w, trigger);
+ }
+
+ if (mode_assert)
+ miter_module->addAssert(NEW_ID, miter_module->Not(NEW_ID, trigger), State::S1);
+
+ trigger_signals.append(trigger);
+ }
+
+ if (mode_trigger) {
+ auto w = miter_module->addWire("\\trigger");
+ w->port_output = true;
+ miter_module->addReduceOr(NEW_ID, trigger_signals, w);
+ }
+
+ miter_module->fixup_ports();
+ }
+
+ void run()
+ {
+ log("Creating miter %s from module %s.\n", log_id(miter_module), log_id(source_module));
+ find_miter_cells_wires();
+ copy_to_miter();
+ make_stuff();
+ }
+};
+
+struct EquivMiterPass : public Pass {
+ EquivMiterPass() : Pass("equiv_miter", "extract miter from equiv circuit") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" equiv_miter [options] miter_module [selection]\n");
+ log("\n");
+ log("This creates a miter module for further analysis of the selected $equiv cells.\n");
+ log("\n");
+ log(" -trigger\n");
+ log(" Create a trigger output\n");
+ log("\n");
+ log(" -cmp\n");
+ log(" Create cmp_* outputs for individual unproven $equiv cells\n");
+ log("\n");
+ log(" -assert\n");
+ log(" Create a $assert cell for each unproven $equiv cell\n");
+ log("\n");
+ log(" -undef\n");
+ log(" Create compare logic that handles undefs correctly\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ EquivMiterWorker worker;
+ worker.ct.setup(design);
+ worker.mode_trigger = false;
+ worker.mode_cmp = false;
+ worker.mode_assert = false;
+ worker.mode_undef = false;
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-trigger") {
+ worker.mode_trigger = true;
+ continue;
+ }
+ if (args[argidx] == "-cmp") {
+ worker.mode_cmp = true;
+ continue;
+ }
+ if (args[argidx] == "-assert") {
+ worker.mode_assert = true;
+ continue;
+ }
+ if (args[argidx] == "-undef") {
+ worker.mode_undef = true;
+ continue;
+ }
+ break;
+ }
+
+ if (argidx+1 >= args.size())
+ log_cmd_error("Invalid number of arguments.\n");
+
+ worker.miter_name = RTLIL::escape_id(args[argidx++]);
+ extra_args(args, argidx, design);
+
+ if (design->module(worker.miter_name))
+ log_cmd_error("Miter module %s already exists.\n", log_id(worker.miter_name));
+
+ worker.source_module = nullptr;
+ for (auto m : design->selected_modules()) {
+ if (worker.source_module != nullptr)
+ goto found_two_modules;
+ worker.source_module = m;
+ }
+
+ if (worker.source_module == nullptr)
+ found_two_modules:
+ log_cmd_error("Exactly one module must be selected for 'equiv_miter'!\n");
+
+ log_header("Executing EQUIV_MITER pass.\n");
+
+ worker.miter_module = design->addModule(worker.miter_name);
+ worker.run();
+ }
+} EquivMiterPass;
+
+PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-19 22:03:33 +0000