Overview

execVAMP is defined in the VAMP microprocessor testing case study as a lifted execution function for VAMP instructions. The paper describes it as “a lifting of exec_instr into the state exception monad” and gives the definition:

definition execVAMP where execVAMP ≡ (λ i σ. Some ((), exec_instr σ i))

In this definition, i is an instruction and σ is the input state. The function returns Some ((), exec_instr σ i), i.e. a successful state-exception-monad result with no meaningful local return value and with the next state computed by exec_instr.

Role in sequence test specifications

The case study uses execVAMP in sequence-oriented test specifications over generated instruction lists ιs :: instr list. The paper distinguishes scenarios that observe local execution steps from scenarios that test the final state; for this application, local steps are not relevant because they are “just actions not reporting a computation result.” Instead, the specifications execute an instruction sequence and then assert a property over the resulting state.

One whole-state conformance pattern is shown as:

test_spec pre ιs::instr list =⇒
  (σ0 |= (_ ← mbind ιs execVAMP;
          assertSE (λσ. σ =k SUT σ0 ιs)))

A more focused pattern compares only register 0 after appending a load instruction:

test_spec pre ιs::instr list =⇒
  (σ0 |= (_ ← mbind (ιs@[load x 0]) execVAMP;
          assertSE (λσ. (gprs σ)!0 = (gprs (SUT σ₀ ιs))!0)))

In both patterns, mbind applies execVAMP across the instruction sequence starting from the initial state σ0, and assertSE checks the final-state property.

Testing context

The same source explains that the test specification preconditions, also called test purposes, restrict generated instruction sequences to a chosen subset. The authors chose an empty initial configuration σ0 for their study and proved it well formed, rather than generating arbitrary initial configurations that might be ill formed in the abstract assembler model.

The testing work is positioned at the design level of the VAMP machine rather than at the available VAMP gate-level model. In the load-store testing example, the test purpose is_load_store restricts instruction generation to load/store operations by syntactic constraints over the VAMP assembly language.