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))$$

where (\operatorname{Stall}) is the implementation's transition function when the stall input is asserted, (l) is the number of stall cycles sufficient to flush all partially executed instructions out of the pipeline, and (\operatorname{Proj}) strips away all but the user-visible state (registers, program counter, memory). [C2, C4] In the Y86-64/UCLID5 formulation the same intuition is stated as: (\alpha(P_0) = S), where (P_0) is a pipeline state and (S) is the architectural state that results when all partially executed instructions are executed. [C5]

The verification obligation is to show that this mapping is preserved by each cycle of processor operation, i.e. that the pipelined implementation and a sequential ISA specification remain consistent under (\alpha). [C2, C4]

In industrial practice (e.g., ARM's ISA-Formal), the abstraction function is written in a hardware description language such as SystemVerilog and is responsible for converting the micro-architectural state of the processor into an architectural state. For an in-order pipeline that commits results in a single pipeline stage, the state before an instruction executes can typically be obtained by reading the state at the end of the writeback stage and the state after by reading from the end of the Mem stage, with the relevant opcode propagated by a pipeline follower. [C7]

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. [C3]

Commutative-diagram correctness criterion

The correctness criterion for a pipeline implementation (\delta_I) and an ISA specification (\delta_S) is expressed by a commutative diagram involving (\alpha):

$$\forall \vec{x}, \vec{u}, \vec{p}.; \alpha(\delta_I(\vec{x}, \langle \vec{u}, \vec{p}\rangle)) ;=; \delta_S(\vec{x}, \alpha(\langle \vec{u}, \vec{p}\rangle))$$

That is, taking an implementation step and then abstracting must equal first abstracting and then taking a specification step. [C4, C6]

When symbolic ternary simulation is used, the criterion is weakened to the bit-level (\subseteq) ordering of the symbolic domain, allowing the implementation side to be no more general than the specification side without producing false positives (although false negatives remain possible). [C4, C6]

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, C6] Starting from a general symbolic initial state (Q_{\text{Impl}}), one simulates a flush of the pipeline by stalling it for a sufficient number of cycles to allow all partially executed instructions to complete, and then takes the resulting user-visible state (register file, program counter, etc.) as the matching specification state (Q_{\text{Spec}}). [C6] 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 that compares two symbolic simulations:

• (\sigma_a): (\operatorname{Init}(P_0)), (\operatorname{Pipe}), (\operatorname{Flush}(n)), (\operatorname{SaveAP}(S^a)) — capturing the effect of one step of PIPE followed by the abstraction function. [C5]
• (\sigma_b): (\operatorname{Init}(P_0)), (\operatorname{Flush}(n)), (\operatorname{Xfer}), (\operatorname{SaveS}(S_0^b)), (\operatorname{Seq}), (\operatorname{SaveS}(S_1^b)) — capturing the effect of the abstraction function followed by one step of SEQ. [C5]

The state values in these two sequences correspond, in terms of (\alpha), to:

$$S^a = \alpha(\operatorname{Pipe}(P_0)), \quad S_0^b = \alpha(P_0), \quad S_1^b = \operatorname{Seq}(\alpha(P_0))$$

and the correspondence condition is (S^a = S_1^b \lor S^a = S_0^b). [C5] The disjunct (S^a = S_1^b) holds when the instruction fetched during the PIPE step eventually completes and so should match a SEQ step; the disjunct (S^a = S_0^b) holds when the PIPE cycle either stalls or fetches an instruction that is later canceled (e.g., due to a mispredicted branch), in which case the cycle should have no effect on architectural state. [C5]

Pipeline followers

Because information needed by the abstraction function (such as the current opcode) is normally discarded shortly after instruction decode and is not available at the point where an instruction commits, an abstraction function is typically accompanied by a pipeline follower: logic that copies the needed signal from one pipeline stage to the next and implements the same pipeline stall/flush logic as the datapath. This is similar in spirit to the introduction of "ghost state" by Lahiri et al. [C7]

For a dual-issue pipeline, where two consecutive instructions are decoded and executed in parallel, a further abstraction function is added to extract the intermediate state between execution of the two instructions. A practical approach is to use a single copy of the specification logic and insert multiplexors to select which pre/post state is used with the specification, rather than instantiating two copies of the specification (which scales poorly beyond dual issue). A subtler problem arises when the second instruction can suppress part of the behaviour of the first (e.g., both instructions modifying the carry flag, with the second's value being the one finally written): in such cases the carry flag value from the first instruction may not be available at writeback, and the correct signal must be identified and propagated down to the point of serialization by an additional pipeline follower. An incorrect choice of signal is detected when that signal is used as part of the pre-state of the second instruction. [C8]

Extensions in industrial practice (ISA-Formal)

In ARM's ISA-Formal framework, abstraction functions are written by hand in SystemVerilog and are responsible for converting the micro-architectural processor state into an architectural state. The instruction-level specification is typically a short piece of purely combinational logic, with SystemVerilog assertions checking that the abstracted result matches the result of the specification when the corresponding instruction retires. [C7]

Several real-world processor features require extending the basic single-issue, in-order, no-fusion abstraction:

• Out-of-order completion. Slow instructions such as loads may complete after later instructions. The reported approach takes a snapshot of the pre-state when the load retires, updates the snapshot as each micro-op for the instruction completes, and uses the final post-state when the last micro-op completes to check against the architecture specification. [C9]
• Instruction fusion. When consecutive instructions are fused into a single macro-operation, intermediate results overwritten by the second instruction may never be computed by the processor. The reported approach is to add additional verification logic to calculate the missing intermediate state, whose correctness is justified when checking that all uses of the first instruction are correct and that the fused pair gives the correct overall result. [C7]
• Register renaming and out-of-order issue. With a rename table and reorder buffer, there is a single clearly identified point of serialization implemented in the reorder buffer, which makes applying ISA-Formal to out-of-order processors in some respects simpler than to in-order processors. In-order processors instead use a variety of scattered mechanisms (varying pipeline length, supporting out-of-order completion of slow instructions) that are harder to handle uniformly. [C10]
• Hand-written abstract functions on functional units. When a functional unit's full behaviour is too complex to specify in full, the processor itself can be used as an oracle: logic tracks the inputs and outputs of the unit and supplies the output value to the architectural specification whenever its inputs match the unit's actual inputs. This cannot detect errors in the trusted unit but can detect errors in the surrounding control and forwarding logic. The same idea covers interface properties (substituting a sufficiently strong interface specification for the actual component) and subset behaviour checking (restricting checks to a chosen subset of inputs). [C11]

Debugging hand-written abstraction functions is reported to be considerably easier using hand-written instruction properties for representative instructions than using a mechanically translated specification; once the abstraction function has been debugged, the framework can be switched over to using machine-generated specifications. [C12]

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. [C3] These abstractions allow verification to focus on pipeline control logic. [C3] Their use of uninterpreted functions with equality also allows 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. [C6]

Origins in Hoare's methodology

The correctness criterion expressed by the commutative diagram and the underlying abstraction function is not new to hardware verification. It 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, with Burch and Dill's method being the canonical instance in microprocessor verification. [C6] More recently, Hoare's methodology has been given a synthetic account in univalent dependent type theory, in which the data of an abstraction function are encoded within types themselves via a phase distinction, yielding a gluing construction that renders an abstraction function as a type together with a pair of modalities fracturing a type into its concrete and abstract parts. [C13] This type-theoretic reformulation scales to cost verification through a monadic sealing effect that allows an implementation to be upper-bounded by its specification even when private details influence observable cost. [C13]

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. 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.