Abstraction Function
ConceptAn 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, and has been extended in industrial practice (ISA-Formal) to handle dual-issue pipelines, instruction fusion, out-of-order completion, register renaming, and the use of hand-written abstract functions on functional units whose full behavior is too complex to specify.
First seen 5/25/2026
Last seen 8/18/2026
Evidence 9 chunks
Wiki v3
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))$$
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
5 connectionsBurch-Dill verification requires proving that an abstraction function mapping pipeline states to architectural states is maintained.
The abstraction function is computed by flushing instructions from the pipeline during symbolic simulation.
Burch and Dill's method uses an abstraction function to map pipeline state to user-visible state.
ISA-Formal relies on abstraction functions to convert micro-architectural state to architectural state.
The pipeline follower is a component that supports the abstraction function by tracking instruction state.
LINKED ENTITIES
2 linksCITATIONS
13 sources13 citations — click to expand
[1] 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, and 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. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[2] An abstraction function α maps the combined user-visible and pipeline state ⟨û, p̃⟩ to the user-visible state via α(⟨û, p̃⟩) = Proj(Stall^l(⟨û, p̃⟩)), stalling the pipeline for l cycles and then projecting away pipeline state. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[3] The Burch and Dill approach uses an abstraction function to bridge the implementation state of the pipeline and the architectural state of the sequential ISA model, requiring a proof that the function exists and is preserved across processor cycles; their method uses term-level modeling with symbolic terms and uninterpreted functions for decoders and ALUs to focus verification on pipeline control logic. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[4] The correctness criterion is expressed by the commutative diagram α(δ_I(x⃗, ⟨û, p̃⟩)) = δ_S(x⃗, α(⟨û, p̃⟩)); under symbolic ternary simulation the criterion is weakened to the bit-level ⊆ ordering of the symbolic domain, giving a conservative approximation that avoids false positives at the cost of possible false negatives. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[5] In the Y86-64/UCLID5 formulation, α(P₀) = S is the architectural state that results when all partially executed instructions are executed, and correspondence checking is done by comparing two sequences σ_a = Init(P₀), Pipe, Flush(n), SaveAP(Sᵃ) and σ_b = Init(P₀), Flush(n), Xfer, SaveS(S₀ᵇ), Seq, SaveS(S₁ᵇ), yielding the condition Sᵃ = S₁ᵇ ∨ Sᵃ = S₀ᵇ where the right disjunct covers stalls and mispredicted branches. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] Burch and Dill's method computes the abstraction function automatically by symbolically simulating a flush of the pipeline from a general symbolic initial state Q_Impl; many pipelined processors already include such flushing mechanisms for exceptional conditions such as halting or interrupt handling. Uninterpreted functions with equality allow a single symbolic variable to denote the initial state of an entire memory array, with each Write or Read building a formula over the current memory state. The correctness criterion traces back to Hoare for verifying abstract data types in software, with Bose and Fisher applying it to pipelined circuits. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[7] In ARM's ISA-Formal, the abstraction function abs is written by hand in SystemVerilog and converts micro-architectural state into architectural state; for an in-order core that commits results in a single stage, the pre-state is read at the end of the writeback stage and the post-state at the end of the Mem stage. Because the opcode is normally discarded shortly after decode, a pipeline follower copies the opcode from one stage to the next and mirrors the pipeline stall/flush logic, similar to ghost state in Lahiri et al. Instruction-level specifications are typically short combinational pieces of logic asserted to match the abstracted result when the instruction retires, and can detect decoder bugs that affect downstream optimization signals such as instruction-fusion eligibility. End-to-End Verification of ARM Processors
[8] For dual-issue pipelines, a further abstraction function is added to extract the intermediate state between execution of the two instructions; the practical approach uses a single copy of the specification with multiplexors selecting which pre/post state is used, rather than two specification copies. When the second instruction can suppress part of the first (e.g., both modifying the carry flag), the suppressed value may not be available at writeback and must be propagated to the point of serialization by an additional pipeline follower; an incorrect choice is detected when the signal is used as part of the pre-state of the second instruction. End-to-End Verification of ARM Processors
[9] For out-of-order completion of slow instructions such as loads, the reported approach takes a snapshot of the pre-state when the load retires and updates it as each micro-op for the instruction completes, using the final post-state when the last micro-op completes to check against the architecture specification. End-to-End Verification of ARM Processors
[10] Processors with register renaming and a reorder buffer have a single clearly identified point of serialization in the reorder buffer, which makes applying ISA-Formal to out-of-order processors simpler in some respects than to in-order processors, since in-order processors use a variety of scattered mechanisms (varying pipeline length, out-of-order completion of slow instructions) to support limited out-of-order execution. End-to-End Verification of ARM Processors
[11] When a functional unit's full behaviour is too complex to specify in full, the processor can be used as an oracle: logic tracks the unit's inputs and outputs and supplies the output value to the architectural specification whenever its inputs match the unit's actual inputs. This cannot detect errors inside the trusted unit but can detect errors in the surrounding control and forwarding logic. The same idea underlies interface properties (substituting a sufficiently strong interface specification for the actual component) and subset behaviour checking (restricting checks to a chosen subset of inputs, e.g., ±{0,1,∞, S-NaN, Q-NaN} for floating-point units). End-to-End Verification of ARM Processors
[12] Debugging hand-written abstraction functions is significantly easier using hand-written properties for representative instructions than using a mechanically translated specification; once the abstraction functions have been debugged, the framework can switch to using machine-generated specifications almost exclusively. End-to-End Verification of ARM Processors
[13] A recent line of work gives a synthetic account of Hoare's abstraction-function methodology within univalent dependent type theory by encoding the data of an abstraction function inside types via a phase distinction, yielding a gluing construction that renders an abstraction function as a type and a pair of modalities fracturing a type into its concrete and abstract parts; a noninterference theorem governs the phase distinction. The approach scales to verification of cost through a monadic sealing effect that allows an implementation to be upper-bounded by its specification even when private details influence observable cost. Abstraction Functions as Types