Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2504.05577

BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation

Jiaqi Yin·Zhan Song·Chen Chen·Qihao Hu·Cunxi Yu
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.AR

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jiaqi Yin, Zhan Song, Chen Chen, Qihao Hu, Cunxi Yu. 2025-04-20. BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation. https://arxiv.org/abs/2504.05577

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A System Architecture for Low Latency Multiprogramming Quantum Computing

As quantum systems scale, multiprogramming quantum computing (MPQC) provides a practical way to improve device utilization and throughput. However, because quantum executables are device-dependent, non-portable across qubit regions, and highly susceptible to noise and crosstalk, current MPQC pipelines rely on expensive online compilation to co-optimize concurrently running programs. This online step dominates runtime and impedes low-latency deployments for practical, real-world workloads in the future, such as repeatedly invoked quantum neural network (QNN) services. We present FLAMENCO, a fidelity-aware multi-version compilation system that enables independent offline compilation and low-latency multiprogramming at runtime. \textbf{At the architecture level}, the system abstracts devices into compute units to reduce the search space of region allocation. \textbf{At compile time}, it generates diverse executable versions for each program---each bound to a distinct qubit region---allowing dynamic region selection at runtime and overcoming non-portability. \textbf{At runtime}, it employs a lightweight orchestrator that uses post-compilation fidelity metrics to avoid conflicts and mitigate crosstalk, supporting conflict-free co-execution without online co-optimization. Evaluations show that FLAMENCO achieves over 5$\times$ runtime speedup in post-scheduling execution while maintaining comparable execution fidelity on common-success workloads. When integrated into existing scheduler-coupled systems, it raises workload-level conflict-free orchestration ratio from 0.183 to 1.000 for HyperQ and from 0.050 to 0.400 for QOS.

cs.AR↗
arXiv2026

HBFSim: Fast and Faithful Simulation of High-Bandwidth Flash Under Real GPU Execution

High-Bandwidth Flash (HBF) places high-capacity NAND beside HBM to relieve the memory-capacity bottleneck of LLM inference, yet its system-level behavior cannot be evaluated before hardware becomes available. Cycle-level GPU simulators are too slow for production-scale models. Trace replay has a further shortcoming: it cannot capture the allocation, migration, and execution changes induced by different HBM-HBF configurations. Our key insight is that HBF need not be evaluated by simulating the GPU: only the program-visible effects of HBF need to be modeled. And only a real LLM workload running on real hardware can answer the arguments about HBF. Hence the modeled service has to be injected into that running program, and the injection must not destroy the GPU concurrency that would hide the original I/O latency. We present HBFSim, an open-source HBF simulator that executes LLM workloads on a real GPU while modeling HBF timing, thermal, and other behaviors online. HBFSim rewrites the PTX of the workload's kernels and routes accesses inside a registered address range into the HBF simulator. It supports asynchronous TMA transfers and capacities beyond physical GPU memory. HBFSim leaves the model's run unaffected across ordinary-memory, TMA, and capacity-mode tests. The delay it injects matches the delay requested to within 0.152%. We also design a coupled thermal module that puts HBF, HBM, and the GPU in one advanced package, which is important for answering how severe the hot throttling problem becomes after HBF runs for a long time. Experiments with Qwen3-30B show how package heating, HBM-HBF allocation, and shared MoE demand jointly constrain the design space of future HBF accelerators.

cs.AR↗
arXiv2026

Bio-inspired Learning and Decision-Making with Probabilistic In-Memory Computing Hardware: Part 2

This report extends our previous work (Part 1), which introduced an energy-based model for learning and decision-making under uncertainty. The model leverages stochastic Langevin dynamics to continuously evolve approximate probability distributions over neuron states and model weights. However, as noted in Part 1 and confirmed through GPU-based implementations, large-scale probabilistic energy-based models of this nature face significant scalability challenges due to excessive execution latency. This latency stems from a fundamental mismatch: massively parallel models with low arithmetic intensity (such as energy-based models) are being executed on processor architectures like GPUs that rely on high-bandwidth memory (HBM) interfaces. The HBM imposes brutally sequential execution constraints on inherently parallelizable models, creating the false impression that such models are unscalable. In reality, it is the GPU architecture itself, with its dependence on HBM interfaces, that is not a scalable processor architecture for this class of AI model. In this report, we demonstrate using a detailed transaction-level model (TLM) of a probabilistic analogue in-memory computing (AIMC) processor that the same energy-based model can execute well over 1000x faster than data-center-grade hardware by eliminating the HBM interface and performing computation directly within on-chip memory.

cs.AR↗