Skip to content
STIMSMITH

Burch-Dill Correspondence Checking

Technique WIKI v1 · 5/26/2026

Burch-Dill Correspondence Checking is presented in the provided evidence as a verification technique for comparing a pipelined microprocessor against a sequential reference implementation. In the UCLID5-based Y86-64 work, the technique requires a combined model of PIPE and SEQ, a script that drives the correspondence check, a projection mechanism from implementation architectural state to the reference model, and a pipeline-flushing mechanism so in-flight instructions can complete before comparison.

Overview

Burch-Dill Correspondence Checking is used in the cited UCLID5 verification work to relate a pipelined microprocessor model to a sequential reference implementation. The modeled system consists of a combination of a pipelined microprocessor and the sequential reference implementation, while the UCLID5 verification script specifies how the state is initialized, how the system is operated, and which verification conditions are checked for Burch-Dill correspondence checking.

In this setting, the method is implemented over hardware-style state-machine models. UCLID5 models hardware by computing a next state from the current state and then transitioning to that next state; for the pipelined-microprocessor verification described in the evidence, only UCLID5's hardware modeling aspects were used.

Core setup

The evidence identifies two special framework extensions needed for Burch-Dill verification:

  1. Projection from PIPE to SEQ. The sequential reference framework must be able to load the architectural state from the pipelined implementation before running one step of SEQ's normal operation. This was implemented with an input signal named proj_impl, which loads the program counter, register file, data memory, and status register from module inputs into the SEQ state.
  2. Pipeline flushing. The pipelined implementation must support a flushing mechanism. Flushing stops the fetching of new instructions while allowing instructions already in the pipeline to complete. The PIPE framework was augmented with an input control signal named force_flush for this purpose.

Flushing behavior

Flushing is implemented by injecting a bubble into the decode stage on each cycle until the pipeline is empty. This dynamically injects nop instructions and sets the status register to SBUB, indicating a pipeline bubble. The evidence notes that bubble injection was already part of the pipeline control logic for ordinary execution cases, such as waiting for a return address to be popped from the stack during a ret instruction.

The evidence also records two subtle requirements for correct flushing:

  • Flushing should not stall the fetch stage or hold the fetch-stage program counter (predPC) fixed, because doing so would prevent a ret or jXX instruction from setting the program counter to the return or jump destination.
  • For variant SW, which stalls the pipeline for one cycle to convert a popq instruction into a two-instruction sequence, flushing must be disabled for one cycle when that conversion occurs.

Pipeline-register semantics

The pipeline-register model used in the evidence supports four possible behaviors on a step: initialization, stalling, bubble injection, or loading its input. This behavior is relevant because flushing relies on bubble injection, while ordinary pipeline operation may also require stalls or normal input loading.

Abstraction and term-level modeling

The evidence connects Burch-Dill-style term-level modeling with UCLID5's uninterpreted types and functions. Uninterpreted terms can be checked for equality, and uninterpreted functions are treated as arbitrary but consistent functions. Such functions are useful for hardware blocks whose exact functionality is not required, provided they behave consistently in both the pipeline and sequential reference models.

The verification work also explores abstraction choices for data and operations. Data can be modeled as uninterpreted values, integers, or bit vectors. Uninterpreted data types are more abstract than concrete integer or bit-vector data, and uninterpreted functions are more abstract than precise mathematical functions. Main memory can be modeled either as an array or as an uninterpreted memory state with uninterpreted read and write functions; because the pipelined implementations perform memory operations in program order, the uninterpreted memory model sufficed in the reported work.

ALU-model precision

The evidence describes a hierarchy of ALU models used with the verification, ranging from an entirely uninterpreted ALU to partially interpreted and precise versions. An uninterpreted ALU sufficed for pipeline variants STD, FULL, STALL, and LF. A model capturing x + 0 = x was required for NT and BTFNT. A model attempting to capture (x + 8) + -8 = x was required for variant SW, but the SMT solver could not make effective use of the axiom encoding this property, so verification at that abstraction level was unsuccessful. A model that fully interprets addition while leaving other operations uninterpreted sufficed for all pipeline variants. The most precise model interprets addition and subtraction, and with bit-vector data also models bitwise logical operations.

Safety and liveness caveat

The evidence warns that a safety-style correspondence check alone can be insufficient: a processor that deadlocks, or even a device that does nothing, can pass such a verification. To complete the verification, liveness must also be checked, specifically that the processor cannot enter a state where it never makes forward progress. The cited report describes an approach that builds on the safety property to show that the pipeline does not stall indefinitely.

LINKED ENTITIES

1 links
UCLID5 implemented_with

CITATIONS

11 sources
11 citations
[1] UCLID5 model and verification script are used to carry out Burch-Dill correspondence checking over a combined pipelined processor and sequential reference implementation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] UCLID5 hardware models are expressed as state machines that compute and transition to a next state, and only hardware modeling aspects were used for the pipelined-microprocessor verification. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] Burch-Dill verification required projection of PIPE architectural state into SEQ using a proj_impl signal before one step of SEQ operation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] Burch-Dill verification required a pipeline flushing mechanism implemented with force_flush and decode-stage bubble injection until the pipeline is empty. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] Correct flushing should not stall fetch, and the SW variant requires flushing to be disabled for one cycle during popq conversion. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] A pipeline register can initialize, stall, inject a bubble, or load its input on a step. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] Uninterpreted terms and functions support term-level modeling associated with Burch and Dill, with arbitrary but consistent function behavior. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] Processor models form abstraction partial orders; uninterpreted data and functions are more abstract than concrete data and precise mathematical functions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[9] Uninterpreted memory modeling sufficed because the pipelined implementations perform memory operations in program order. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[10] Different pipeline variants require different ALU abstraction precision, from uninterpreted models through partial interpretations to precise arithmetic and bit-vector operations. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[11] Safety-only verification can allow deadlocked or non-progressing processors to pass, so liveness must also be verified to show the pipeline does not stall indefinitely. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5