Dill

Person

Dill is cited, together with Burch, for 1994 ideas that became central to formal verification of pipelined microprocessors, including automatic computation of an abstraction function by symbolic pipeline flushing and the approach later described as correspondence checking.

First seen 5/25/2026

Last seen 6/5/2026

Evidence 2 chunks

Wiki v1

WIKI

Overview

Dill is referenced in the context of formal verification of pipelined microprocessors as a coauthor, with Burch, of 1994 ideas that influenced later verification work. The cited approach requires proving an abstraction function, α, from microprocessor states to architectural states, and showing that this mapping is maintained by each processor cycle. Its key contribution was that the abstraction function could be computed automatically by symbolically simulating the processor while flushing instructions out of the pipeline. [C1]

Role in correspondence checking

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

LINKED ENTITIES

1 links

Burch-Dill Correspondence Checking PROPOSED Extracted graph relationship

CITATIONS

4 sources

4 citations — click to collapse

[1] Dill, together with Burch, is associated with 1994 ideas requiring an abstraction function from microprocessor states to architectural states and automatic computation of that function by symbolic pipeline flushing. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[2] For a single-issue microprocessor, the Burch-and-Dill approach checks equivalence between flushing-then-ISA-execution and normal-cycle-then-flushing symbolic simulations, and the source calls this correspondence checking. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[3] Burch and Dill demonstrated term-level data abstraction for automated microprocessor verification, using symbolic terms and uninterpreted functions, and were first to show such abstractions in an automated microprocessor verification tool. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[4] Burch-Dill verification proves safety by showing each processor cycle is consistent with some number of ISA-model steps, but it does not by itself prove liveness. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5