diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-10-22 15:40:27 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-10-22 15:40:27 +0200 |
commit | 84a07ffb8a9eef2137d858802c5e7cce343fb53e (patch) | |
tree | 7716ae8a936ee7e29908456e8f635d50880a3f85 | |
parent | 00e05b131092c3e8343ee4e4a2e6b863fc15f416 (diff) | |
download | yosys-84a07ffb8a9eef2137d858802c5e7cce343fb53e.tar.gz yosys-84a07ffb8a9eef2137d858802c5e7cce343fb53e.tar.bz2 yosys-84a07ffb8a9eef2137d858802c5e7cce343fb53e.zip |
Added equiv_purge
-rw-r--r-- | passes/equiv/Makefile.inc | 1 | ||||
-rw-r--r-- | passes/equiv/equiv_purge.cc | 209 |
2 files changed, 210 insertions, 0 deletions
diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc index d5bb9495a..4d6157429 100644 --- a/passes/equiv/Makefile.inc +++ b/passes/equiv/Makefile.inc @@ -7,4 +7,5 @@ OBJS += passes/equiv/equiv_add.o OBJS += passes/equiv/equiv_remove.o OBJS += passes/equiv/equiv_induct.o OBJS += passes/equiv/equiv_struct.o +OBJS += passes/equiv/equiv_purge.o diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc new file mode 100644 index 000000000..286bd3573 --- /dev/null +++ b/passes/equiv/equiv_purge.cc @@ -0,0 +1,209 @@ +/* + * 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" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct EquivPurgeWorker +{ + Module *module; + SigMap sigmap; + int name_cnt; + + EquivPurgeWorker(Module *module) : module(module), sigmap(module), name_cnt(0) { } + + SigSpec make_output(SigSpec sig, IdString cellname) + { + if (sig.is_wire()) { + Wire *wire = sig.as_wire(); + if (wire->name[0] == '\\') { + if (!wire->port_output) { + log(" Module output: %s (%s)\n", log_signal(wire), log_id(cellname)); + wire->port_output = true; + } + return wire; + } + } + + while (1) + { + IdString name = stringf("\\equiv_%d", name_cnt++); + if (module->count_id(name)) + continue; + + Wire *wire = module->addWire(name, GetSize(sig)); + wire->port_output = true; + module->connect(wire, sig); + log(" Module output: %s (%s)\n", log_signal(wire), log_id(cellname)); + return wire; + } + } + + SigSpec make_input(SigSpec sig) + { + if (sig.is_wire()) { + Wire *wire = sig.as_wire(); + if (wire->name[0] == '\\') { + if (!wire->port_output) { + log(" Module input: %s\n", log_signal(wire)); + wire->port_input = true; + } + return module->addWire(NEW_ID, GetSize(sig)); + } + } + + while (1) + { + IdString name = stringf("\\equiv_%d", name_cnt++); + if (module->count_id(name)) + continue; + + Wire *wire = module->addWire(name, GetSize(sig)); + wire->port_input = true; + module->connect(sig, wire); + log(" Module input: %s\n", log_signal(wire)); + return module->addWire(NEW_ID, GetSize(sig)); + } + } + + void run() + { + log("Running equiv_purge on module %s:", log_id(module)); + + for (auto wire : module->wires()) { + wire->port_input = false; + wire->port_output = false; + } + + pool<SigBit> queue, visited; + + // cache for traversing signal flow graph + dict<SigBit, pool<IdString>> up_bit2cells; + dict<IdString, pool<SigBit>> up_cell2bits; + + for (auto cell : module->cells()) + { + if (cell->type != "$equiv") { + for (auto &port : cell->connections()) { + if (cell->input(port.first)) + for (auto bit : sigmap(port.second)) + up_cell2bits[cell->name].insert(bit); + if (cell->output(port.first)) + for (auto bit : sigmap(port.second)) + up_bit2cells[bit].insert(cell->name); + } + continue; + } + + SigSpec sig_a = sigmap(cell->getPort("\\A")); + SigSpec sig_b = sigmap(cell->getPort("\\B")); + SigSpec sig_y = sigmap(cell->getPort("\\Y")); + + if (sig_a == sig_b) + continue; + + for (auto bit : sig_a) + queue.insert(bit); + + for (auto bit : sig_b) + queue.insert(bit); + + for (auto bit : sig_y) + visited.insert(bit); + + cell->setPort("\\Y", make_output(sig_y, cell->name)); + } + + SigSpec srcsig; + SigMap rewrite_sigmap(module); + + while (!queue.empty()) + { + pool<SigBit> next_queue; + + for (auto bit : queue) + visited.insert(bit); + + for (auto bit : queue) + { + auto &cells = up_bit2cells[bit]; + + if (cells.empty()) { + srcsig.append(bit); + } else { + for (auto cell : cells) + for (auto bit : up_cell2bits[cell]) + if (visited.count(bit) == 0) + next_queue.insert(bit); + } + } + + next_queue.swap(queue); + } + + srcsig.sort_and_unify(); + + for (SigSpec sig : srcsig.chunks()) + rewrite_sigmap.add(sig, make_input(sig)); + + for (auto cell : module->cells()) + if (cell->type == "$equiv") + cell->setPort("\\Y", rewrite_sigmap(sigmap(cell->getPort("\\Y")))); + + module->fixup_ports(); + } +}; + +struct EquivPurgePass : public Pass { + EquivPurgePass() : Pass("equiv_purge", "purge equivalence checking module") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" equiv_purge [options] [selection]\n"); + log("\n"); + log("This command removes the proven part of an equivalence checking module, leaving\n"); + log("only the unproven segments in the design. This will also remove and add module\n"); + log("ports as needed.\n"); + log("\n"); + } + virtual void execute(std::vector<std::string> args, Design *design) + { + log_header("Executing EQUIV_PURGE pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + // if (args[argidx] == "-foobar") { + // continue; + // } + break; + } + extra_args(args, argidx, design); + + for (auto module : design->selected_whole_modules_warn()) { + EquivPurgeWorker worker(module); + worker.run(); + } + } +} EquivPurgePass; + +PRIVATE_NAMESPACE_END |