From 4cec1c058d5cef6960e12bc4d5371aa853cb72d9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 23 Oct 2015 23:56:58 +0200 Subject: Added equiv_mark command --- passes/equiv/Makefile.inc | 1 + passes/equiv/equiv_mark.cc | 263 ++++++++++++++++++++++++++++++++++++++++++++ passes/equiv/equiv_purge.cc | 2 +- 3 files changed, 265 insertions(+), 1 deletion(-) create mode 100644 passes/equiv/equiv_mark.cc (limited to 'passes/equiv') diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc index 4d615742..dd7b3be0 100644 --- a/passes/equiv/Makefile.inc +++ b/passes/equiv/Makefile.inc @@ -8,4 +8,5 @@ OBJS += passes/equiv/equiv_remove.o OBJS += passes/equiv/equiv_induct.o OBJS += passes/equiv/equiv_struct.o OBJS += passes/equiv/equiv_purge.o +OBJS += passes/equiv/equiv_mark.o diff --git a/passes/equiv/equiv_mark.cc b/passes/equiv/equiv_mark.cc new file mode 100644 index 00000000..da61678d --- /dev/null +++ b/passes/equiv/equiv_mark.cc @@ -0,0 +1,263 @@ +/* + * 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 EquivMarkWorker +{ + Module *module; + SigMap sigmap; + + // cache for traversing signal flow graph + dict> up_bit2cells; + dict> up_cell2bits; + pool edge_cells, equiv_cells; + + // graph traversal state + pool queue, visited; + + // assigned regions + dict cell_regions; + dict bit_regions; + int next_region; + + // merge-find + dict region_mf; + + int region_find(int r) + { + vector backlog; + + while (region_mf.count(r)) { + backlog.push_back(r); + r = region_mf.at(r); + } + + for (int q : backlog) + region_mf[q] = r; + + return r; + } + + void region_merge(int r, int q) + { + r = region_find(r); + q = region_find(q); + + if (r != q) + region_mf[r] = q; + } + + EquivMarkWorker(Module *module) : module(module), sigmap(module) + { + for (auto cell : module->cells()) + { + if (cell->type == "$equiv") + equiv_cells.insert(cell->name); + + 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); + } + } + + next_region = 0; + } + + void mark() + { + while (!queue.empty()) + { + pool cells; + + for (auto &bit : queue) + { + // log_assert(bit_regions.count(bit) == 0); + bit_regions[bit] = next_region; + visited.insert(bit); + + for (auto cell : up_bit2cells[bit]) + if (edge_cells.count(cell) == 0) + cells.insert(cell); + } + + queue.clear(); + + for (auto cell : cells) + { + if (next_region == 0 && equiv_cells.count(cell)) + continue; + + if (cell_regions.count(cell)) { + if (cell_regions.at(cell) != 0) + region_merge(cell_regions.at(cell), next_region); + continue; + } + + cell_regions[cell] = next_region; + + for (auto bit : up_cell2bits[cell]) + if (visited.count(bit) == 0) + queue.insert(bit); + } + } + + next_region++; + } + + void run() + { + log("Running equiv_mark on module %s:\n", log_id(module)); + + // marking region 0 + + for (auto wire : module->wires()) + if (wire->port_id > 0) + for (auto bit : sigmap(wire)) + queue.insert(bit); + + for (auto cell_name : equiv_cells) + { + auto cell = module->cell(cell_name); + + SigSpec sig_a = sigmap(cell->getPort("\\A")); + SigSpec sig_b = sigmap(cell->getPort("\\B")); + + if (sig_a == sig_b) { + for (auto bit : sig_a) + queue.insert(bit); + edge_cells.insert(cell_name); + cell_regions[cell_name] = 0; + } + } + + mark(); + + // marking unsolved regions + + for (auto cell : module->cells()) + { + if (cell_regions.count(cell->name) || cell->type != "$equiv") + continue; + + SigSpec sig_a = sigmap(cell->getPort("\\A")); + SigSpec sig_b = sigmap(cell->getPort("\\B")); + + log_assert(sig_a != sig_b); + + for (auto bit : sig_a) + queue.insert(bit); + + for (auto bit : sig_b) + queue.insert(bit); + + cell_regions[cell->name] = next_region; + mark(); + } + + // setting attributes + + dict final_region_map; + int next_final_region = 0; + + dict region_cell_count; + dict region_wire_count; + + for (int i = 0; i < next_region; i++) { + int r = region_find(i); + if (final_region_map.count(r) == 0) + final_region_map[r] = next_final_region++; + final_region_map[i] = final_region_map[r]; + } + + for (auto cell : module->cells()) + { + if (cell_regions.count(cell->name)) { + int r = final_region_map.at(cell_regions.at(cell->name)); + cell->attributes["\\equiv_region"] = Const(r); + region_cell_count[r]++; + } else + cell->attributes.erase("\\equiv_region"); + } + + for (auto wire : module->wires()) + { + pool regions; + for (auto bit : sigmap(wire)) + if (bit_regions.count(bit)) + regions.insert(region_find(bit_regions.at(bit))); + + if (GetSize(regions) == 1) { + int r = final_region_map.at(*regions.begin()); + wire->attributes["\\equiv_region"] = Const(r); + region_wire_count[r]++; + } else + wire->attributes.erase("\\equiv_region"); + } + + for (int i = 0; i < next_final_region; i++) + log(" region %d: %d cells, %d wires\n", i, region_wire_count[i], region_cell_count[i]); + } +}; + +struct EquivMarkPass : public Pass { + EquivMarkPass() : Pass("equiv_mark", "mark equivalence checking regions") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" equiv_mark [options] [selection]\n"); + log("\n"); + log("This command marks the regions in an equivalence checking module. Region 0 is\n"); + log("the proven part of the circuit. Regions with higher numbers are connected\n"); + log("unproven subcricuits. The integer attribute 'equiv_region' is set on all\n"); + log("wires and cells.\n"); + log("\n"); + } + virtual void execute(std::vector args, Design *design) + { + log_header("Executing EQUIV_MARK 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()) { + EquivMarkWorker worker(module); + worker.run(); + } + } +} EquivMarkPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc index 286bd357..e14ffe31 100644 --- a/passes/equiv/equiv_purge.cc +++ b/passes/equiv/equiv_purge.cc @@ -87,7 +87,7 @@ struct EquivPurgeWorker void run() { - log("Running equiv_purge on module %s:", log_id(module)); + log("Running equiv_purge on module %s:\n", log_id(module)); for (auto wire : module->wires()) { wire->port_input = false; -- cgit v1.2.3