Neuro-Symbolic Reasoning for Verified Hardware-Software Co-Design

Modern accelerator design requires exploring an enormous space of hardware
configurations and software mappings—a combinatorial problem where exhaustive search is
intractable, yet correctness must be guaranteed. This project develops a **neuro-symbolic**
framework that unifies artificial intelligence, formal methods, and mathematical reasoning via
(stochastic) integer programming to enable **verified and robust hardware-software co-design**.

The work centers on three research thrusts:

1. **Program Synthesis for Hardware Specialization** — SMT-based and neural-guided synthesis
that automatically generates equivalent instruction sequences, control words for accelerator
datapaths, and microprogrammed expansions for rare-case instructions.
2. **E-Graph-Based Design Space Exploration** — equality saturation to represent and navigate
the combinatorial space of hardware-software configurations, enabling global optimization
across ISA selection, microarchitecture parameters, and software transformations.
3. **Formal Circuit Specialization** — k-induction and Property-Directed Reachability (PDR/IC3)
to discover redundancies and don't-cares from constrained usage patterns, automatically
transforming general-purpose hardware into optimized, application-specific circuits.

The framework is validated on hardware accelerator design, including Application-Specific
Instruction-Set Processors (ASIPs) and domain-specific accelerators; preliminary results on ASIP
generation show significant area and power savings over state-of-the-art approaches.

**Broader impact.** As data centers face severe power constraints on AI deployment, reducing
accelerator area and power addresses a critical bottleneck in U.S. computing infrastructure. All
tools, benchmarks, and synthesized designs will be released as open-source infrastructure,
strengthening open alternatives to commercial EDA tools and lowering barriers to domestic chip
development. The project trains graduate and undergraduate students in the interdisciplinary
skills spanning AI, formal methods, and hardware design that the semiconductor workforce needs.

**Funding.** NSF FET Award #2615387 — CISE Future Computing Research (NSF 25-543), a Standard
Grant of \$800,000 (Sept 2026 – Aug 2030).

**Team.** PI Nathaniel Bleier (CSE); co-PIs Siqian Shen (IOE) and Yatin Manerkar (CSE), in
collaboration with the Michigan Institute for Computational Discovery and Engineering.