L3 Specification of the RISC-V ISA
----------------------------------

For more on RISC-V, see http://riscv.org.

This L3 specification can be used to generate an executable interpreter of
RISC-V binaries, similar to the Spike simulator for RISC-V.

It can also be used to generate a machine-readable specification in a simple
sexpr-based syntax.

Dependencies
------------

This model needs a recent Poly/ML compiler (at least version 5.7.2 if released,
or built from the latest source at github.com/polyml), and L3 itself.

L3 is available from: http://www.cl.cam.ac.uk/~acjf3/l3
Ensure that you are using a recent version (L3-2018-02-09 or later).

The tandem-verification to Spike needs a recent version of Spike installed, and
the RISCV environment variable set to its installation directory.

The model supports the following combinations of Spike configuration flags:
  --[en|dis]able-dirty --[en|dis]able-misaligned


Building
--------

- Ensure that l3 is in your path.

- Ensure that the RISCV environment variable is correctly defined.

- $ make

This will build the interpreter in 'l3riscv.poly' when compiled with Poly/ML.

Using the interpreter
---------------------

- Execute a RISC-V ELF binary:

  $ ./l3riscv --trace 1 <riscv-binary>

  To execute this in lock-step with a Spike back-end:

  $ ./l3riscv --trace 1 --check true <riscv-binary>

  The execution will stop with a failure at the first discrepancy between the
  execution of the model and that of Spike.

- Disassemble a RISC-V ELF binary:

  $ ./l3riscv --dis true  <riscv-binary>

Note that the interpreter cannot currently boot an OS since the SBI spec for
RISC-V has not yet been released.

Generating a machine-readable specification
-------------------------------------------

$ make ilspec

The specification generated will be in src/il/riscv.l3.

Known Issues
------------

- It passes most 64-bit M-, S-, and U-mode tests, and the 32-bit M- and U-mode
  tests, in Spike-checked mode.

  It does not implement the debug-module registers, and hence fails the
  rv{32,64}mi-p-breakpoint tests.

- It does not yet boot a full OS since it has no device models.

Credits
-------

This model started out as a port of the L3 MIPS model to RISC-V. The original
l3mips model is at https://github.com/acjf3/l3mips