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

For a single-issue microprocessor, the Burch-and-Dill approach reduces verification to checking equivalence between two symbolic simulations: one in which the pipeline is flushed and then a single ISA instruction is executed, and another in which the pipeline first performs a normal cycle and then flushes. The evidence identifies this verification approach as correspondence checking. [C2]

Use of abstraction

The evidence also credits Burch and Dill with demonstrating the value of data abstractions in automated microprocessor verification. Their method used term-level modeling, in which data values are treated as symbolic terms and units such as instruction decoders and ALUs can be abstracted as uninterpreted functions. The source states that Burch and Dill were the first to show the use of these abstractions in an automated microprocessor verification tool. [C3]

Scope and limitation of Burch-Dill verification

Burch-Dill verification proves a safety property for a pipelined processor design: each processor cycle has an effect consistent with some number of ISA-model steps, including the case of zero progress. The source notes that this means a deadlocked processor, or even a device that does nothing, can pass this safety verification unless liveness is also verified. [C4]

Related concept

• [[Burch-Dill Correspondence Checking]]: Dill is linked to this concept through the Burch-and-Dill verification approach described above.