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

diff --git a/passes/sat/share.cc b/passes/sat/share.cc
index 065b90d3e457c116f2ef90c5e7de490c43b6c514..5f3cf421484dec6811f733225e92c070c17fdf33 100644 (file)
--- 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;