doc: document aslp installation and use (avanhatt#80)

Document how to install and run the ASLp tooling.

cranelift/isle/veri/README.md

@@ -44,3 +44,43 @@ following command can be used to limit to all expansions that involve named rule
 ```
 ./script/veri.sh -- --rule <rule>
 ```
+
+## ISA Specifications
+
+Where possible we derive ISA specifications in VeriISLE format from
+authoritative specifications distributed by vendors. Currently this is only
+possible for the AArch64 backend, with specifications derived from ARM's Machine
+Readable Specification in Architecture Specification Language (ASL). We rely on
+the [ASLp](https://github.com/UQ-PAC/aslp) tool to assist with distilling down
+the original verbose specifications to usable semantics for verification.
+
+The resulting ISA specifications are checked in to the repository, so there is
+no requirement to install ASLp unless you want to alter existing or derive more
+specifications with it.
+
+### Generating ISA Specifications
+
+To run ISA specification generation, you will first need to install ASLp:
+
+1.  [Install `opam`](https://opam.ocaml.org/doc/Install.html), the OCaml Package
+    Manager. The "Binary distribution" method is recommended.
+2.  Install ASLp with `./veri/script/install/aslp.sh -i <aslp_install_path>`.
+3.  Ensure ASLp tools are available by adding `<aslp_install_path>/bin` to your
+    `PATH`.
+
+To run ISA specification generation, from the `isaspec` directory run:
+
+```
+./script/generate.sh -l
+```
+
+This will:
+
+1.  Launch an instance of the `aslp-server`. Communicating with ASLp over a
+    server connection allows us to pay the initialization cost of reading the
+    large ASL specification once.
+2.  Build and execute the `isaspec` tool.
+3.  Write outputs to the `cranelift/codegen/src/isa/aarch64/spec/` directory.
+
+On a clean checkout this should be a no-op, and in fact we have CI tests that
+verify this.