Merge pull request #3537 from jix/xprop

New xprop pass

3 files changed, 30 insertions, 13 deletions

diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index 962e350a1..e36379096 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -532,12 +532,14 @@ struct FormalFfPass : public Pass {
 						if ((int)bits.size() == ff.val_init.size()) {
 							// This check is only to make the private names more helpful for debugging
 							ff.is_anyinit = true;
+							ff.is_fine = false;
 							emit = true;
 							break;
 						}
 
 						auto slice = ff.slice(bits);
 						slice.is_anyinit = is_anyinit;
+						slice.is_fine = false;
 						slice.emit();
 					}
 				}
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");
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1cd1ebc71..e8dda4c45 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -509,7 +509,7 @@ struct SimInstance
 		}
 	}
 
-	bool update_ph2()
+	bool update_ph2(bool gclk)
 	{
 		bool did_something = false;
 
@@ -567,7 +567,8 @@ struct SimInstance
 			}
 			if (ff_data.has_gclk) {
 				// $ff
-				current_q = ff.past_d;
+				if (gclk)
+					current_q = ff.past_d;
 			}
 			if (set_state(ff_data.sig_q, current_q))
 				did_something = true;
@@ -616,7 +617,7 @@ struct SimInstance
 		}
 
 		for (auto it : children)
-			if (it.second->update_ph2()) {
+			if (it.second->update_ph2(gclk)) {
 				dirty_children.insert(it.second);
 				did_something = true;
 			}
@@ -985,7 +986,7 @@ struct SimWorker : SimShared
 			writer->write(use_signal);
 	}
 
-	void update()
+	void update(bool gclk)
 	{
 		while (1)
 		{
@@ -997,7 +998,7 @@ struct SimWorker : SimShared
 			if (debug)
 				log("\n-- ph2 --\n");
 
-			if (!top->update_ph2())
+			if (!top->update_ph2(gclk))
 				break;
 		}
 
@@ -1047,7 +1048,7 @@ struct SimWorker : SimShared
 		set_inports(clock, State::Sx);
 		set_inports(clockn, State::Sx);
 
-		update();
+		update(false);
 
 		register_output_step(0);
 
@@ -1060,7 +1061,7 @@ struct SimWorker : SimShared
 			set_inports(clock, State::S0);
 			set_inports(clockn, State::S1);
 
-			update();
+			update(true);
 			register_output_step(10*cycle + 5);
 
 			if (debug)
@@ -1076,7 +1077,7 @@ struct SimWorker : SimShared
 				set_inports(resetn, State::S1);
 			}
 
-			update();
+			update(true);
 			register_output_step(10*cycle + 10);
 		}
 
@@ -1193,7 +1194,7 @@ struct SimWorker : SimShared
 					initial = false;
 				}
 				if (did_something)
-					update();
+					update(true);
 				register_output_step(time);
 
 				bool status = top->checkSignals();
@@ -1342,12 +1343,12 @@ struct SimWorker : SimShared
 						set_inports(clock, State::S0);
 						set_inports(clockn, State::S1);
 					}
-					update();
+					update(true);
 					register_output_step(10*cycle);
 					if (!multiclock && cycle) {
 						set_inports(clock, State::S0);
 						set_inports(clockn, State::S1);
-						update();
+						update(true);
 						register_output_step(10*cycle + 5);
 					}
 					cycle++;
@@ -1419,12 +1420,12 @@ struct SimWorker : SimShared
 						log("Simulating cycle %d.\n", cycle);
 					set_inports(clock, State::S1);
 					set_inports(clockn, State::S0);
-					update();
+					update(true);
 					register_output_step(10*cycle+0);
 					if (!multiclock) {
 						set_inports(clock, State::S0);
 						set_inports(clockn, State::S1);
-						update();
+						update(true);
 						register_output_step(10*cycle+5);
 					}
 					cycle++;