Skip to content
STIMSMITH

Burch-Dill Correspondence Checking

Concept WIKI v1 · 5/25/2026

Burch-Dill correspondence checking is a formal verification approach for pipelined microprocessors. It proves that a pipelined implementation maintains an abstraction to the architectural state of a sequential ISA model, using symbolic simulation and pipeline flushing to compare two execution scenarios. The method establishes safety but must be complemented by liveness checking to rule out designs that never make forward progress.

Overview

Burch-Dill correspondence checking is an approach to formal microprocessor verification based on ideas described by Burch and Dill in 1994. Its goal is to prove that a pipelined microprocessor faithfully implements the sequential semantics of an instruction-set architecture (ISA) model for all possible instruction sequences.[C1]

The approach is motivated by the gap between ISA specifications and high-performance implementations. An ISA model describes the effect of each instruction on architectural state—registers, the program counter, and memory—under strict sequential execution. Pipelined processors overlap multiple instructions, so verification must show that the pipelined execution obtains the same result as a purely sequential ISA implementation.[C1]

Core method

The central requirement is an abstraction function, usually denoted α, that maps microprocessor states to architectural states. Verification must show that this mapping is maintained by each cycle of processor operation.[C2]

Burch and Dill's key contribution was showing that this abstraction function can be computed automatically by symbolically simulating the microprocessor while it flushes instructions out of the pipeline.[C3] This relies on the fact that most pipelined designs already include a mechanism for pipeline flushing, because flushing is needed to bring the pipeline to a quiescent state during exceptional conditions such as halting or interrupt handling.[C3]

For a single-issue microprocessor, the verification obligation becomes an equivalence check between two symbolic simulations:

  1. Flush the pipeline, then execute a single instruction in the ISA model.
  2. Let the pipeline operate for one normal cycle, then flush the pipeline.

The cited report calls this equivalence-based verification strategy "correspondence checking."[C4]

Modeling style and abstraction

Burch-Dill verification uses data abstraction to reduce the verification burden. Rather than modeling all hardware operations at exact bit-level detail, term-level modeling treats data values as symbolic terms. Operations such as instruction decoding and ALU behavior can be represented as uninterpreted functions, and parameters such as register count, memory size, and bit widths can also be abstracted away.[C5]

These abstractions allow the verifier to focus on pipeline control logic instead of low-level data representation. The evidence notes that Burch and Dill demonstrated the value of these abstractions in an automated microprocessor verification tool.[C5]

Safety property and liveness limitation

Burch-Dill verification proves a safety property: every cycle of processor operation has an effect consistent with some number of steps k of the ISA model.[C6] The value k may be zero, meaning a cycle causes no progress in program execution. This can occur during stalls for hazards or when instructions are canceled after a mispredicted branch.[C6]

Because k = 0 is allowed, safety alone does not rule out a deadlocked processor. The evidence explicitly notes that a processor that does nothing can pass the safety verification, so a complete verification must also prove liveness: the processor cannot reach a state where it never makes forward progress.[C6]

Use in UCLID5-based Y86-64 verification

In the UCLID5-based verification of pipelined Y86-64 microprocessors, the modeled system combines a pipelined microprocessor with a sequential reference implementation. The UCLID5 verification script specifies initialization, operation, and the verification conditions needed to carry out Burch-Dill correspondence checking.[C7]

UCLID5 supports term-level modeling using uninterpreted types and uninterpreted functions. These are suitable for the style demonstrated by Burch and Dill, where hardware blocks can be abstracted as consistent functions shared between the pipeline and the sequential reference model.[C8]

LINKED ENTITIES

6 links
Abstraction Function USES
Symbolic Simulation USES
Pipeline Flushing USES
Burch PROPOSED
Dill PROPOSED
Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5 APPLIES

CITATIONS

8 sources
8 citations
[1] Burch-Dill correspondence checking verifies that pipelined microprocessor execution faithfully implements the sequential semantics of an ISA model for all instruction sequences. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] The approach requires an abstraction function α mapping microprocessor states to architectural states, maintained by each cycle of processor operation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] Burch and Dill's key contribution was automatic computation of the abstraction function by symbolic simulation while flushing instructions out of the pipeline. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] For a single-issue microprocessor, correspondence checking proves equivalence between flushing then executing one ISA instruction and running one pipeline cycle then flushing. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] Burch-Dill-style verification uses term-level modeling and uninterpreted functions to abstract data representations, operation details, and parameters such as register counts, memory words, and bit widths. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] Burch-Dill verification proves safety but does not by itself prove liveness, because k may be zero and a deadlocked processor can still pass the safety check. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] In the UCLID5 Y86-64 verification, the modeled system combines a pipelined microprocessor and sequential reference implementation, and the script carries out Burch-Dill correspondence checking. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] UCLID5 supports uninterpreted terms and functions suitable for Burch-Dill term-level modeling, including consistent abstract models of hardware blocks used in both the pipeline and sequential reference model. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5