A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor

Zhe Hou 📧, David Sanan 📧, Alwen Tiu 📧 and Yang Liu 📧

October 19, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Session SPARCv8

Depends on

Cite

× 
@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: