Added equiv_purge

2 files changed, 210 insertions, 0 deletions

diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc
index d5bb9495..4d615742 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 00000000..286bd357
--- /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