RISC-V formal ISA Specification
Copyright © Evgeny Ukhanov
This is a formal (and executable) specification for the RISC-V ISA (Instruction Set Architecture), written in F# purely functional style. We deliberately choose an "extremely elementary" implementation of F# to make it readable and usable by wide audience who do not know F# and who do not plan to learn F#.
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.
- Features & Current status
- Reading the code
- How to build and run it on RISC-V binaries
- How to Contribute
Features & Current status
- Supports the following features (or in active development state)
- Base instruction set: RV32I
- Tests RV32I
- Base instruction set: RV64I
- Tests RV64I
- Standard extension M (integer multiply/divide)
- Tests for Standard extension M RV32/RV64
- Standard extension A (atomic memory ops)
- Tests for Standard extension A RV32/RV64
- Features under development
- 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 U (User)
- Privilege Level S (Supervisor)
- Virtual Memory schemes SV32, SV39 and SV48
- Application can be executed as a F# program flexible with CLI (command line interface) support, which in turn executes RISC-V ELF binaries. This is a sequential interpretation: one-instruction-at-a-time, sequential memory model.
- Tests passing for RISC-V under development:
- Basic instruction flow
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)
Reading the code
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.
Main part for reading Specification:
Decodes contain decoders for specific instructions set and notified with instruction/extension set symbol. For example
Executes contain executions for specific instructions set and notified with instruction/extension set symbol. For example
Contain helper function and types for building effective CLI commands and options.
Basic type specific functions for manipulations with
Basic Run flow - fetch, decode, execute, logging execution flow.
Basic architecture types for RISC-V specification.
Basic type and functions described RISC-V machine state.
Main application to execute RISC-V simulator/emulator.
Contain unit-tests for instructions set and extensions
Contain Assembler test programs for manual testing RISC-V CPI implementation. It depend on risc-v toolchain and it has special auto-build
How to build and run it on RISC-V binaries
Application can be executed as a sequential RISC-V simulator (sequential, one-instruction-at-a-time semantics), by building and executing it as a standard F# program.
Supported .NET SDK:
- .NET SDK 2.2
- .NET SDK 3.0
Install .NET SDK
For Windows preferred way to use Visual Studio.
Other examples will be for Linux. Please follow to instruction https://dotnet.microsoft.com/download
$ wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb $ sudo dpkg -i packages-microsoft-prod.deb $ sudo apt-get update $ sudo apt-get install apt-transport-https $ sudo apt-get update $ sudo apt-get install dotnet-sdk-3.0
To check installation:
$ dotnet --version
will tell you what version of
dotnet you have.
Make the application executable
You can build the application executable with:
$ dotnet build
Run the application executable
Most simple way to run immediately
build command) to see command-line
options on the executable:
$ dotnet run -- --help
If you run the application without option:
$ dotnet run
you'll receive error message:
Wrong parameters put --help to get more information
Example to run specific ISA with extensions, verbosity output and ELF file for execution in RISC-V CPI simulator:
$ dotnet run -- -A rv32i -v myapp.elf
How to Contribute
Please read file CONTRIBUTING.md
- github ISA manual: https://github.com/riscv/riscv-isa-manual
- RISC-V specification: https://riscv.org/specifications/
- RISC-V Formal Verification Framework: https://github.com/SymbioticEDA/riscv-formal