Abstraction Function

Concept

An abstraction function α maps the implementation-level state of a pipelined microprocessor to its architectural (user-visible) state, providing the bridge that makes correspondence checking between an ISA specification and a pipeline implementation possible. In the Burch and Dill method, α is computed automatically by symbolically simulating the pipeline as it flushes partially executed instructions, and the verification obligation is that each pipeline cycle of the implementation correspond, under α, to zero or more ISA-level steps of the specification. The idea generalizes Hoare's methodology for relating concrete implementations to abstract specifications.

First seen 5/25/2026

Last seen 6/18/2026

Evidence 5 chunks

Wiki v2

WIKI

Definition

In Burch–Dill-style microprocessor verification, an abstraction function (\alpha) maps the combined user-visible and pipeline state of an implementation, written (\langle \vec{u}, \vec{p} \rangle), to the user-visible (architectural) state of the implementation. Concretely, Bryant and colleagues define:

$$\alpha(\langle \vec{u}, \vec{p} \rangle) ;\dot{=}; \operatorname{Proj}(\operatorname{Stall}^{l}(\langle \vec{u}, \vec{p} \rangle))$$

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

3 connections

Burch-Dill Correspondence Checking ← uses 100% 2e

Burch-Dill verification requires proving that an abstraction function mapping pipeline states to architectural states is maintained.

Pipeline Flushing uses → 100% 2e

The abstraction function is computed by flushing instructions from the pipeline during symbolic simulation.

Burch and Dill Pipeline Verification Method ← uses 100% 2e

Burch and Dill's method uses an abstraction function to map pipeline state to user-visible state.

LINKED ENTITIES

1 links

Burch and Dill Pipeline Verification Method USES Extracted graph relationship

CITATIONS

9 sources

9 citations — click to expand

[1] The abstraction function α maps the combined user-visible and pipeline state ⟨u⃗, p⃗⟩ of the implementation to its user-visible state by stalling the pipeline for l cycles to flush partially executed instructions and then projecting away non-user-visible state: α(⟨u⃗, p⃗⟩) = Proj(Stall^l(⟨u⃗, p⃗⟩)). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[2] The commutative-diagram correctness criterion is: ∀ x⃗, u⃗, p⃗. α(δ_I(x⃗, ⟨u⃗, p⃗⟩)) = δ_S(x⃗, α(⟨u⃗, p⃗⟩)). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[3] The Burch and Dill approach uses symbolic simulation of the hardware design to automatically compute an abstraction function by starting from a symbolic initial pipeline state Q_Impl, stalling (flushing) the pipeline for a sufficient number of cycles to complete partially executed instructions, and taking the resulting user-visible state as the matching specification state Q_Spec. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[4] Burch and Dill use uninterpreted functions with equality to introduce a single symbolic variable denoting the initial state of an entire memory array, with each Write or Read operation building a formula over the current memory state. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[5] In the Y86-64/UCLID5 formulation, α(P₀) = S maps a pipeline state to the architectural state that results when all partially executed instructions are executed, and correspondence checking compares two sequences σ_a = Init(P₀), Pipe, Flush(n), SaveAP(S^a) and σ_b = Init(P₀), Flush(n), Xfer, SaveS(S₀^b), Seq, SaveS(S₁^b), requiring S^a = S₁^b ∨ S^a = S₀^b. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5

[6] With symbolic ternary simulation, the Burch–Dill correctness criterion weakens to bit-level ⊆ containment: Abs(δ_I(x⃗, ⟨u⃗, p⃗⟩)) ⊆ Abs(⟨u⃗, p⃗⟩)), so that the ternary EMM is a conservative approximation (no false positives, possible false negatives). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[7] The correctness criterion expressed by the commutative diagram and underlying abstraction function was introduced by Hoare for verifying computations on abstract data types in software and has been reused by Bose and Fisher to verify pipelined circuits. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[8] Hoare's methodology using abstraction functions to demonstrate coherence between concrete implementations and abstract specifications can be given a synthetic account in univalent dependent type theory by encoding abstraction functions within types themselves, via a phase distinction that yields a gluing construction and a pair of modalities fracturing a type into concrete and abstract parts; this approach also supports modular cost verification through a monadic sealing effect. Abstraction Functions as Types

[9] An abstraction function is a mapping from implementation-level microprocessor states to architectural states; it must be preserved by each processor cycle and can be computed automatically by symbolic simulation during a pipeline flush. Previous wiki article (Abstraction Function, v1)