Fixed "share" for complex scenarios with never-active cells

1 files changed, 22 insertions, 6 deletions

diff --git a/passes/sat/share.cc b/passes/sat/share.cc
index 065b90d3e..5f3cf4214 100644
--- a/passes/sat/share.cc
+++ b/passes/sat/share.cc
@@ -685,12 +685,13 @@ struct ShareWorker
 			RTLIL::SigSpec cell_activation_signals = bits_from_activation_patterns(cell_activation_patterns);
 
 			if (cell_activation_patterns.empty()) {
-				log ("    Cell is never active. Sharing is pointless, we simply remove it.\n");
+				log("    Cell is never active. Sharing is pointless, we simply remove it.\n");
+				cells_to_remove.insert(cell);
 				continue;
 			}
 
 			if (cell_activation_patterns.count(std::pair<RTLIL::SigSpec, RTLIL::Const>())) {
-				log ("    Cell is always active. Therefore no sharing is possible.\n");
+				log("    Cell is always active. Therefore no sharing is possible.\n");
 				continue;
 			}
 
@@ -717,13 +718,15 @@ struct ShareWorker
 				RTLIL::SigSpec other_cell_activation_signals = bits_from_activation_patterns(other_cell_activation_patterns);
 
 				if (other_cell_activation_patterns.empty()) {
-					log ("      Cell is never active. Sharing is pointless, we simply remove it.\n");
+					log("      Cell is never active. Sharing is pointless, we simply remove it.\n");
 					shareable_cells.erase(other_cell);
+					cells_to_remove.insert(other_cell);
 					continue;
 				}
 
 				if (other_cell_activation_patterns.count(std::pair<RTLIL::SigSpec, RTLIL::Const>())) {
-					log ("      Cell is always active. Therefore no sharing is possible.\n");
+					log("      Cell is always active. Therefore no sharing is possible.\n");
+					shareable_cells.erase(other_cell);
 					continue;
 				}
 
@@ -750,8 +753,6 @@ struct ShareWorker
 				optimize_activation_patterns(filtered_other_cell_activation_patterns);
 
 				ezDefaultSAT ez;
-				ez.non_incremental();
-
 				SatGen satgen(&ez, &modwalker.sigmap);
 
 				std::set<RTLIL::Cell*> sat_cells;
@@ -798,6 +799,21 @@ struct ShareWorker
 						break;
 				}
 
+				if (!ez.solve(ez.expression(ez.OpOr, cell_active))) {
+					log("      According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell));
+					cells_to_remove.insert(cell);
+					break;
+				}
+
+				if (!ez.solve(ez.expression(ez.OpOr, other_cell_active))) {
+					log("      According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell));
+					cells_to_remove.insert(other_cell);
+					shareable_cells.erase(other_cell);
+					continue;
+				}
+
+				ez.non_incremental();
+
 				all_ctrl_signals.sort_and_unify();
 				std::vector<int> sat_model = satgen.importSigSpec(all_ctrl_signals);
 				std::vector<bool> sat_model_values;