diff options
| -rw-r--r-- | README | 10 | ||||
| -rw-r--r-- | mips/README | 23 |
2 files changed, 30 insertions, 3 deletions
@@ -11,7 +11,7 @@ specification language: - sail, the type checker and compiler for programs in the Sail language; -- an example Sail specification of a MIPS processor (in mips/mips.sail) +- an example Sail specification of a MIPS processor (in mips/) - a sequential Sail interpreter, which evaluates an ELF binary for an architecture that has been specified using Sail (for ABIs included @@ -38,8 +38,12 @@ analogy with the existing MIPS definition, using the sail executable just to check that it is type-correct. After building sail (as described below), this is done by: -./sail mips/mips.sail +./sail mips/mips_prelude.sail mips/mips_wrappers.sail mips/mips_insts.sail mips/mips_epilogue.sail +Sail treats multiple file arguments as though they wre concatenated +into a single large file (although error messages will give the +appropriate file and line number). For an explanation of why the MIPS +model is devided up see mips/README. Once sufficient instructions have been represented in a specification, then one may also want to run executables sequentially, to debug the @@ -53,7 +57,7 @@ factored out into external specification files. Building the architecture for compilation to connect to the interpreter, one uses the sail executable: -./sail mips/mips.sail -lem_ast +./sail <sail files...> -lem_ast which will generate a mips.lem file in the current directory, which will be linked with the sail interpreter (the output is a verbose diff --git a/mips/README b/mips/README new file mode 100644 index 00000000..feaebfde --- /dev/null +++ b/mips/README @@ -0,0 +1,23 @@ +This directory contains a MIPS64-style processor written in Sail. To +support integration with the CHERI ISA it is split across several +files, which must be given to sail in the following order: + + 1. mips_prelude.sail contains definitions used in the rest of the + ISA, including register declarations and helper functions, for + example for performing address translation. + + 2. mips_wrappers.sail contains wrappers and hooks around certain + functions. In straight MIPS these are mostly identity functions, but + on CHERI they are substituted for functions which implement + CHERI-specific behaviour. + + 3. mips_insts.sail contains descriptions of instructions in the form + of AST members, decode and execute function clauses (using Sail's + scattered union/function definitions). + + 4. mips_epilogue.sail just closes the function and AST union definitions. + +The CHERI sail model extends this model by adding more declarations in a +file cheri_prelude.sail, included after mips_prelude.sail, replacing +the functions in mips_wrappers.sail and adding new instruction +definitions in cheri_insts.sail. |