Copyright (c) 2018-2019 Rishiyur S. Nikhil, Bluespec, Inc. Portions Copyright (c) Niraj Nayan Sharma, Bluespec, Inc.
See LICENSE for license details.
This is a formal (and executable) specification for the RISC-V ISA (Instruction Set Architecture), written in "extremely elementary" Haskell. We deliberately choose an "extremely elementary" subset of Haskell to make it readable and usable by people who do not know Haskell and who do not plan to learn Haskell.
This is a work-in-progress, one of several similar concurrent efforts within the "ISA Formal Specification" Technical Group constituted by The RISC-V Foundation (https://riscv.org). We welcome your feedback, comments and suggestions.
Please see NEWS for a timeline of significant events in the development of Forvis.
Uses Galois' softfloat-hs Haskell wrappers for Berkeley softfloat.
Uses the Berkeley softfloat C library for IEEE Floating Point emulation.
-
Forvis supports the following features
- Base instruction sets: RV32I and RV64I
- RV32 and RV64 are supported simultaneously, e.g., a program can have parts running in RV64 mode at Machine privilege and other parts running in Supervisor or User privilege in RV32 mode, by setting MISA.MXL, MSTATUS.SXL and MSTATUS.UXL appropriately.
- Standard extension M (integer multiply/divide)
- Standard extension A (atomic memory ops)
- Standard extension C (Compressed 16-bit instructions)
- Standard extension F (Single-precision floating point)
- Standard extension D (Double-precision floating point)
- Privilege Level M (Machine)
- Privilege Level S (Supervisor)
- Virtual Memory schemes SV32, SV39 and SV48
- Privilege Level U (User)
- Base instruction sets: RV32I and RV64I
-
Forvis can be executed today as a Haskell program, which in turn executes RISC-V ELF binaries. This is a sequential interpretation: one-instruction-at-a-time, sequential memory model (a concurrent interpreter will follow, later).
-
Passes all RISC-V ISA tests in the following sets (currently 402 tests):
-
rv32ui-p-*,rv64ui-p-*(Base instruction set) -
rv32um-p-*,rv64um-p-*(M extension) -
rv32ua-p-*,rv64ua-p-*(A extension) -
rv32uc-p-*,rv64uc-p-*(C extension) -
rv32ud-p-*,rv64ud-p-*(D extension) -
rv32uf-p-*,rv64uf-p-*(F extension) -
rv32mi-p-*,rv64mi-p-*(Machine privilege) -
rv32si-p-*,rv64si-p-*(Supervisor privilege) -
rv32ui-v-*,rv64ui-v-*(Base instruction set in virtual memory) -
rv32um-v-*,rv64um-v-*(M extension in virtual memory) -
rv32ua-v-*,rv64ua-v-*(A extension in virtual memory) -
rv32uc-v-*,rv64uc-v-*(C extention in virtual memory) -
rv32ud-v-*,rv64ud-v-*(D extension in virtual memory) -
rv32uf-v-*,rv64uf-v-*(F extension in virtual memory)
In this repo we provide pre-compiled binaries (ELF files) for all these tests, a script to run them as a regression, and sample output logs.
-
- 'Feature List' argument that configures Forvis to make particular allowed implementation choices (such as: trap or handle misaligned mem access) so that its instruction trace exactly matches a particular implementation.
- Interpreter supporting concurrency (modeling out-of-order execution, pipelining, speculation, multi-hart and more), and integration with RISC-V's RVWMO Weak Memory Model.
We expect that many people might use this as a reading reference (whether or not they build and execute it) to clarify their understanding of RISC-V ISA semantics.
The file src/Forvis_Spec.hs is the central file to read, containing
essentially the entire ISA specification. It specifies
instruction-fetch, and the execution of each kind of instruction.
That file, and all the remaining files, are expressed in Haskell, and can be found in:
src/*.hs
A PDF reading guide is provided in Doc/forvis_reading_guide.pdf. It
is intended to be used as a reference while perusing the actual
Haskell code, and is not a standalone document. It displays code
fragments automatically extracted from the actual code. [CAVEAT: needs
serious updating; was last revised July 2018; has not caught up with
addition of extensions A, C, F, D, decode step, etc.]
We suggest reading the code in this order:
Arch_Defs.hs Machine_State.hs Forvis_Spec.hs Forvis_Spec_I.hs ALU.hs Forvis_Spec_Common.hs Forvis_Spec_Zicsr.hs Virtual_Mem.hs GPR_File.hs CSR_File.hs Mem_Ops.hs Memory.hs MMIO.hs Run_Program.hs Main_Run_Program.hs Main.hs
The following are about specific architecture extensions and can be read in any order. They all follow the same pattern as Forvis_Spec_I.hs
Forvis_Spec_Zifencei.hs Forvis_Spec_I64.hs Forvis_Spec_A.hs Forvis_Spec_C.hs Forvis_Spec_M.hs Forvis_Spec_F.hs FPR_File.hs Forvis_Spec_D.hs FPR_File.hs
You can ignore the following, which are used for testing virtual memory translation and Tandem Verification, respectively (you're welcome to read them, if you're curious):
Main_Test_Virtual_Mem.hs Main_Tandem_Verifier.hs
Forvis can be executed as a sequential RISC-V simulator (sequential, one-instruction-at-a-time semantics), by building and executing it as a standard Haskell program.
You will need the standard Haskell compiler ghc and cabal, a
standard build/package manager for Haskell. These are available on
Linux, MacOS and Windows. Full installation details can be found at
haskell.org.
You will also need Haskell's standard elf library for parsing ELF
files.
For example, on Debian and Ubuntu systems, you can say:
$ sudo apt-get update
$ sudo apt-get install -y software-properties-common
$ sudo add-apt-repository -y ppa:hvr/ghc
$ sudo apt-get update
$ sudo apt-get install -y cabal-install-3.2 ghc-8.8.3
These will install the named versions of ghc and cabal into
/opt/cabal/ and /opt/ghc/. Add these to your PATH:
$ export PATH=/opt/cabal/bin:/opt/ghc/bin:$PATH
Then, you can install the elf library:
$ cabal install --lib elf
The above version numbers were current in March 2020. For Forvis per
se, the specific version of ghc should not matter, since Forvis is
written in "extremely elementary" Haskell that has been stable for
more than a decade. However, the simulator uses some external Haskell
libraries (elf, softfloat-hs) that require ghc version 8.2.1 or
later.
$ ghc --version
will tell you what version of ghc you have.
For other OSs, you can do the analogous package-install using their
native package mechanisms, Macports on Apple OS X, etc. Please consult
haskell.org for more details.
If you are not interested in the RISC-V F and D extensions (single- and double-precision floating point), you can skip this section and its steps.
By default, the Makefile builds a Forvis simulator without F and D because the build is a little more involved, using the Berkeley 'softfloat' IEEE floating point emulation library and the Galois Haskell foreign-function interface wrappers for softfloat.
To include F and D, you should first uncomment the # FLOAT := yes
line in the Makefile.
Next, you need the following one-time action to get, build and install the Berkeley 'softfloat' .
$ make build_softfloat
This is the only step where there may be trouble, since its components are external git repos. Please see the Makefile for the detailed steps, if necessary.
Then, you can build the Forvis executable (forvis_exe) with:
$ make exe
Run the following to see command-line options on the executable:
$ ./forvis_exe --help
Then, try the following tests to execute the standard RISC-V ISA test
rv32ui-p-add on the Forvis executable at verbosity 0, 1 and 2
respectively.
$ make test
$ make test_v1
$ make test_v2
Look at the commands in the Makefile that these execute. If you
substitute "64" for "32" you'll run the rv64ui-p-add test.
You can also run two pre-compiled C programs--the standard "Hello World!" program and the "Thuemorse" program:
$ make test_hello
$ make test_thue
You can follow the template of any of the above tests to execute any
of the many pre-compiled RISC-V ELF binaries found in
Test_Programs/. Please see README.txt in that directory for more
information on the binaries.
Please see Regression_Testing/README.txt for how to automatically
run Forvis on all ELF files in a directory tree such as Test_Programs/.
Note: the default build excludes the RISC-V F and D extensions (single- and double-precision floating point). When you run the regression, it will expectedly fail on all the ISA tests for F and D (having 'uf' and 'ud' in the filenames of the tests).
We have provided a pre-built Linux kernel ELF file in: Test_Programs/Linux_kernel/rv64-vmlinux.elf
We have provided an RV64 boot ROM containing a compiled device tree in: Test_Programs/boot_ROM_RV64.hex32
The kernel has been built for RV64IMAUS. It expects to access the following:
- A boot ROM with a compiled device tree;
- A 256 MiB memory;
- A timer implementing the memory-mapped MTIME and MTIMECMP locations, capable of generating timer interrupts;
- A memory-mapped location MSIP for generaing software interrupts;
- A model of the National Semiconductor NS16550 UART for console I/O.
All these are supplied in the source code and incorporated into the Forvis executable.
To boot the Linux kernel, in the top-level directory, after you have created the Forvis executable (see above):
$ make test_linux_boot
This takes about 8 minutes on a 2.60GHz Intel Core i7-6700HQ with 6
MiB cache, with 16 GiB of memory (Forvis, when running, takes about
3.1 GiB of memory). Please see Linux_boot_log.txt for an example of
what you should see on your console. At the end of the boot sequence,
you will see a prompt:
... <various boot progress messages> ...
[ 0.080000] This architecture does not have kernel memory protection.
Please press Enter to activate this console.
Press the key, and after a short delay you should see a shell prompt, at which you can type various shell commands. When done, press Control-C to exit. Examples:
/ # ls
bin etc linuxrc root sys usr
dev init proc sbin tmp
/ # cat /proc/cpuinfo
cat /proc/cpuinfo
hart : 0
isa : rv64imaus
mmu : sv39
/ # cat /etc/inittab
cat /etc/inittab
::sysinit:/etc/init.d/rcS
console::askfirst:/bin/sh
/ # ^C
Caveat: because of simulation overheads, the shell response is sluggish; please wait for a bit for each response.