SYLQ-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching

Symbolic execution explores every path through a hardware design to find bugs and security flaws, giving high-quality verification, but it drowns in the path-explosion problem and in expensive SMT solver calls at each branch, so it is too slow for large designs; this paper (University of North Carolina — Kaki Ryan, Cynthia Sturton) presents SylQ-SV, a SystemVerilog symbolic execution engine that borrows query caching from software analysis — slicing each solver query to its minimal form, normalizing and renaming it so equivalent queries are recognized, and caching results to skip the solver on a hit — reaching a cache hit rate over 60 percent, cutting solver calls by 74 percent, and reducing run time by up to 17 percent over the state of the art, with full support for SystemVerilog Assertions and evaluation on real SoCs like OpenTitan.

Why this problem is worth solving

Verifying that a chip design is correct and secure before it is manufactured is a high-stakes, expensive activity, and symbolic execution is one of the most thorough tools for it.

The reason cost is so stubborn is that two different expenses compound, and the obvious remedy from software does not transfer cleanly.

What people did before, and where it broke

• Concrete simulation and testing. Run the design on many concrete input vectors and check outputs. Where it broke. It only covers the inputs actually tried, missing corner-case bugs and security flaws that symbolic execution’s all-paths reasoning would catch.
• Software symbolic-execution engines (KLEE-style) or Verilog-only tools. Reuse existing symbolic-execution machinery, or tools that handle only small designs or single modules. Where it broke. They lack full support for real SystemVerilog, including SystemVerilog Assertions, so they cannot run end-to-end on the large open-source designs used in practice.
• Piecewise composition (Sylvia). Cut path explosion with a divide-and-conquer approach that reduces duplicated path exploration by an order of magnitude. Where it broke. It greatly helps the exploration side, but the SMT solver queries remain expensive and numerous, so run times stay high — well over a minute to find a violation in a RISC-V SoC.
• Naive whole-path query caching. Cache the solver’s answer to each path’s full constraint and reuse it. Where it broke. No two feasible paths have equivalent or co-satisfiable constraints, so whole-path queries essentially never repeat and the cache never hits.
• The gap. No hardware symbolic-execution engine made query caching pay off — by caching normalized sub-queries that actually recur and recognizing equivalent queries — while also fully supporting SystemVerilog and its assertions for end-to-end verification of real designs.

How SylQ-SV works

The idea

Cache what recurs — sub-queries — not whole paths that never repeat. The pivotal realization in SylQ-SV is that caching, which slashes solver cost in software symbolic execution, seemed inapplicable to hardware because whole-path constraints are all distinct — no two feasible paths share a constraint. The fix is to change the granularity: slice each solver query down to the minimal relevant sub-query, and cache those, because the same small logical questions arise again and again across many different paths even when the full paths never match. This is the standard memoization move — remember the answer to an expensive computation so you never pay for it twice — applied at the right unit of work. Caching and reusing the results of expensive repeated work so the system stops recomputing what it has already figured out is the same efficiency principle the work on caching multi-level indexes in domain-specific architectures… — but more precisely here, reusing an SMT solver as the expensive engine and being clever about when you must actually invoke it echoes the concern the work on a solver-aided compiler for packet-processing pipelines covered elsewhere on this site is built on, where the solver is the workhorse and the art is in how sparingly and effectively you call it. SylQ-SV’s art is calling the solver far less by caching normalized sub-queries.

Recognize equivalent queries cheaply, trading precision for low overhead. Caching sub-queries only helps if you can tell when two queries are really the same despite looking different, and that recognition is itself hard: computing a true canonical form for bitvector formulas is NP-hard. SylQ-SV takes a lightweight, polynomial-time approach — normalizing the atomic propositions, reordering the propositional terms, and renaming variables to a set scheme — so it catches most equivalent queries without paying an intractable normalization cost. This is a deliberate accuracy-versus-overhead trade: a cheaper normalization that misses some equivalences but keeps the caching itself fast. Making a verification analysis scale by carefully engineering it to avoid intractable steps while still delivering rigorous results is the same discipline the work on verifying crash consistency via symbolic reasoning and an SMT solver covered elsewhere on this site pursues, keeping a solver-backed analysis tractable. SylQ-SV’s contribution is a normalization scheme tuned so that query caching nets out to a real speedup rather than being swamped by its own overhead.

Support the language and the whole workflow, on real designs. A verification tool is only useful if it runs on the designs people actually build, so SylQ-SV provides full support for SystemVerilog, including SystemVerilog Assertions, enabling end-to-end verification of the open-source designs common in the literature, and it adds SystemVerilog-specific optimizations such as caching always_comb blocks to avoid redundant traversals of combinational logic. Scaling a tool for real hardware designs by handling their actual language and structure, rather than a simplified subset, is the same practicality the work on scaling RTL analysis to real designs covered elsewhere on this site embodies, meeting hardware where it is written. SylQ-SV demonstrates this by verifying full CPUs and systems-on-chip end to end, and by making its source and evaluation data public so the results can be reproduced and built upon.

Following a query through SylQ-SV

Every branch point is a potential solver call, and solver calls dominate cost.

Why it works

• Sub-queries recur where whole-path queries never do. No two feasible paths share a full constraint, so caching whole queries never hits → but slicing exposes small sub-queries that arise across many paths → so the cache finds real matches and skips real solver calls.
• Normalization makes equivalent queries look identical. Logically equivalent queries can be written many syntactic ways, defeating a literal cache → but normalizing propositions, reordering terms, and renaming variables collapses them to one form → so equivalents hit the same cache entry.
• A lightweight normalization keeps caching a net win. A true canonical form is NP-hard, so exact normalization would cost more than it saves → but a polynomial-time approximate normalization catches most equivalences cheaply → so the caching nets out to a speedup rather than overhead.
• Skipping the solver attacks the dominant cost. SMT queries over bitvectors are the expensive part of hardware symbolic execution → but a cache hit returns the answer without invoking the solver → so cutting solver calls by most of them cuts run time directly.
• Language and combinational-logic support make it real. A tool that cannot parse real SystemVerilog or re-walks combinational logic each cycle is slow or unusable → but full SVA support and cached always_comb blocks avoid that → so SylQ-SV verifies full CPUs and SoCs end to end.

What it costs (trade-offs and scope)

• The gain is a run-time reduction, not a change in what is verified. SylQ-SV cuts run time by up to 17 percent over the state of the art by avoiding solver calls; it accelerates the same symbolic-execution analysis rather than making a previously impossible verification possible, and the headline speedup, while meaningful, is incremental on top of Sylvia’s order-of-magnitude exploration gains.
• Caching trades memory for time. Maintaining a cache of solved queries consumes memory that grows with the number of distinct normalized queries; the paper notes this trade-off, so the benefit assumes enough memory to hold a useful cache.
• Normalization is approximate and adds its own overhead. Because exact canonicalization is NP-hard, SylQ-SV uses a lightweight normalization that misses some equivalences (so not every reusable query is recognized) and still costs time per query; the design balances this, but it is a real overhead that limits the achievable hit rate.
• The results are for specific designs and one baseline. The over-60-percent hit rate, 74 percent solver-call reduction, and 17 percent run-time reduction are measured on the OR1200 CPU, OpenTitan SoC, and two HACK@DAC SoCs against the state-of-the-art engine; other designs, properties, and solvers could shift the numbers.
• It inherits symbolic execution’s fundamental limits. Query caching does not eliminate path explosion; symbolic execution can still be overwhelmed by designs with enormous numbers of paths, and SylQ-SV’s contribution is to make each solver query cheaper on average, not to remove the exponential path count.

The evaluation

Check yourself

Sources

The paper is “SylQ-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching” by Kaki Ryan and Cynthia Sturton (University of North Carolina at Chapel Hill), published at ASPLOS 2025 (Volume 3), DOI 10.1145/3676642.3736123. It is licensed CC BY.

This explainer is written from the paper’s full text (the authors’ PDF of the ASPLOS 2025 paper). The paper presents SylQ-SV, a dedicated SystemVerilog symbolic execution engine that uses SMT query caching to scale symbolic execution of hardware designs, a path-based analysis that delivers high-quality coverage and security verification but struggles with path explosion and remains expensive. The key ideas: symbolic execution’s remaining cost is dominated by SMT solver queries, and although naive whole-path query caching fails (no two feasible paths have equivalent or co-satisfiable constraints), caching the right pieces works. SylQ-SV draws query slicing, query normalization, and variable renaming from the software-engineering community to improve query reuse — slicing ensures only the minimum query is used, and normalization plus renaming let equivalent queries be recognized — and, because computing a true canonical form is NP-hard, it uses a lightweight polynomial-time normalization (normalizing atomic propositions, reordering propositional terms, renaming variables). It builds on the Sylvia engine’s piecewise composition (a divide-and-conquer approach that reduced duplicated path exploration by an order of magnitude) and adds SystemVerilog-specific optimizations, including a look-up table for always_comb blocks to avoid re-walking the syntax tree for combinational logic twice per clock cycle, and extending piecewise composition to combinational logic. The reported results are the paper’s own: a maximum cache hit rate of over 60 percent, a 74 percent average reduction in solver calls, and up to a 17 percent run-time reduction over the state of the art, with full support for SystemVerilog and SystemVerilog Assertions, evaluated on the OR1200 CPU, the OpenTitan SoC with Ibex core, and two HACK@DAC competition SoCs (with PULPissimo and CVA6 cores); the source code and evaluation data are publicly available. No numbers beyond the paper’s own have been introduced; exact algorithms, the normalization procedure, and the full evaluation should be confirmed in the paper.