From: Bogdan Vukobratovic <bogdan.vukobratovic@gmail.com>
Date: Fri, 14 Jun 2019 09:35:45 +0000 (+0200)
Subject: Some cleanup, revert sat.cc
X-Git-Tag: working-ls180~1239^2~4^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=291b36afeb1075b7c6329d1e57594ed3e6b71581;p=yosys.git

Some cleanup, revert sat.cc
---

diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index c5db344e8..41bbdcd57 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -460,15 +460,19 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 	}
 
 	if (sat && has_init) {
-		std::vector<int> removed_sigbits;
+		bool removed_sigbits = false;
 
+		// Create netlist for the module if not already available
 		if (!netlists.count(mod)) {
 			netlists.emplace(mod, Netlist(mod));
 			comb_filters.emplace(mod, comb_cells_filt());
 		}
 
+		// Load netlist for the module from the pool
 		Netlist &net = netlists.at(mod);
 
+
+		// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
 		for (int position = 0; position < GetSize(sig_d); position += 1) {
 			RTLIL::SigBit q_sigbit = sig_q[position];
 			RTLIL::SigBit d_sigbit = sig_d[position];
@@ -480,6 +484,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 			ezSatPtr ez;
 			SatGen satgen(ez.get(), &net.sigmap);
 
+			// Create SAT instance only for the cells that influence the register bit combinatorially
 			for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) {
 				if (!satgen.importCell(cell))
 					log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name),
@@ -492,12 +497,10 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 			int q_sat_pi = satgen.importSigBit(q_sigbit);
 			int d_sat_pi = satgen.importSigBit(d_sigbit);
 
+			// Try to find out whether the register bit can change under some circumstances
 			bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
 
-			if (position == 14) {
-				counter_example_found = false;
-			}
-
+			// If the register bit cannot change, we can replace it with a constant
 			if (!counter_example_found) {
 
 				RTLIL::SigBit &driver_port = net.driver_port(q_sigbit);
@@ -511,11 +514,11 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 
 				mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val));
 
-				removed_sigbits.push_back(position);
+				removed_sigbits = true;
 			}
 		}
 
-		if (!removed_sigbits.empty()) {
+		if (removed_sigbits) {
 			return true;
 		}
 	}
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 4492fc2b7..cbba738f0 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1548,20 +1548,17 @@ struct SatPass : public Pass {
 			print_proof_failed();
 
 		tip_failed:
-			design->scratchpad_set_bool("sat.success", false);
 			if (verify) {
 				log("\n");
 				log_error("Called with -verify and proof did fail!\n");
 			}
 
-			if (0) {
+			if (0)
 		tip_success:
-			design->scratchpad_set_bool("sat.success", true);
 			if (falsify) {
 				log("\n");
 				log_error("Called with -falsify and proof did succeed!\n");
 			}
-			}
 		}
 		else
 		{
@@ -1631,7 +1628,6 @@ struct SatPass : public Pass {
 
 			if (sathelper.solve())
 			{
-				design->scratchpad_set_bool("sat.success", false);
 				if (max_undef) {
 					log("SAT model found. maximizing number of undefs.\n");
 					sathelper.maximize_undefs();
@@ -1671,7 +1667,6 @@ struct SatPass : public Pass {
 			}
 			else
 			{
-				design->scratchpad_set_bool("sat.success", true);
 				if (sathelper.gotTimeout)
 					goto timeout;
 				if (rerun_counter)