BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
X-LIC-LOCATION:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260402T024534Z
LOCATION:3006\, Level 3
DTSTART;TZID=America/Los_Angeles:20250624T153000
DTEND;TZID=America/Los_Angeles:20250624T154500
UID:dac_DAC 2025_sess138_RESEARCH1958@linklings.com
SUMMARY:BoolE: Exact Symbolic Reasoning via Boolean Equality Saturation*
DESCRIPTION:Jiaqi Yin, Zhan Song, Chen Chen, Qihao Hu, and Cunxi Yu (Unive
 rsity of Maryland, College Park)\n\nBoolean symbolic reasoning for gate-le
 vel netlists is a critical step in fields such as verification, logic and 
 datapath synthesis, and hardware security. Specifically, reasoning datapat
 h and carry-chain in bit-blasted Boolean networks is particularly crucial 
 for verification and synthesis, and challenging. Conventional approaches e
 ither failed to accurately (exactly) identify the carry-chain of the desig
 ns 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 equalit
 y saturation (e-graph). BoolE optimizes scalability and performance by dom
 ain-specific ruleset pruning in e-graph rewriting, and incorporates a nove
 l extraction algorithm to efficiently identify and capture multi-input mul
 ti-output high-level structures (e.g., full adder) in the constructed e-gr
 aph, enhancing its structural insight and computational efficiency.\n\nOur
  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 performanc
 e on various multiplier architecture with different configurations. Our re
 sults show that BoolE identifies 3.53x and 3.01x more exact full adders th
 an ABC in carry-save array (CSA) and Booth-encoded multipliers, respective
 ly. Additionally, we integrated BoolE into multiplier formal verification 
 tasks, where it significantly accelerates the performance of traditional f
 ormal verification tools using computer algebra.\n\nTopics: EDA\n\nTracks:
  EDA5: RTL/Logic Level and High-level Synthesis\n\nSession Chairs: Giovann
 i De Micheli (École Polytechnique Fédérale de Lausanne) and Eleonora Testa
  (Synopsys)\n\n
END:VEVENT
END:VCALENDAR