Overview

VerisoftXT was a German research project cited alongside the Verisoft project in work on formally verified computer systems. In a 2013 case study on test-program generation for a microprocessor, the authors state that the Verified Architecture Microprocessor (VAMP) and the VAMOS micro-kernel were developed and verified in the context of the German research projects Verisoft and VerisoftXT.

Technical context

The cited case study situates VerisoftXT in a line of research concerned with pervasive formal verification of system artifacts. The source describes Verisoft, in particular, as aiming at formal verification from the application level down to silicon hardware design, and it presents the Verisoft architecture as layered into application software, system software, tools, and hardware.

Within that setting, VAMP is described as a pipelined reduced instruction set (RISC) processor based on out-of-order execution. The assembly-level model, VAMPasm, is described as the instruction-set level of VAMP and includes 56 instructions across memory transfer, constant transfer, register transfer, arithmetic and logical operations, test operations, shifts, control operations, and interrupt handling.

Relationship to testing and verification tooling

The same case study uses the VAMP instruction-set model for model-based generation of test programs. It describes tests generated from a formal model of the instruction set to check conformance between the gate-level implementation and the assembly-level model. The paper also notes that the Verisoft project developed formal models for both the processor and a small operating system in Isabelle/HOL, and that HOL-TestGen can reuse such Isabelle/HOL models for generating test sequences.