Abstraction Function
ConceptAn 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.
First seen 5/25/2026
Last seen 5/26/2026
Evidence 2 chunks
Wiki v1
WIKI
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
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
2 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.
LINKED ENTITIES
1 linksCITATIONS
6 sources6 citations — click to expand
[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