L3riscv

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