Added equiv_mark command

3 files changed, 265 insertions, 1 deletions

diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc
index 4d6157429..dd7b3be02 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 000000000..da61678df
--- /dev/null
+++ b/passes/equiv/equiv_mark.cc
@@ -0,0 +1,263 @@
+/*
+ *  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
diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc
index 286bd3573..e14ffe31c 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;