From 9d4362990f514ffd2aad3170ec7382f21b8bca67 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 9 Aug 2014 17:07:20 +0200 Subject: [PATCH] Fixed "share" for complex scenarios with never-active cells --- passes/sat/share.cc | 28 ++++++++++++++++++++++------ 1 file 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())) { - 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())) { - 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 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 sat_model = satgen.importSigSpec(all_ctrl_signals); std::vector sat_model_values; -- 2.30.2