Burch-Dill Correspondence Checking

Technique

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.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 7 chunks

Wiki v1

WIKI

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.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

8 connections

Pipeline Flushing uses → 100% 2e

Burch-Dill verification computes the abstraction function by symbolically simulating the processor as it flushes instructions out of the pipeline.

ALU Abstraction Modeling ← part of 90% 2e

Different levels of ALU abstraction are required for verifying different variants of PIPE in Burch-Dill verification.

Abstraction Function uses → 100% 2e

Burch-Dill verification requires proving that an abstraction function mapping pipeline states to architectural states is maintained.

Symbolic Simulation uses → 100% 2e

Burch-Dill verification involves proving equivalence of two symbolic simulations of the processor.

formal verification ← uses 100% 1e

Burch-Dill correspondence checking is a key technique used in formal microprocessor verification.

Term-Level Modeling uses → 100% 1e

Burch and Dill demonstrated the value of term-level modeling for microprocessor verification.

UCLID5 Verification Condition (correspondence invariant) ← implements 100% 1e

The UCLID5 verification condition expresses the Burch-Dill correspondence invariant between PIPE and SEQ.

UCLID5 ← implements 100% 1e

UCLID5's verification script carries out Burch-Dill correspondence checking for pipelined microprocessors.

LINKED ENTITIES

1 links

UCLID5 implemented_with The evidence states that UCLID5 provides the modeling and command language used to describe the combined system and the script for Burch-Dill correspondence checking.

CITATIONS

11 sources

11 citations — click to expand

[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