miter: Add -make_cover option to cover each output pair difference

1 files changed, 14 insertions, 0 deletions

diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index bf33c9ce3..1f64c0216 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -30,6 +30,7 @@ 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;
 
@@ -54,6 +55,10 @@ 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;
@@ -237,6 +242,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);
 		}
 	}
@@ -402,6 +413,9 @@ 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");