F# RISC-V Instruction Set Formal Specification

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
  • How to build and run it on RISC-V binaries
    • Make the application executable
    • Run the application executable

Features & Current status

  • Supports the following features
    • Base instruction sets: RV32I
  • Features under development
    • Base instruction sets: RV64I
    • 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 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 :
    rv32ui-p-*, rv64ui-p-*
    rv32um-p-*, rv64um-p-*
    rv32ua-p-*, rv64ua-p-*
    rv32uc-p-*, rv64uc-p-*

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:

  • Decode*.fs

    Decodes contain decoders for specific instructions set and notified with instruction/extention set symbol. For example DecodeI.fs

  • Execute*.fs

    Executes contain executions for specific instructions set and notified with instruction/extention set symbol. For example ExecuteI.fs

  • Utilities:

    • CLI.fs

      Contain helper function and types for building effective CLI commands and options.

    • Bits.fs

      Basic type specific functions for manipulations with bits .

    • Run.fs

      Basic Run flow - fetch, decode, execute, logging execution flow.

  • Architecture

    • Arch.fs

      Basic architecture types for RISC-V specification.

    • MachineState.fs

      Basic type and functions described RISC-V machine state.

  • Main app

    • Program.fs

    Main application to execute RISC-V simulator/emulator .

  • Test

    • Test/*.fs

      Contain unit-tests for instuctions set and extensions

    • Test/asm/

      Contain Assembler test programs for manual testing RISC-V CPI implementation. It depend on risc-v toolchain and it has special auto-build Make file .

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 OS:

  • Linux
  • Windows
  • MacOS

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

For Ubuntu:

$ 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

Then, you can build the application executable with:

$ dotnet build

Run the application executable

Most simple way run immediately run (without additional build command) to see command-line options on the executable:

$ dotnet run -- --help

If you run the application without option, like thet:

$ dotnet run

you'll receive error message:

Example to run specific ISA with extentions, verbosity output and ELF file for execution in RISC-V CPI simulator:

$ dotnet run -- -A rv32i -v myapp.elf

Wrong parameters put --help to get more information


MIT License