Demo Data from VLDB 2026 / reviewers in the wild / expert
Qihao Hu
dblp:325/9690
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2025
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Computer architecture, parallel and distributed computing, and storage systems
1 paper |
Electronic design automation · 100% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Electronic design automation › logic synthesis
boolean reasoning |
0.9 | 1 | 2025 | BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation · DAC 2025 |
Electronic design automation › hardware verification and test
formal verification |
0.9 | 1 | 2025 | BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation · DAC 2025 |
Electronic design automation › hardware verification and test
hardware verification |
0.9 | 1 | 2025 | BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation · DAC 2025 |
Electronic design automation
logic synthesis |
0.9 | 1 | 2025 | BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation · DAC 2025 |
Methods — techniques the papers use, named apart from their topics
term rewriting · 0.9e-graph extraction · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | BoolE: Exact Symbolic Reasoning via Boolean Equality SaturationabstractBoolean 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. Zhan Song, Qihao Hu, Cunxi Yu |
DAC | 4 |