Skip to content
STIMSMITH

Abstraction Function

Concept WIKI v1 · 5/25/2026

An abstraction function, in the cited Burch-Dill microprocessor-verification setting, is a mapping α from implementation-level microprocessor states to architectural states. It is required to be preserved by each processor cycle and can be computed automatically by symbolic simulation while flushing the pipeline.

Definition

In Burch-Dill-style microprocessor verification, an abstraction function (\alpha) maps states of a microprocessor implementation to architectural states. The verification obligation is to prove that this mapping is maintained by each cycle of processor operation. [C2]

Role in microprocessor verification

The architectural target is an ISA model: a sequential specification that describes the effect of each instruction on architectural state, including registers, the program counter, and memory. [C1] Pipelined implementations overlap multiple instructions, so formal verification must show that the pipelined execution faithfully implements the sequential ISA semantics for all possible instruction sequences. [C1]

Within this setting, the abstraction function provides the bridge between the implementation state of the pipeline and the architectural state of the sequential ISA model. Burch and Dill's approach requires proving that such a function exists and is preserved across processor cycles. [C2]

Automatic computation by flushing

A key contribution attributed to Burch and Dill is that the abstraction function can be computed automatically by symbolically simulating the microprocessor as it flushes instructions out of the pipeline. [C3] The evidence notes that many pipelined processors already include mechanisms for flushing instructions, because flushing is needed to bring the pipeline to a quiescent state for exceptional conditions such as halting or interrupt handling. [C3]

For a single-issue microprocessor, this leads to a correspondence-checking proof structure: compare two symbolic simulations, one in which the pipeline is flushed and then a single instruction is executed in the ISA model, and another in which the pipeline runs for one normal cycle and then flushes. [C4]

Relationship to abstraction in modeling

The same source describes Burch and Dill's broader use of abstraction in verification. Instead of requiring precise bit-level models, their method uses term-level modeling, in which data representations and operations are abstracted as symbolic terms and units such as decoders and ALUs can be represented by uninterpreted functions. [C5] These abstractions allow verification to focus on pipeline control logic. [C5]

Verification scope

Burch-Dill verification establishes a safety property: every cycle of processor operation has an effect consistent with some number (k) of ISA-model steps, including (k = 0), where a cycle makes no program progress. [C6] The source also notes that this safety result alone does not rule out deadlock; liveness must additionally be verified to show that the processor cannot remain forever without making progress. [C6]

LINKED ENTITIES

1 links
Burch-Dill Correspondence Checking USES

CITATIONS

6 sources
6 citations
[1] C1: An ISA model describes the effect of each instruction on architectural state, including registers, the program counter, and memory, and pipelined verification checks faithful implementation of sequential ISA semantics. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] C2: Burch and Dill's approach requires proving that an abstraction function α maps microprocessor states to architectural states and is maintained by each cycle of processor operation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] C3: Burch and Dill showed that the abstraction function can be computed automatically by symbolically simulating the microprocessor as it flushes the pipeline. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] C4: For a single-issue microprocessor, correspondence checking compares a flush-then-ISA-step simulation with a normal-cycle-then-flush simulation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] C5: Burch and Dill used term-level modeling and uninterpreted functions to abstract data representations, operations, and implementation parameters so verification could focus on pipeline control logic. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] C6: Burch-Dill verification proves a safety property that each processor cycle corresponds to some number k of ISA steps, including k = 0, but liveness must also be verified to rule out non-progress or deadlock. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5