Skip to content
STIMSMITH

Burch

Person WIKI v1 · 5/25/2026

Burch is referenced in formal microprocessor verification for work with Dill in 1994 that introduced key ideas behind correspondence checking for pipelined processor designs, including automatic computation of an abstraction function by symbolic pipeline flushing.

Overview

Burch is cited together with Dill as the source of key ideas used in formal verification of pipelined microprocessors. The cited 1994 approach requires proving an abstraction function, α, that maps microprocessor states to architectural states and is maintained across each processor cycle. [C1]

Role in pipelined processor verification

The verification setting described in the evidence compares a pipelined implementation against an instruction set architecture (ISA) model. The ISA model specifies architectural state—registers, the program counter, and memory—under a strictly sequential execution semantics. Formal verification must show that, for any instruction sequence, the pipelined processor obtains the same result as a purely sequential ISA implementation. [C2]

Burch and Dill's key contribution was showing that the abstraction function could be computed automatically by symbolically simulating the microprocessor as it flushes instructions from the pipeline. For a single-issue microprocessor, the resulting verification task is to prove equivalence between two symbolic simulations: one that flushes the pipeline and then executes one ISA instruction, and another that executes one normal pipeline cycle and then flushes. The source identifies this approach as correspondence checking. [C3]

Abstraction and term-level modeling

The evidence credits Burch and Dill with demonstrating the value of data abstractions for microprocessor verification through term-level modeling. In this style, implementation details such as data representations and operations are abstracted as symbolic terms, and components such as instruction decoders and ALUs may be modeled as uninterpreted functions. The evidence states that Burch and Dill were the first to show the use of these abstractions in an automated microprocessor verification tool. [C4]

Scope and limitation of Burch-Dill verification

Burch-Dill verification proves a safety property: every processor cycle has an effect consistent with some number of ISA-model steps, including zero steps. This accommodates stalls and canceled instructions, but it also means that a deadlocked processor—or one that does nothing—could pass the safety check. The evidence therefore notes that liveness must also be verified to rule out non-progressing states. [C5]

Related concept

  • [[Burch-Dill Correspondence Checking]]

LINKED ENTITIES

1 links
Burch-Dill Correspondence Checking PROPOSED

CITATIONS

5 sources
5 citations
[1] C1: Burch and Dill's 1994 approach requires an abstraction function α mapping microprocessor states to architectural states and maintaining that mapping across processor cycles. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] C2: Formal pipelined microprocessor verification compares pipelined execution with a sequential ISA model whose architectural state includes registers, the program counter, and memory. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] C3: Burch and Dill's key contribution was automatic computation of the abstraction function by symbolic simulation during pipeline flushing, yielding the equivalence-checking approach called correspondence checking. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] C4: Burch and Dill demonstrated the value of data abstractions and term-level modeling in automated microprocessor verification, including symbolic terms and uninterpreted functions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] C5: Burch-Dill verification proves safety but not liveness, because cycles may correspond to zero ISA steps and a deadlocked or inactive processor could still pass the safety verification. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5