3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-23 06:13:41 +00:00

opt_balance_tree pass formal equiv

This commit is contained in:
Alain Dargelas 2025-01-14 09:35:43 -08:00
parent 57bf3a6f51
commit 14cfd027b7

View file

@ -46,7 +46,9 @@ struct OptBalanceTreeWorker {
pool<Cell *> chain_start_cells; pool<Cell *> chain_start_cells;
pool<Cell *> candidate_cells; pool<Cell *> candidate_cells;
void make_sig_chain_next_prev(IdString cell_type) // Ignore signals fanout while looking ahead which chains to split.
// Post splitfanout, take that into account.
void make_sig_chain_next_prev(IdString cell_type, bool ignore_split)
{ {
// Mark all wires with keep attribute as having non-chain users // Mark all wires with keep attribute as having non-chain users
for (auto wire : module->wires()) { for (auto wire : module->wires()) {
@ -66,11 +68,12 @@ struct OptBalanceTreeWorker {
SigSpec y_sig = sigmap(cell->getPort(ID::Y)); SigSpec y_sig = sigmap(cell->getPort(ID::Y));
// If a_sig already has a chain user, mark its bits as having non-chain users // If a_sig already has a chain user, mark its bits as having non-chain users
if (sig_chain_next.count(a_sig)) if (sig_chain_next.count(a_sig)) {
for (auto a_bit : a_sig.bits()) if (!ignore_split)
sigbit_with_non_chain_users.insert(a_bit); for (auto a_bit : a_sig.bits())
// Otherwise, mark cell as the next in the chain relative to a_sig sigbit_with_non_chain_users.insert(a_bit);
else { // Otherwise, mark cell as the next in the chain relative to a_sig
} else {
if (fanout_in_range(y_sig)) { if (fanout_in_range(y_sig)) {
sig_chain_next[a_sig] = cell; sig_chain_next[a_sig] = cell;
} }
@ -78,11 +81,12 @@ struct OptBalanceTreeWorker {
if (!b_sig.empty()) { if (!b_sig.empty()) {
// If b_sig already has a chain user, mark its bits as having non-chain users // If b_sig already has a chain user, mark its bits as having non-chain users
if (sig_chain_next.count(b_sig)) if (sig_chain_next.count(b_sig)) {
for (auto b_bit : b_sig.bits()) if (!ignore_split)
sigbit_with_non_chain_users.insert(b_bit); for (auto b_bit : b_sig.bits())
// Otherwise, mark cell as the next in the chain relative to b_sig sigbit_with_non_chain_users.insert(b_bit);
else { // Otherwise, mark cell as the next in the chain relative to b_sig
} else {
if (fanout_in_range(y_sig)) { if (fanout_in_range(y_sig)) {
sig_chain_next[b_sig] = cell; sig_chain_next[b_sig] = cell;
} }
@ -214,11 +218,11 @@ struct OptBalanceTreeWorker {
cell->fixup_parameters(); cell->fixup_parameters();
} }
void process_chain(vector<Cell *> &chain) bool process_chain(vector<Cell *> &chain)
{ {
// If chain size is less than 3, no balancing needed // If chain size is less than 3, no balancing needed
if (GetSize(chain) < 3) if (GetSize(chain) < 3)
return; return false;
// Get mid, midnext (at index mid+1) and end of chain // Get mid, midnext (at index mid+1) and end of chain
Cell *mid_cell = chain[GetSize(chain) / 2]; Cell *mid_cell = chain[GetSize(chain) / 2];
@ -275,6 +279,7 @@ struct OptBalanceTreeWorker {
// Width reduce mid cell // Width reduce mid cell
wreduce(mid_cell); wreduce(mid_cell);
return true;
} }
void cleanup() void cleanup()
@ -364,7 +369,7 @@ struct OptBalanceTreeWorker {
bool has_cell_to_split = false; bool has_cell_to_split = false;
for (auto cell_type : cell_types) { for (auto cell_type : cell_types) {
// Find chains of ops // Find chains of ops
make_sig_chain_next_prev(cell_type); make_sig_chain_next_prev(cell_type, true);
find_chain_start_cells(); find_chain_start_cells();
// For each chain, if len >= 3, select all the elements // For each chain, if len >= 3, select all the elements
@ -393,13 +398,19 @@ struct OptBalanceTreeWorker {
// Do for each cell type // Do for each cell type
for (auto cell_type : cell_types) { for (auto cell_type : cell_types) {
// Find chains of ops // Find chains of ops
make_sig_chain_next_prev(cell_type); make_sig_chain_next_prev(cell_type, false);
find_chain_start_cells(); find_chain_start_cells();
// For each chain, if len >= 3, convert to tree via "rotation" and recurse on subtrees // For each chain, if len >= 3, convert to tree via "rotation" and recurse on subtrees
for (auto c : chain_start_cells) { for (auto c : chain_start_cells) {
vector<Cell *> chain = create_chain(c); vector<Cell *> chain = create_chain(c);
process_chain(chain); if (process_chain(chain)) {
// Rename cells for formal check to pass as cells signals have changed functionalities post rotation
for (Cell *cell : chain) {
module->rename(cell, NEW_ID2_SUFFIX("mid_cell"));
log("Renaming cell %s \n", cell->name.c_str());
}
}
cell_count[cell_type] += GetSize(chain); cell_count[cell_type] += GetSize(chain);
} }