1 files changed, 54 insertions, 4 deletions

diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 37efadfbd..8f27c4c6f 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -30,7 +30,9 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 	bool flag_make_outputs = false;
 	bool flag_make_outcmp = false;
 	bool flag_make_assert = false;
+	bool flag_make_cover = false;
 	bool flag_flatten = false;
+	bool flag_cross = false;
 
 	log_header(design, "Executing MITER pass (creating miter circuit).\n");
 
@@ -53,10 +55,18 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 			flag_make_assert = true;
 			continue;
 		}
+		if (args[argidx] == "-make_cover") {
+			flag_make_cover = true;
+			continue;
+		}
 		if (args[argidx] == "-flatten") {
 			flag_flatten = true;
 			continue;
 		}
+		if (args[argidx] == "-cross") {
+			flag_cross = true;
+			continue;
+		}
 		break;
 	}
 	if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
@@ -75,6 +85,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 
 	RTLIL::Module *gold_module = design->module(gold_name);
 	RTLIL::Module *gate_module = design->module(gate_name);
+	pool<Wire*> gold_cross_ports;
 
 	for (auto gold_wire : gold_module->wires()) {
 		if (gold_wire->port_id == 0)
@@ -82,12 +93,17 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 		RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name);
 		if (gate_wire == nullptr)
 			goto match_gold_port_error;
+		if (gold_wire->width != gate_wire->width)
+			goto match_gold_port_error;
+		if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
+				gate_wire->port_input && !gate_wire->port_output) {
+			gold_cross_ports.insert(gold_wire);
+			continue;
+		}
 		if (gold_wire->port_input != gate_wire->port_input)
 			goto match_gold_port_error;
 		if (gold_wire->port_output != gate_wire->port_output)
 			goto match_gold_port_error;
-		if (gold_wire->width != gate_wire->width)
-			goto match_gold_port_error;
 		continue;
 	match_gold_port_error:
 		log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str());
@@ -99,12 +115,15 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 		RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name);
 		if (gold_wire == nullptr)
 			goto match_gate_port_error;
+		if (gate_wire->width != gold_wire->width)
+			goto match_gate_port_error;
+		if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
+				gate_wire->port_input && !gate_wire->port_output)
+			continue;
 		if (gate_wire->port_input != gold_wire->port_input)
 			goto match_gate_port_error;
 		if (gate_wire->port_output != gold_wire->port_output)
 			goto match_gate_port_error;
-		if (gate_wire->width != gold_wire->width)
-			goto match_gate_port_error;
 		continue;
 	match_gate_port_error:
 		log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str());
@@ -123,6 +142,22 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 
 	for (auto gold_wire : gold_module->wires())
 	{
+		if (gold_cross_ports.count(gold_wire))
+		{
+			SigSpec w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
+			gold_cell->setPort(gold_wire->name, w);
+			if (flag_ignore_gold_x) {
+				RTLIL::SigSpec w_x = miter_module->addWire(NEW_ID, GetSize(w));
+				for (int i = 0; i < GetSize(w); i++)
+					miter_module->addEqx(NEW_ID, w[i], State::Sx, w_x[i]);
+				RTLIL::SigSpec w_any = miter_module->And(NEW_ID, miter_module->Anyseq(NEW_ID, GetSize(w)), w_x);
+				RTLIL::SigSpec w_masked = miter_module->And(NEW_ID, w, miter_module->Not(NEW_ID, w_x));
+				w = miter_module->And(NEW_ID, w_any, w_masked);
+			}
+			gate_cell->setPort(gold_wire->name, w);
+			continue;
+		}
+
 		if (gold_wire->port_input)
 		{
 			RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
@@ -215,6 +250,12 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 				miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
 			}
 
+			if (flag_make_cover)
+			{
+				auto cover_condition = miter_module->Not(NEW_ID, this_condition);
+				miter_module->addCover("\\cover_" + RTLIL::unescape_id(gold_wire->name), cover_condition, State::S1);
+			}
+
 			all_conditions.append(this_condition);
 		}
 	}
@@ -380,10 +421,19 @@ struct MiterPass : public Pass {
 		log("    -make_assert\n");
 		log("        also create an 'assert' cell that checks if trigger is always low.\n");
 		log("\n");
+		log("    -make_cover\n");
+		log("        also create a 'cover' cell for each gold/gate output pair.\n");
+		log("\n");
 		log("    -flatten\n");
 		log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
 		log("\n");
 		log("\n");
+		log("    -cross\n");
+		log("        allow output ports on the gold module to match input ports on the\n");
+		log("        gate module. This is useful when the gold module contains additional\n");
+		log("        logic to drive some of the gate module inputs.\n");
+		log("\n");
+		log("\n");
 		log("    miter -assert [options] module [miter_name]\n");
 		log("\n");
 		log("Creates a miter circuit for property checking. All input ports are kept,\n");