Some documentation updates

README.md

@@ -1,17 +1,23 @@
-A HOL4 project for hardware/Verilog development
+Verilog development and verification project for HOL4
 
 # Installation and setup
 
-The development requires [HOL4](https://hol-theorem-prover.org) and [L3](http://www.cl.cam.ac.uk/~acjf3/l3). 
+The development requires [HOL4](https://hol-theorem-prover.org).
 
-To build you need to point $CAKEMLDIR to your CakeML compiler directory.
+## Ag32-specific setup
 
-## ISA generation
+To build Ag32-related theories, such as the processor itself and `cakeml_connection`, you need to point `$CAKEMLDIR` to your CakeML compiler directory.
 
-The following command in the L3 REPL (named `l3`, located in the `bin` directory in your L3 directory) will produce ISA HOL code from the ISA specification:
+### ISA generation
+
+Translating the Silver ISA from L3 to HOL is not necessary as the already-translated ISA stored in the CakeML compiler project is used.
+
+However, after updating the L3 ISA the following steps are required to update the HOL ISA.
+
+First, make sure you have [L3](http://www.cl.cam.ac.uk/~acjf3/l3) installed.
+
+With L3 installed, the following command in the L3 REPL (named `l3`, located in the `bin` directory in your L3 directory) will produce the HOL ISA from the L3 ISA:
 
 ```
 HolExport.spec ("ag32.spec", "ag32");
 ```
-
-Doing this is not necessary as the generated ISA stored in the CakeML compiler project is used.

regexp/compilation/regexpExampleVerilogPrintLib.sml

@@ -30,6 +30,8 @@ fun toVerilogListInit name l =
  l
  |> mapi (fn i => fn e => name ^ "[" ^ (Int.toString i) ^ "] = " ^ e);
 
+regexp_res here is from regexpExampleScript.sml:
+
  regexp_res
  |> #final
  |> vectorToList

verilog_glue/README.md

@@ -1 +1,5 @@
+Some glue code use to integrate the Silver processor with our FPGA board.
+
+The cache layer is currently unused.
+
 The nonsense "_wrapper" files are only needed because Vivado do not allow SystemVerilog at the top-level in the block integrator.