XBDD cuts memory use in Boolean function maps with new edge tricks
XBDD: A Highly Optimized ROBDD with Per-Edge Variable-Flip Maps
Data Structures and Algorithms
Summary
Representing complex yes/no questions about circuits often requires big diagrams that use a lot of memory. The authors found a way to shrink these diagrams by allowing edges to 'flip' input variables as you follow them, so that parts that differ only by these flips can share the same node. This reduces the size of the diagrams, sometimes by a huge amount. They also developed methods to keep the extra information about which variables to flip in a memory-efficient way and made other improvements to keep things fast. Their experiments show that this approach trades some extra time for much less memory use.
What this means in practice
- •For hardware verification teams: Shrinks memory use in Boolean function checks, enabling larger circuit equivalence tests.
- •For formal verification engineers: Optimizes satisfiability checking tools by reducing diagram sizes without major speed loss.
Authors
Yinglong Gan, Jintao Yu, Shenggang Ying, Yusen Li, Xin Hong
Abstract
The Reduced Ordered Binary Decision Diagram (ROBDD) is a canonical representation of Boolean functions and is widely used in tasks such as equivalence checking and satisfiability checking of combinational circuits. Classical ROBDD packages greatly improve the efficiency of building ROBDDs through a series of optimization techniques, and compress the node scale of the ROBDD through complement edges. However, existing implementations do not take into account the local polarity differences of isomorphic Boolean functions, and still produce a distinct node for each polarity combination, thereby causing an explosion in the number of nodes. This paper proposes XBDD, a highly optimized ROBDD that, on the basis of fully implementing complement edges and their accompanying engineering techniques, introduces a per-edge variable-flip map. XBDD attaches a flip map to each edge to indicate which input variables must be negated when that edge is followed. This allows nodes that differ only in local input polarities to be merged, further reducing the node count. For certain function families, this sharing even yields exponential compression. We also propose methods that use a bitmap and a map pool to substantially reduce the extra overhead brought by the map, and propose normalization and cofactor operators for the map. In addition, XBDD implements several other engineering optimizations to further improve both time and space efficiency. Experiments show that XBDD trades a controllable time cost for a significant space gain, validating the effectiveness of the per-edge variable-flip map.