Content area
Ensuring the correctness and security of hardware designs is critical in modern computing systems. Formal verification methods, particularly model checking, are widely used in industry to verify functional correctness. Recently, symbolic execution has emerged as a powerful alternative for hardware security verification. However, symbolic execution faces fundamental scalability challenges. Symbolic execution suffers from the path explosion problem, where the number of execution paths grows exponentially with the number of branch points executed. Furthermore, symbolic execution engines rely heavily on satisfiability modulo theories (SMT) solvers to compute satisfiability queries, which dominate the overall runtime and remain a bottleneck.
This dissertation introduces three innovations to make symbolic execution practical for large-scale hardware verification. First, we present the Sylvia hardware symbolic execution engine and a new technique called piecewise composition, which leverages the modularity of hardware designs to reduce redundant path exploration. By decomposing execution into independent logical blocks and reconstructing full execution paths using SMT queries, piecewise composition significantly reduces the number of paths explored per clock cycle. Building from here, SylQ-SV extends our hardware-oriented symbolic execution engine by adding language support for SystemVerilog and SystemVerilog Assertions. Furthermore, we bring query caching to the hardware domain to reduce redundant solver invocations. Finally, we develop SEIF, a symbolic execution-based information flow analysis framework that integrates symbolic execution with a static signal connectivity graph, guiding path exploration toward security-critical flows.
We evaluate our approaches on multiple open-source hardware designs, including system-on-chip (SoC) architectures and CPU cores, and contribute a new set of open-source hardware security verification benchmarks to the community. Our results demonstrate that piecewise composition reduces redundant work, query caching significantly improves execution time, and augmenting symbolic execution with static analysis unlocks information flow validation. By addressing the scalability challenges of symbolic execution, this work establishes new foundations for efficient, security-driven symbolic execution of hardware designs.