--- /dev/null
+/*
+ * 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 EquivMarkWorker
+{
+ Module *module;
+ SigMap sigmap;
+
+ // cache for traversing signal flow graph
+ dict<SigBit, pool<IdString>> up_bit2cells;
+ dict<IdString, pool<SigBit>> up_cell2bits;
+ pool<IdString> edge_cells, equiv_cells;
+
+ // graph traversal state
+ pool<SigBit> queue, visited;
+
+ // assigned regions
+ dict<IdString, int> cell_regions;
+ dict<SigBit, int> bit_regions;
+ int next_region;
+
+ // merge-find
+ dict<int, int> region_mf;
+
+ int region_find(int r)
+ {
+ vector<int> 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<IdString> 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<int, int> final_region_map;
+ int next_final_region = 0;
+
+ dict<int, int> region_cell_count;
+ dict<int, int> 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<int> 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<std::string> 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
projects / yosys.git / commitdiff