Presentation
BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation*
DescriptionBoolean symbolic reasoning for gate-level netlists is a critical step in fields such as verification, logic and datapath synthesis, and hardware security. Specifically, reasoning datapath and carry-chain in bit-blasted Boolean networks is particularly crucial for verification and synthesis, and challenging. Conventional approaches either failed to accurately (exactly) identify the carry-chain of the designs in gate-level netlist with structural hashing, or failed due to runtime complexity with functional or formal methods. This paper introduces BoolE, an exact symbolic reasoning framework for Boolean netlists using equality saturation (e-graph). BoolE optimizes scalability and performance by domain-specific ruleset pruning in e-graph rewriting, and incorporates a novel extraction algorithm to efficiently identify and capture multi-input multi-output high-level structures (e.g., full adder) in the constructed e-graph, enhancing its structural insight and computational efficiency.
Our experiments show that BoolE surpasses state-of-the-art symbolic reasoning baselines, including the structural/functional approach (ABC) and machine learning-based method (Gamora). Specifically, we evaluated its performance on various multiplier architecture with different configurations. Our results show that BoolE identifies 3.53x and 3.01x more exact full adders than ABC in carry-save array (CSA) and Booth-encoded multipliers, respectively. Additionally, we integrated BoolE into multiplier formal verification tasks, where it significantly accelerates the performance of traditional formal verification tools using computer algebra.
Our experiments show that BoolE surpasses state-of-the-art symbolic reasoning baselines, including the structural/functional approach (ABC) and machine learning-based method (Gamora). Specifically, we evaluated its performance on various multiplier architecture with different configurations. Our results show that BoolE identifies 3.53x and 3.01x more exact full adders than ABC in carry-save array (CSA) and Booth-encoded multipliers, respectively. Additionally, we integrated BoolE into multiplier formal verification tasks, where it significantly accelerates the performance of traditional formal verification tools using computer algebra.
Event Type
Research Manuscript
TimeTuesday, June 243:30pm - 3:45pm PDT
Location3006, Level 3
EDA
EDA5: RTL/Logic Level and High-level Synthesis