Overview

The VAMP SML executable model is ML/SML code generated for the VAMP processor. The cited case study presents it as an SML structure VAMP signature containing datatypes for numeric representations, sets, and instructions, plus functions for arithmetic, data conversion, and instruction execution.^[1]

Interface elements

The shown signature includes:

structure VAMP : sig
  datatype num = One | Bit0 of num | Bit1 of num
  datatype 'a set = Set of 'a list | Coset of 'a list
  datatype instr = Ilb of IntInf.int * IntInf.int * IntInf.int |
     ...
     Ijr of IntInf.int | Itrap of IntInf.int | Irfe
  val int_add : IntInf.int -> IntInf.int -> IntInf.int
  val int_sub : IntInf.int -> IntInf.int -> IntInf.int
  val cell2data : IntInf.int -> IntInf.int
  val exec_instr : unit aSMcore_t_ext -> instr -> unit aSMcore_t_ext
  val sigma_0 : unit aSMcore_t_ext
  val execInstrs : unit aSMcore_t_ext -> instr list -> unit aSMcore_t_ext
  ...
end

The instr datatype is described as generated from the instruction type definition introduced earlier in the case study, while function definitions are generated from corresponding constants and functions in the model.^[2]

Use in test-program generation

In the case study, HOL-TestGen generated two test scripts targeting load/store sequences and arithmetic operation sequences. For each category, 585 test cases were generated and transformed into executable testers. When those tests were run against the same executable model used for generation, they did not reveal errors.^[3]

Mutation experiment

To evaluate the generated tests, the authors created a mutant executable model by changing three operations in the generated SML code: int_add, int_sub, and cell2data.^[4]

Reported results for the mutant were:

The case study states that, with these mutations, a majority of tests detected the introduced errors; the detailed reported counts show particularly high failure detection for the load/store test set.^[5]

Role in the verification and testing workflow

The executable model is part of an approach that reuses existing verification models for model-based test generation rather than relying on independently developed dedicated test models. The paper contrasts this integration with other test-program generation approaches that use separate test models.^[6]

^[1]: See citation "VAMP SML API". ^[2]: See citation "Generated instruction and function definitions". ^[3]: See citation "Baseline HOL-TestGen execution". ^[4]: See citation "Mutant model changes". ^[5]: See citation "Mutation experiment results". ^[6]: See citation "Reuse of verification models".