An executable formalisation of the SPARCv8 instruction set architecture: A case study for the LEON3 processor

Abstract

The SPARCv8 instruction set architecture (ISA) has been used in various processors for workstations, embedded systems, and space missions. However, there are no publicly available formal models for the SPARCv8 ISA. In this work, we give the first formal model for the integer unit of SPARCv8 ISA in Isabelle/HOL. We capture the operational semantics of the instructions using monadic definitions. Our model is a detailed model, which covers many features specific to SPARC processors, such as delayed-write for control registers, windowed general registers, and more complex memory access. Our model is also general, as we retain an abstract layer of the model which allows it to be instantiated to support all SPARCv8 compliant processors. We extract executable code from our formalisation, giving us the first systematically verified executable semantics for the SPARCv8 ISA. We have tested our model extensively against a LEON3 simulation board, covering both singlestep executions and sequential execution of programs. We prove some important properties for our formal model, including a non-interference property for the LEON3 processor.