Event
Ph.D. Dissertation Defense: Jiaqi Yin
Thursday, January 15, 2026
8:30 a.m.
AVW 1146 (ISR)
Sarah Pham
301 473 2449
spham124@umd.edu
NAME: Jiaqi Yin
Committee:
Prof. Cunxi Yu (Chair/Advisor)
Prof. Alan Sussman (Dean's Representative)
Prof. Shuvra S. Bhattacharyya
Prof. Ang Li
Prof. Gang Qu
Date/time: Thursday, January 15, 2026 at 8:30am – 11:00am
Location: AVW 1146 (ISR)
Title: Equality Saturation: A Unified Formal Paradigm for Multi-Level Hardware Systems
Abstract:
Modern hardware design faces a fundamental challenge: achieving both functional correctness and optimal performance across increasingly complex architectures. Traditional optimization pipelines rely on phase-ordered transformations that commit to specific implementations early, leading to brittleness where solution quality depends arbitrarily on transformation sequences. This dissertation develops equality saturation—a non-destructive optimization paradigm that maintains multiple equivalent representations simultaneously—into a unified formal methodology addressing verification and optimization challenges across multiple hardware abstraction layers. The work makes three primary contributions: (1) BoolE, a gate-level framework for exact Boolean symbolic reasoning that reconstructs arithmetic structures from optimized netlists, achieving over four orders of magnitude speedup in multiplier verification; (2) HEC, an MLIR-based equivalence checker that validates complex compiler transformations through hybrid static-dynamic rewriting, discovering critical bugs in standard benchmarks; and (3) scalable solving frameworks (e-boost and Inc-ILP) that bridge the scalability-optimality trade-off by synergistically combining adaptive heuristics with exact solvers, achieving 558× runtime speedup while maintaining provably optimal results.
Together, these contributions establish equality saturation as an end-to-end methodology for hardware design automation, demonstrating that the longstanding dichotomy between scalability and optimality in Electronic Design Automation can be resolved through intelligent integration of symbolic reasoning, formal methods, and learning-guided optimization. By deferring commitment to specific implementations until extraction and providing formal correctness guarantees throughout, this paradigm advances the state of the art in hardware verification, synthesis, and optimization across gate, program, and solver abstraction levels.
