From 898f3c1a2764ee09509a17c715df5a05bb6a0ac3 Mon Sep 17 00:00:00 2001 From: Michael McLoughlin Date: Sat, 28 Sep 2024 01:46:14 -0400 Subject: [PATCH] doc: document aslp installation and use (#80) Document how to install and run the ASLp tooling. --- cranelift/isle/veri/README.md | 40 +++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/cranelift/isle/veri/README.md b/cranelift/isle/veri/README.md index c92b9fa06543..185b76a72888 100644 --- a/cranelift/isle/veri/README.md +++ b/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 ``` + +## 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 `. +3. Ensure ASLp tools are available by adding `/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.