### Abstract

We formalise the SPARCv8 instruction set architecture (ISA) which is used in processors such as LEON3. Our formalisation can be specialised to any SPARCv8 CPU, here we use LEON3 as a running example. Our model covers the operational semantics for all the instructions in the integer unit of the SPARCv8 architecture and it supports Isabelle code export, which effectively turns the Isabelle model into a SPARCv8 CPU simulator. We prove the language-based non-interference property for the LEON3 processor. Our model is based on deterministic monad, which is a modified version of the non-deterministic monad from NICTA/l4v.

### License

BSD License

### Topics

- Computer science/Security
- Computer science/Hardware

### Session SPARCv8

- WordDecl
- Sparc_Types
- Lib
- DetMonad
- DetMonadLemmas
- RegistersOps
- MMU
- Sparc_State
- Sparc_Instruction
- Sparc_Execution
- Sparc_Properties
- Sparc_Init_State
- Sparc_Code_Gen

### Depends on

- Finite Machine Word Library

## Cite

×

SPARCv8-AFP

    @article{SPARCv8-AFP,
      author  = {Zhe Hou and David Sanan and Alwen Tiu and Yang Liu},
      title   = {A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/SPARCv8.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Oct 19, 2016 : Isabelle2016