Add README in mips directory describing file breakdown and remove reference to non-existent mips.sail in top level README.

2 files changed, 30 insertions, 3 deletions

diff --git a/README b/README
index a2c29c6b..5f43dcd7 100644
--- a/README
+++ b/README
@@ -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.