Implicit Permutation Enumeration Networks and Binary Decision Diagrams Reordering

摘要

Ordered Binary Decision Diagrams are a canonical representation of Boolean functions that is at the core of most formal verification systems and silicon compilers. Canonicity enables efficiency of manipulation but comes at the cost of fixing a variable evaluation order and predictably, BDD sizes are very sensitive to the selected order. The state-of-the-art reordering algorithms are based on transpositions of consecutive variables (swaps). Exact algorithms enumerate all possible n! permutations by performing a series of at least n! − 1 swaps, while heuristics typically either search for the optimum location of each variable independently (sifting) or utilize exact algorithms as a subroutine (k-window.) In this work we reduce the problem of variable ordering to that of obtaining a permutation enumeration transposition network. Our proposed network avoids traversing all n! permutations by exploiting structural properties of BDDs and requires the execution of fewer than 4ⁿ swaps sequentially instead of n! − 1. For the practically interesting cases of n = 4; 5 our algorithm requires only 11 (resp 59) sequential swaps instead of 23 (resp 119). We also propose an algorithm for moving between arbitrary variable orderings that executes at most n swaps sequentially, an improvement upon equation. Results suggest speedups of 162%; 308%;> 10X over the k - window heuristic for k = 4; 6; 8 and near-linear speedups when moving between orderings.