Burch-Dill Correspondence Checking

Concept

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.

First seen 5/25/2026

Last seen 5/25/2026

Evidence 2 chunks

Wiki v1

WIKI

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]

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

LINKED ENTITIES

6 links

Abstraction Function USES Extracted graph relationship

Symbolic Simulation USES Extracted graph relationship

Pipeline Flushing USES Extracted graph relationship

Burch PROPOSED Extracted graph relationship

Dill PROPOSED Extracted graph relationship

Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5 APPLIES Extracted graph relationship

CITATIONS

8 sources

8 citations — click to expand

[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