Skip to content
STIMSMITH

State Machine Model

Concept WIKI v1 · 5/26/2026

A state machine model, as described for UCLID5 hardware modeling, represents hardware state with present and next values. Next-state values are computed from current state and then all state variables are synchronously updated, making it suitable for modeling synchronous hardware such as pipelined microprocessors.

Definition

In the UCLID5 hardware-modeling setting, a state machine model represents a system by computing a next state from the current state and then transitioning to that next state. Hardware is expressed this way in UCLID5, while software is modeled as a sequence of operations that update parts of the system state. [C1]

State variables and update semantics

UCLID5 associates two values with each state variable in the hardware state-machine model:

  • the present value, referenced by the ordinary variable name; and
  • the next value, referenced by appending a single quote to the variable name. [C2]

For example, var denotes the current value of a state variable, while var' denotes its next-state value. Assignment statements define next-state values based on current state variables and, in some cases, other next-state values. Conceptually, the state machine first computes all next-state values and then synchronously updates all state variables so that their next values become their present values. [C2]

Contrast with serial execution

UCLID5 distinguishes the state-machine model from a serial execution model. For software modeling, assignment statements execute in sequence and update some portion of the system state at each step. For hardware modeling, the state-machine model instead computes a full next state and then updates state elements together. [C1]

Use in hardware verification

The state-machine model is used in the cited UCLID5 verification work to model synchronous hardware, specifically pipelined Y86-64 microprocessors and their sequential reference implementation. The verification setup uses a modeling language to describe the system and a command language to initialize state, operate the system, and check verification conditions. [C3]

In symbolic simulation, state variables can be captured as UCLID5 variables, and assertions can then be verified over those recorded values. In the cited pipeline verification, two copies of the PIPE model and one copy of the SEQ model are run in parallel to express correspondence-checking sequences. [C4]

Timing consequences

Because state updates are synchronous, changing a control signal does not immediately change its present value. The cited report notes that changing a control signal, such as one used to start flushing, takes a full cycle before the changed next state becomes the current value of that signal. For a verification requiring n flushing steps, the overall symbolic-simulation sequence requires n + 4 steps. [C5]

UCLID5 also allows an individual module at a step either to remain in its current state or to operate for one step. During symbolic simulation, the symbolic state of selected modules can be recorded, and correctness conditions can be expressed over those recorded states. [C5]

Procedures as next-state computations

The cited authors report that direct use of primed and unprimed variables can be difficult when translating hardware control logic, because some expressions need current values while others need values computed earlier in the same clock cycle. To handle this, they used a mixed strategy: the processor is described as a state machine, but next-state computation is expressed with procedures. [C6]

Under this style, UCLID5 treats assignments within procedures as assignments to next-state values, while using assignment ordering to determine whether later expressions refer to current or next values. The report gives the example:

varA = varA + varB;
varB = varA + varB;

which is equivalent to:

varA' = varA + varB;
varB' = varA' + varB;

This procedural style requires the ordering of procedure calls and assignments to respect signal flow through the circuit’s combinational logic. [C6]

Role in verification conditions

In the cited verification, correctness conditions are expressed as invariants over symbolic simulation steps. One invariant checks that PIPE operation is consistent with SEQ operation after the necessary flushing sequence. The invariant’s antecedent includes a step bound, step > nflush+3, meaning the correspondence is required only from step n + 4 onward. [C7]

LINKED ENTITIES

2 links
UCLID5 implements_model
Burch-Dill Correspondence Checking used_in_verification

CITATIONS

7 sources
7 citations
[1] UCLID5 models hardware as state machines that compute a next state from the current state and then transition to that next state, while software uses sequential operations. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] In the UCLID5 state-machine model, each state variable has a present value and a next value; the next value is denoted with a prime, and all state variables are synchronously updated after next-state computation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] The cited UCLID5 verification work models a combination of a pipelined microprocessor and a sequential reference implementation and uses scripts to initialize state, operate the system, and check verification conditions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] The verification captures state-variable values as UCLID5 variables and runs two PIPE model copies plus one SEQ model copy in symbolic simulation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] Because synchronous state-machine updates delay control-signal changes by a full cycle, a verification requiring n flushing steps needs n + 4 symbolic-simulation steps; modules may either remain in their current state or operate for one step. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] The authors used procedures to express next-state computation within a state-machine processor model; UCLID5 treats procedure assignments as next-state assignments and uses assignment order to determine whether references are to current or next values. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] A PIPE-versus-SEQ correctness condition is represented as an invariant, with the step condition step > nflush+3 limiting the required correspondence to steps n + 4 and beyond. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5