From 84a07ffb8a9eef2137d858802c5e7cce343fb53e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 22 Oct 2015 15:40:27 +0200 Subject: Added equiv_purge --- passes/equiv/Makefile.inc | 1 + passes/equiv/equiv_purge.cc | 209 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 210 insertions(+) create mode 100644 passes/equiv/equiv_purge.cc 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 + * + * 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 queue, visited; + + // cache for traversing signal flow graph + dict> up_bit2cells; + dict> 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 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 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 -- cgit v1.2.3