BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation

TL;DR

This work tackles the challenge of exact symbolic reasoning on gate-level Boolean netlists under heavy optimization and technology mapping. It presents BoolE, an exact reasoning framework based on Boolean equality saturation over e-graphs, augmented with a novel extraction algorithm to identify multi-input, multi-output blocks like full adders. By combining a large, domain-specific rewriting ruleset with incremental saturation and a DAG-based extraction, BoolE produces exact FA structures and an AIG output, and it integrates with ABC and RevSCA-2.0 for practical verification tasks. Empirical results show BoolE outperforms state-of-the-art baselines in exact FA recovery and yields orders-of-magnitude speedups in formal verification for large multipliers, highlighting its potential impact on synthesis, verification, and hardware security tooling.

Abstract

Boolean symbolic reasoning for gate-level netlists is a critical step in verification, logic and datapath synthesis, and hardware security. Specifically, reasoning datapath and adder tree in bit-blasted Boolean networks is particularly crucial for verification and synthesis, and challenging. Conventional approaches either fail to accurately (exactly) identify the function blocks of the designs in gate-level netlist with structural hashing and symbolic propagation, or their reasoning performance is highly sensitive to structure modifications caused by technology mapping or logic optimization. This paper introduces BoolE, an exact symbolic reasoning framework for Boolean netlists using equality saturation. BoolE optimizes scalability and performance by integrating domain-specific Boolean ruleset for term rewriting. We incorporate a novel extraction algorithm into BoolE to enhance its structural insight and computational efficiency, which adeptly identifies and captures multi-input, multi-output high-level structures (e.g., full adder) in the reconstructed e-graph. Our experiments show that BoolE surpasses state-of-the-art symbolic reasoning baselines, including the conventional 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.53\times$ and $3.01\times$ more exact full adders than ABC in carry-save array 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, demonstrated over four orders of magnitude runtime improvements.

Figures (5)

• Figure 1: Motivations for BoolE. The component blocks of exact FA, NPN FA, and HA are shown in blue, green, and grey blocks. The output signals of corresponding XOR and MAJ are marked as green and red correspondingly. (a) AIG of a 3-bit CSA multiplier generated by ABC and mapped using 7nm ASAP Technology Mapping. (b) FA and HA blocks in AIG detected by ABC. (c) Adder tree extracted from AIG. There is only one NPN FA. (d) The output netlist extracted after BoolE rewriting. An additional exact FA is reconstructed after BoolE rewriting.
• Figure 2: The overview of BoolE, an exact symbolic reasoning framework for Boolean netlists utilizing equality saturation. It enhances performance by employing a novel extraction algorithm specifically designed to identify and capture multi-input, multi-output exact FA structure. We incorporate part of the e-graph for motivating example shown in Figure \ref{['fig:motivations']} to illustrate how the additional extra FA is extracted from e-graph, where the extracted e-nodes are specially highlighted. The XOR and MAJ gates forming an exact FA are highlighted in green.
• Figure 3: FA Structure: XOR and MAJ e-nodes with the exactly same inputs will be paired. Each paired XOR/MAJ operation will insert a FA nodes and utilize FST/SND to project out the carry/sum bits. FST/SND will unified to the e-classes of XOR/MAJ
• Figure 4: Performance comparison among BoolE, ABC, and Gamora for CSA (left) and Booth (right) multipliers after ASAP 7nm technology mapping. BoolE consistently outperforms ABC and Gamora, identifying $3.53\times$ and $3.01\times$ exact FAs than ABC in CSA and Booth multipliers. And BoolE achieves an average of $93.48\%$ and $84.81\%$ of the theoretical upper bound in number of NPN FAs, respectively.
• Figure 5: BoolE runtime of post-mapping CSA and Booth multiplier w.r.t. the size of the input netlist (AIG node number).