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

SHF: Neuro-Symbolic Reasoning for Verified Hardware-Software Co-Design Specialized computer chips called accelerators are everywhere in modern life: they power voice recognition in phones, driver-assistance features in cars, medical imaging machines, satellite instruments, and the data centers behind everyday internet services. Designing one of these chips is exceptionally hard because countless decisions about which operations to build into silicon, how to lay out the circuits, and how to translate software onto them all interact. Today, designers either spend years exploring this enormous space of choices by hand or rely on automated tools that may produce inefficient or incorrect designs. As demand for energy-efficient computing grows, particularly to support artificial intelligence services that already strain national electricity supplies, the cost of poor design decisions is rising. This project develops a new framework that combines two complementary ways of reasoning about hardware: pattern-finding methods drawn from artificial intelligence, which can quickly suggest promising designs, and mathematical proof techniques, which can guarantee that a design behaves correctly. Together they make it possible to explore far larger design spaces than today's tools allow while preserving the correctness guarantees that applications such as automotive and medical devices demand. The resulting open-source software lowers barriers for chip designers working outside large companies, supports United States semiconductor competitiveness, and helps train graduate and undergraduate students in skills that the domestic semiconductor workforce urgently needs. The project develops a neuro-symbolic framework for hardware-software co-design that formulates accelerator design as the joint synthesis of hardware specializations and the software transformations that target them, rather than treating the software workload as a fixed input. The research is organized in three coordinated activities. The first activity combines learning-guided program synthesis with automated logical reasoning to generate equivalent instruction sequences, control codes for accelerator datapaths, and microcoded expansions for rare instructions, in each case formally proven equivalent to the original program. The second activity uses equality saturation, a representation that compactly captures large families of equivalent programs, together with integer-programming-based extraction to globally optimize across choices that are normally treated separately: which instructions a chip should support, how its microarchitecture is parameterized, and how the software is transformed to fit. The third activity applies inductive proof techniques originally developed for hardware verification to discover redundancies that emerge once a chip is restricted to a known class of workloads, enabling general-purpose circuits to be automatically pruned into compact application-specific designs. The framework will be validated on application-specific instruction-set processors and on domain-specific accelerators, with evaluation across standard embedded benchmark suites measuring chip area, power, performance, and end-to-end functional correctness. Preliminary work by the team has already demonstrated up to 40 percent area reduction and 8 percent power savings versus state-of-the-art baselines, and the project will release the full toolchain, benchmarks, and synthesized designs as open-source infrastructure to support adoption by industry, academia, and educational use. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.