Skip to content
STIMSMITH

Abstract Functions (Oracle-based Verification)

Concept WIKI v1 · 8/18/2026

Abstract functions are an oracle-based verification technique used within the ISA-Formal framework for end-to-end verification of ARM processors. They handle gaps in generated Verilog at functional-unit interfaces by treating the processor itself as the oracle, allowing detection of bugs in surrounding control and forwarding logic even when the unit under verification cannot itself be fully checked.

Abstract Functions (Oracle-based Verification)

Abstract functions are one of three approaches used to fill gaps left in generated Verilog at the interfaces between ISA-specified partitions and other parts of a processor design (such as the memory system, floating-point units, or exception/address-translation logic) when verifying ARM processors with ISA-Formal. Where the generated Verilog for the "Instruction Set Architecture" partition omits functions at call boundaries, abstract functions provide an oracle-based strategy for the remaining unfilled interfaces (cfd57488).

Motivation

When the ISA specification is partitioned along function-call boundaries into parts such as "Instruction Set Architecture," "Floating Point," "Exception," and "Address Translation," Verilog is only generated for the ISA part. Hand-written shims of a few lines bridge the other interfaces, but this leaves parts of the processor un-checked by ISA-Formal. The authors therefore track which parts of the processor are not checked by ISA-Formal and ensure that an alternative verification technique covers those parts. Abstract functions are one such alternative, complementing interface properties and subset behaviour checking (cfd57488).

Mechanism

The technique works by adding logic that tracks the inputs and outputs from some functional unit in the processor. The processor itself is then used as an oracle:

  1. Auxiliary logic observes the actual inputs supplied to a functional unit during simulation and records the corresponding outputs produced by that unit.
  2. If the inputs of a function in the architectural specification match the actual inputs observed for a functional unit in the processor, the recorded oracle output is used as the expected value for that function in the specification.

Because the behaviour of the chosen unit is trusted by construction, abstract functions cannot detect bugs inside the unit itself. However, they can detect bugs in the surrounding control and forwarding logic that route values into and out of the unit, since mismatches between the recorded oracle behaviour and the architectural expectation will surface during checking (cfd57488).

Relationship to the Other Interface Strategies

  • Interface properties are used when an existing interface specification is already strong enough — for example, the memory system, where an architectural-to-microarchitectural translator of requests and responses suffices (cfd57488).
  • Subset behaviour checking is used when the full behaviour of a unit is too complex to specify but a restricted subset is tractable — for example, restricting floating-point inputs to ±{0, 1, ∞, S-NaN, Q-NaN}. A separate signal indicates whether the inputs are in the supported subset so that this restriction only affects checks of values written to floating-point registers and not other ISA-Formal checks (condition flags, exceptions, memory accesses, register writes) (cfd57488).
  • Abstract functions are the fallback used when neither of the above is sufficient, leveraging the processor itself as the oracle (cfd57488).

Trade-offs

  • Strengths: Catches errors in control logic and forwarding around the unit; does not require a complete formal specification of the unit.
  • Limitations: Cannot detect bugs inside the trusted functional unit, so it must be paired with other verification techniques that cover the unit itself.

Use in Context

In the broader end-to-end verification effort described in the CAV 2016 paper, abstract functions are part of the toolbox that allows ISA-Formal to be applied to realistic, partitioned ARM processor designs — including out-of-order completing cores, where constructing an accurate post-state is complicated by instructions such as loads being split into multiple micro-ops that complete independently. The paper proposes taking a snapshot of the pre-state when such an instruction retires and updating the snapshot as each micro-op completes (cfd57488). This style of state tracking is conceptually aligned with the input/output observation performed by abstract functions.

LINKED ENTITIES

1 links
ISA-Formal USES

CITATIONS

7 sources
7 citations
[1] Abstract functions are one of three approaches used to fill gaps in generated Verilog at the interfaces between the ISA partition and other parts of the processor when verifying ARM processors with ISA-Formal. End-to-End Verification of ARM Processors
[2] Abstract functions add logic to track the inputs and outputs from a functional unit and use the processor as an oracle: when the inputs of an architectural-specification function match the actual inputs of a functional unit in the processor, the recorded oracle output is used as the expected value. End-to-End Verification of ARM Processors
[3] Because the behaviour of the chosen functional unit is trusted, abstract functions cannot detect bugs inside the unit itself but can detect bugs in the surrounding control and forwarding logic. End-to-End Verification of ARM Processors
[4] The authors track which parts of the processor are not checked by ISA-Formal and ensure that an alternative verification technique is applied to those parts, of which abstract functions is one option alongside interface properties and subset behaviour checking. End-to-End Verification of ARM Processors
[5] Interface properties are used where existing interface specifications are strong enough (e.g., the memory system), and subset behaviour checking is used where a restricted input subset makes the unit tractable (e.g., floating-point inputs restricted to ±{0, 1, ∞, S-NaN, Q-NaN}). End-to-End Verification of ARM Processors
[6] For subset behaviour checking, a separate signal indicates whether inputs are in the supported subset so that the restriction only affects checks of values written to floating-point registers and not other ISA-Formal checks (condition flags, exceptions, memory accesses, register writes). End-to-End Verification of ARM Processors
[7] The paper describes handling out-of-order completing instructions (such as loads split into multiple independently completing micro-ops) by taking a snapshot of the pre-state when the instruction retires and updating the snapshot as each micro-op completes. End-to-End Verification of ARM Processors