From 66a6b86daa7f54336d193fab6979205284297cf2 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 25 Jan 2015 14:00:49 +0100 Subject: [PATCH] Added equiv_miter --- passes/equiv/Makefile.inc | 1 + passes/equiv/equiv_miter.cc | 343 ++++++++++++++++++++++++++++++++++++ 2 files changed, 344 insertions(+) create mode 100644 passes/equiv/equiv_miter.cc diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc index 385170c9a..c952fae54 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 000000000..f9f119162 --- /dev/null +++ b/passes/equiv/equiv_miter.cc @@ -0,0 +1,343 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * 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 bit_to_driver; + pool seed_cells, miter_cells; + pool miter_wires; + + void follow_cone(pool &cone, pool &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 gold_cone, gold_leaves; + pool 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 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 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 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 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 -- 2.30.2