Improvements in assertpmux

1 files changed, 158 insertions, 21 deletions

diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc
index 3c8928db5..63a907671 100644
--- a/passes/sat/assertpmux.cc
+++ b/passes/sat/assertpmux.cc
@@ -18,40 +18,166 @@
  */
 
 #include "kernel/yosys.h"
+#include "kernel/sigtools.h"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-void assertpmux_worker(Cell *pmux, bool flag_noinit)
+struct AssertpmuxWorker
 {
-	Module *module = pmux->module;
+	Module *module;
+	SigMap sigmap;
 
-	log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux));
+	bool flag_noinit;
+	bool flag_always;
 
-	int swidth = pmux->getParam("\\S_WIDTH").as_int();
-	int cntbits = ceil_log2(swidth+1);
+	// get<0> ... mux cell
+	// get<1> ... mux port index
+	// get<2> ... mux bit index
+	dict<SigBit, pool<tuple<Cell*, int, int>>> sigbit_muxusers;
 
-	SigSpec sel = pmux->getPort("\\S");
-	SigSpec cnt(State::S0, cntbits);
+	dict<SigBit, SigBit> sigbit_actsignals;
+	dict<SigSpec, SigBit> sigspec_actsignals;
+	dict<tuple<Cell*, int>, SigBit> muxport_actsignal;
 
-	for (int i = 0; i < swidth; i++)
-		cnt = module->Add(NEW_ID, cnt, sel[i]);
+	AssertpmuxWorker(Module *module, bool flag_noinit, bool flag_always) :
+			module(module), sigmap(module), flag_noinit(flag_noinit), flag_always(flag_always)
+	{
+		for (auto wire : module->wires())
+		{
+			if (wire->port_output)
+				for (auto bit : sigmap(wire))
+					sigbit_actsignals[bit] = State::S1;
+		}
+
+		for (auto cell : module->cells())
+		{
+			if (cell->type.in("$mux", "$pmux"))
+			{
+				int width = cell->getParam("\\WIDTH").as_int();
+				int numports = cell->type == "$mux" ? 2 : cell->getParam("\\S_WIDTH").as_int() + 1;
+
+				SigSpec sig_a = sigmap(cell->getPort("\\A"));
+				SigSpec sig_b = sigmap(cell->getPort("\\B"));
+				SigSpec sig_s = sigmap(cell->getPort("\\S"));
+
+				for (int i = 0; i < numports; i++) {
+					SigSpec bits = i == 0 ? sig_a : sig_b.extract(width*(i-1), width);
+					for (int k = 0; k < width; k++) {
+						tuple<Cell*, int, int> muxuser(cell, i, k);
+						sigbit_muxusers[bits[k]].insert(muxuser);
+					}
+				}
+			}
+			else
+			{
+				for (auto &conn : cell->connections()) {
+					if (!cell->known() || cell->input(conn.first))
+						for (auto bit : sigmap(conn.second))
+							sigbit_actsignals[bit] = State::S1;
+				}
+			}
+		}
+	}
+
+	SigBit get_bit_activation(SigBit bit)
+	{
+		sigmap.apply(bit);
+
+		if (sigbit_actsignals.count(bit) == 0)
+		{
+			SigSpec output;
+
+			for (auto muxuser : sigbit_muxusers.at(bit))
+			{
+				Cell *cell = std::get<0>(muxuser);
+				int portidx = std::get<1>(muxuser);
+				int bitidx = std::get<2>(muxuser);
+
+				tuple<Cell*, int> muxport(cell, portidx);
+
+				if (muxport_actsignal.count(muxport) == 0) {
+					if (portidx == 0)
+						muxport_actsignal[muxport] = module->LogicNot(NEW_ID, cell->getPort("\\S"));
+					else
+						muxport_actsignal[muxport] = cell->getPort("\\S")[portidx-1];
+				}
+
+				output.append(module->LogicAnd(NEW_ID, muxport_actsignal.at(muxport), get_bit_activation(cell->getPort("\\Y")[bitidx])));
+			}
+
+			output.sort_and_unify();
+
+			if (GetSize(output) == 0)
+				output = State::S0;
+			else if (GetSize(output) > 1)
+				output = module->ReduceOr(NEW_ID, output);
+
+			sigbit_actsignals[bit] = output.as_bit();
+		}
+
+		return sigbit_actsignals.at(bit);
+	}
+
+	SigBit get_activation(SigSpec sig)
+	{
+		sigmap.apply(sig);
+		sig.sort_and_unify();
+
+		if (sigspec_actsignals.count(sig) == 0)
+		{
+			SigSpec output;
+
+			for (auto bit : sig)
+				output.append(get_bit_activation(bit));
 
-	SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits));
-	SigSpec assert_en = State::S1;
+			output.sort_and_unify();
 
-	if (flag_noinit) {
-		Cell *initstate_cell = module->addCell(NEW_ID, "$initstate");
-		SigSpec initstate_sig = module->addWire(NEW_ID);
-		initstate_cell->setPort("\\Y", initstate_sig);
-		assert_en = module->LogicNot(NEW_ID, initstate_sig);
+			if (GetSize(output) == 0)
+				output = State::S0;
+			else if (GetSize(output) > 1)
+				output = module->ReduceOr(NEW_ID, output);
+
+			sigspec_actsignals[sig] = output.as_bit();
+		}
+
+		return sigspec_actsignals.at(sig);
 	}
 
-	Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en);
+	void run(Cell *pmux)
+	{
+		log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux));
+
+		int swidth = pmux->getParam("\\S_WIDTH").as_int();
+		int cntbits = ceil_log2(swidth+1);
+
+		SigSpec sel = pmux->getPort("\\S");
+		SigSpec cnt(State::S0, cntbits);
 
-	if (pmux->attributes.count("\\src") != 0)
-		assert_cell->attributes["\\src"] = pmux->attributes.at("\\src");
-}
+		for (int i = 0; i < swidth; i++)
+			cnt = module->Add(NEW_ID, cnt, sel[i]);
+
+		SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits));
+		SigSpec assert_en;
+
+		if (flag_noinit)
+			assert_en.append(module->LogicNot(NEW_ID, module->Initstate(NEW_ID)));
+
+		if (!flag_always)
+			assert_en.append(get_activation(pmux->getPort("\\Y")));
+
+		if (GetSize(assert_en) == 0)
+			assert_en = State::S1;
+
+		if (GetSize(assert_en) == 2)
+			assert_en = module->LogicAnd(NEW_ID, assert_en[0], assert_en[1]);
+
+		Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en);
+
+		if (pmux->attributes.count("\\src") != 0)
+			assert_cell->attributes["\\src"] = pmux->attributes.at("\\src");
+	}
+};
 
 struct AssertpmuxPass : public Pass {
 	AssertpmuxPass() : Pass("assertpmux", "convert internal signals to module ports") { }
@@ -67,10 +193,16 @@ struct AssertpmuxPass : public Pass {
 		log("    -noinit\n");
 		log("        do not enforce the pmux condition during the init state\n");
 		log("\n");
+		log("    -always\n");
+		log("        usually the $pmux condition is only checked when the $pmux output\n");
+		log("        is used be the mux tree it drives. this option will deactivate this\n");
+		log("        additional constrained and check the $pmux condition always.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
 		bool flag_noinit = false;
+		bool flag_always = false;
 
 		log_header(design, "Executing ASSERTPMUX pass (add asserts for $pmux cells).\n");
 
@@ -81,12 +213,17 @@ struct AssertpmuxPass : public Pass {
 				flag_noinit = true;
 				continue;
 			}
+			if (args[argidx] == "-always") {
+				flag_always = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
 		for (auto module : design->selected_modules())
 		{
+			AssertpmuxWorker worker(module, flag_noinit, flag_always);
 			vector<Cell*> pmux_cells;
 
 			for (auto cell : module->selected_cells())
@@ -94,7 +231,7 @@ struct AssertpmuxPass : public Pass {
 					pmux_cells.push_back(cell);
 
 			for (auto cell : pmux_cells)
-				assertpmux_worker(cell, flag_noinit);
+				worker.run(cell);
 		}
 
 	}