Symbolic Execution of Digital Hardware Designs: A Systematic Map of Path-Conditioned Design Execution

Summary

A systematic map and critical survey of path-conditioned symbolic execution for digital hardware designs, with RTL at the center. The survey uses a strict five-part operational test: a qualifying work executes a design or documented derived representation with symbolic hardware values, constructs predicates for alternatives distinguished by that design representation over control and, for sequential designs, time, uses feasibility to choose or reconstruct execution, and makes that mechanism load-bearing in its result. A derived or HLS representation must document a semantic bridge adequate to the design-level claim; paths that fork only in an external testbench do not qualify.

The map distinguishes classical, concolic, and selective-hybrid execution. Symbolic simulation, STE, BMC, trace-only search, and generic synthesizable-source analysis are treated as adjacent rather than silently folded into the topic. The survey explains hardware path semantics, semantic bridges, scaling mechanisms, evidence strength, and the contract needed to interpret a test, exploit, coverage result, mismatch, or bounded conclusion.

Reading list

The works below anchor the mechanism and evidence synthesis. The complete map and every exclusion decision are in the survey record.

Foundations and classical execution

Paper	What	Venue · Year	Notes
Building SystemC Waiting State Automata	Scheduler-aware symbolic paths and trace composition	VECoS · 2011	notes
Hardware Verification Using Software Analyzers	Verilog-to-C execution separated from BMC and abstract interpretation	ISVLSI · 2015	notes
Generating High Coverage Tests for SystemC Designs Using Symbolic Execution	KLEE extended with SystemC scheduling, signals, datatypes, and clocks	ASP-DAC · 2016	notes
Automatic Generation of High-Coverage Tests for RTL Designs Using Software Techniques and Tools	Verilator-to-C++ execution with RTL witness replay	ICIEA · 2016	notes
End-to-End Automated Exploit Generation for Validating the Security of Processor Designs	Backward cycle-level execution and replayed processor exploits	MICRO · 2018	notes
EISec: Exhaustive Information Flow Security of Hardware Intellectual Property Utilizing Symbolic Execution	Gate-netlist path execution for information-flow witnesses	AsianHOST · 2022	notes
Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs	Solver-checked composition of independent RTL path fragments	FMCAD · 2023	notes
SEIF: Augmented Symbolic Execution for Information Flow in Hardware Designs	Static-flow landmarks guide replayable RTL security witnesses	HASP · 2023	notes

Concolic and selective-hybrid execution

Paper	What	Venue · Year	Notes
Scalable Test Generation by Interleaving Concrete and Symbolic Execution	One time-indexed HDL trace with a solver-targeted diversion	VLSID · 2014	notes
Directed Test Generation Using Concolic Testing on RTL Models	Target-aware CFG guidance for concrete/symbolic RTL search	DATE · 2018	notes
Scalable Concolic Testing of RTL Models	Hardware-aware contribution analysis and state reuse	IEEE TC · 2021	notes
FuSS: Coverage-Directed Hardware Fuzzing with Selective Symbolic Execution	Fuzzer prefix, Verilated state snapshot, and local symbolic suffix	ACM TECS · 2025	notes
AutoVeriFix+: High-Correctness RTL Generation via Trace-Aware Causal Fix and Semantic Redundancy Pruning	Concolic branch refinement inside an LLM RTL repair workflow	arXiv · 2026	notes

HLS and cross-level contracts

Paper	What	Venue · Year	Notes
Hardware/Software Co-verification Using Path-based Symbolic Execution	Coupled hardware/software paths with explicit interface assumptions	arXiv · 2020	notes
Processor Verification Using Symbolic Execution: A RISC-V Case-Study	Verilated RTL and ISS co-execution at retirement boundaries	DATE · 2023	notes
Using Symbolic Execution to Analyze the Hardware TCP Protocol	HLS datatypes, streams, and timing with source-level claims	M.S. thesis · 2024	notes
Comparing Methods for the Cross-Level Verification of SystemC Peripherals With Symbolic Execution	Standalone and reference-coupled SystemC execution	IEEE TCAD · 2026	notes