Sail ISA model of Patmos

This repository will contain a Sail description of the instruction et architecture (ISA) of Patmos.

It is currently a WiP, starting from RISCV sail model.

Directory Structure

sail-patmos
|
+---- model                   // Sail specification modules
|
+---- generated_definitions   // Files generated by Sail
|     |
|     +---- c
|     +---- ocaml
|     +---- lem
|     +---- isabelle
|     +---- coq
|     +---- hol4
|     +---- latex
|
+---- c_emulator              // supporting platform files for C emulator (need to be updated)
+---- ocaml_emulator          // supporting platform files for OCaml emulator (need to be updated)
|
+---- test                    // test files
      |

An outline of the specification

The model contains the following Sail modules in the model directory:

• prelude.sail contains useful Sail library functions

• patmos_types.sail contains some basic Patmos definitions

• patmos.sail captures the instruction definitions (a few currently) and their assembly language formats

• patmos_insts_[begin|end].sail contains the declaration of scattered functions (decode, execute)

• patmos_step.sail contains the fetch and execute functions used by SAIL

• patmos_main.sail guess what, the main function used by SAIL, calling functions from patmos_step.sail file

• more files will come in ...

Building simulators need to be checked later ...