Skip to content
STIMSMITH

UCLID5 Verification Condition: correspondence invariant

CodeArtifact WIKI v1 · 5/26/2026

The `correspondence` invariant is a UCLID5 verification condition used in the formal verification of pipelined Y86-64 microprocessors. It checks that the state produced by PIPE execution is consistent with the state produced by SEQ execution after the required flushing sequence and under the permitted initial pipeline-state restrictions.

Overview

The correspondence invariant is the UCLID5 representation of a correctness condition for verifying that a pipelined Y86-64 processor model (PIPE) behaves consistently with a sequential processor model (SEQ). The cited source identifies Figure 14 as a "Verification Condition" and states that the check ensures PIPE operation is consistent with SEQ operation. [C1]

invariant correspondence :
(
 step  > nflush+3
 && pipe_state_ok0
) ==>
 ((S_stat_b0 == SAOK ==> S_pc_a == S_pc_b0)
   &&  S_rf_a == S_rf_b0
   &&  S_cc_a == S_cc_b0
   &&  S_mem_a == S_mem_b0
   &&  S_stat_a == S_stat_b0) ||
 ((S_stat_b0 == SAOK ==> S_pc_a == S_pc_b1)
   &&  S_rf_a == S_rf_b1
   &&  S_cc_a == S_cc_b1
   &&  S_mem_a == S_mem_b1
   &&  S_stat_a == S_stat_b1);

Verification setup

The symbolic simulation uses two parallel copies of the PIPE model, named pipe_A and pipe_B, plus one copy of SEQ. Both PIPE copies start from the same initial state, with symbolic constants and uninterpreted functions used to encode the possible pipeline states, or a superset of them. [C2]

The verification framework includes control signals that allow PIPE to operate in either normal or flushing mode, allow SEQ state elements to import values from corresponding PIPE elements, and allow SEQ itself to operate. During execution, state-variable values are captured as UCLID5 variables, and assertions over those captured variables are verified. [C3]

Invariant timing condition

The invariant is syntactically required to hold at every symbolic-simulation step, but its antecedent restricts the meaningful obligation to steps satisfying:

step > nflush+3 && pipe_state_ok0

The source explains that step > nflush+3 means the correspondence need only hold at steps n + 4 and beyond. This timing arises from the UCLID5 state-machine model, where state updates occur simultaneously and a changed control signal takes a full cycle before its new value becomes current. For a verification requiring n flushing steps, the overall symbolic-simulation sequence therefore requires n + 4 steps. [C4]

The other antecedent term, pipe_state_ok0, represents restrictions that may be imposed on the initial pipeline state. [C5]

State correspondence checked

The consequent is a disjunction of two possible state correspondences. In each branch, the invariant compares the architectural state captured from pipe_A against one of two captured SEQ-related states, using either the b0 or b1 suffixes:

  • program counter: S_pc_a compared to S_pc_b0 or S_pc_b1, conditionally;
  • register file: S_rf_a compared to S_rf_b0 or S_rf_b1;
  • condition codes: S_cc_a compared to S_cc_b0 or S_cc_b1;
  • memory: S_mem_a compared to S_mem_b0 or S_mem_b1;
  • status: S_stat_a compared to S_stat_b0 or S_stat_b1. [C6]

The program-counter comparison is guarded by S_stat_b0 == SAOK. The source notes that the consistency condition for the PC is imposed only for steps in which the processor starts in normal execution. [C7]

Role in the proof

This invariant is part of a Burch-Dill-style symbolic simulation approach: instead of running from a reset state for many cycles, the machine is operated over all possible states for a short simulation sequence. The correspondence invariant then states the architectural equality condition that must hold after the flushing and setup sequence has completed. [C8]

CITATIONS

8 sources
8 citations
[1] Figure 14 is a UCLID5 verification condition named `correspondence` that checks PIPE operation for consistency with SEQ operation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] The symbolic simulation is expressed as parallel runs of two PIPE copies, `pipe_A` and `pipe_B`, plus one SEQ copy, with both PIPE copies starting from the same symbolic initial state. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] The verification framework includes control signals for normal or flushing PIPE operation, importing PIPE values into SEQ state elements, and operating SEQ; state-variable values are captured as UCLID5 variables for assertions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] Although the condition is expressed as an invariant, `step > nflush+3` means correspondence is required only at steps `n + 4` and beyond; this relates to UCLID5's simultaneous state-update model and flushing-step sequencing. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] `pipe_state_ok0` describes restrictions that may be imposed on the initial pipeline state. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] The invariant's consequent compares program counter, register file, condition codes, memory, and status values between `S_*_a` and either the `b0` or `b1` state. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] The PC consistency condition is imposed only when the processor starts in normal execution, represented in the invariant by the guard `S_stat_b0 == SAOK`. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] The approach differs from traditional simulation-based testing by operating over all possible states for a short simulation sequence rather than starting from reset and running for many cycles. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5