Skip to content

Sequential Symbolic Execution

Jump to bottom
julianspeith edited this page Aug 12, 2026 · 2 revisions

The sequential_symbolic_execution plugin performs symbolic execution across multiple clock cycles, including sequential gates. Where ordinary Boolean function extraction stops at the first flip-flop, this plugin unrolls the circuit over time and gives you the symbolic value of a net at a chosen cycle.

This plugin is not built by default. Rebuild HAL with -DBUILD_ALL_PLUGINS=ON or -DPL_SEQUENTIAL_SYMBOLIC_EXECUTION=ON, see Building HAL. It builds on Z3 and returns Z3 expressions rather than HAL Boolean functions.

Why this matters

Combinational reasoning has a hard boundary: the register. SubgraphNetlistDecorator.get_subgraph_function (see Decorators) recursively composes gate functions and stops as soon as it reaches a flip-flop, because the value stored there depends on when you look.

That is exactly the boundary you need to cross for any design that computes over several cycles — which is most interesting hardware. A block cipher applies its round function repeatedly; a controller's output depends on the state it reached three cycles ago; a counter's value is a function of how long it has been running. None of these can be expressed as a single combinational function, but all of them can be expressed as a function of the initial state and the inputs applied at each cycle.

Symbolic execution over time is how you get there: unroll the circuit for n cycles, treat the inputs at each cycle as separate symbolic variables, and you obtain a closed-form expression for what a net holds at cycle n. That expression can then be simplified, compared against a reference, or handed to a solver — see Z3 Utilities.

The cost is that unrolled expressions grow quickly with the number of cycles, so this is a tool for targeted questions about a handful of cycles rather than for whole-design analysis.

Usage

The plugin is used from Python via the sequential_symbolic_execution module. Because it operates in terms of Z3 expressions, you will typically use it together with Z3 Utilities.

from hal_plugins import sequential_symbolic_execution

get_pg_word_values_at_z3(...) evaluates whole module pin groups as multi-bit words at given time indices, which is the word-level entry point and usually what you want: it answers "what does this register hold at cycle n" rather than asking bit by bit.

The evaluation is parameterized by:

Concept Meaning
Words Groups of nets treated as one multi-bit value, typically taken from module pin groups
Time indices The cycles at which each word should be evaluated
Subgraph gates Which gates are included in the unrolled circuit; everything outside becomes a free input
Known inputs Concrete values for inputs at specific cycles, which massively reduce expression size
Word-level calculations Pin groups whose behavior is already known and can be substituted instead of unrolled

Supplying known inputs and known word-level behavior is what makes this tractable. Every input you pin down is one fewer symbolic variable to carry through the unrolling, and every already-identified subcircuit you substitute is a block of logic that does not have to be expanded at all — which is why this plugin pairs naturally with module identification.

Because the C++ interface exposes Z3 types directly, consult the Python API documentation for the exact signatures available in your build.

Practical notes

  • Bound the number of cycles. Expression size grows with each unrolled cycle; the difference between 3 cycles and 30 is not linear.
  • Pin down what you know. Known inputs and substituted word-level operations are the difference between a tractable query and one that never returns.
  • Restrict the subgraph. Include only the gates relevant to the net you are asking about; everything else becomes a free variable that inflates the expression.

See also

Clone this wiki locally