RISCV in Sail

References:

RISCV Sail Definitions

riscv spec deps

in directory model/

  • ./model/ (files in dependency order)

    • …
    • riscv_xlen32.sail: define xlen for RV32
    • riscv_xlen64.sail: define xlen for RV64
    • …
    • prelude.sail : constains Sail library functions
    • prelude_mapping.sail :
    • prelude_mem.sail : defines lowest level memory access primitives. These primitives will be implemented by the various Sail backends. This depends on the value of xlen
    • prelude_mem_metadata.sail :
    • …
    • riscv_types.sail : This contains basic definitions used throughout the specification
      • privilege levels,
      • register indices,
      • interrupt and exception definitions,
      • enumerations,
      • types used to define memory accesses.
    • riscv_reg_type.sail : register types. In a separate file so that it can be redefined in the extensions.
    • riscv_regs.sail : contains base register file. Types is defined in riscv_reg_type.sail.
    • …
    • riscv_pc_access.sail : functions to access and modify the program counter.
    • …
    • riscv_sys_regs.sail : This describes the privileged architectural state:
      • M-mode and S-mode CSRs.
      • helpers to interpret CSR content, such sa WLRL and WARL fields.
      • WLRL/WARL fields are intended to capture platform-specific functionality, thus future versions of the model might separate their handling functions out into a separate platform-defined file.
      • riscv_sys_control.sail : This describes interrupt and exception delegation and dispatch, and the handling of privilege transitions.
      • riscv_sys_exceptions.sail : This defines the handling of the addresses involved in exception handling.
      • riscv_sync_exception.sail : This describes the structure used to capture the architectural information for an exception.
    • …
    • riscv_platform.sail : contains platform-specific functionality for the model.
      • physical memory map
      • local interrupt controller
      • the MMIO interfaces to the clock
      • timer and terminal devices
      • externally selectable options for platform behavior, such as:
        • handling of misaligned memory accesses
        • handling of PTE dirty-bit updates during address translation
        • those implemented outside of sail model, e.g., C or Ocaml emulators.
    • …
    • riscv_mem.sail : converts physical address access into 1) physical memory access, or 2) MMIO access to the devices, or 3) access fault.

    • riscv_vmem_*.sail : describes the S-mode address translation.

      • riscv_vmem_types.sail and riscv_vmem_common.sail contain the definitions and processing of the page-table entries and their various permission and status bits.

    • riscv_addr_checks_common.sail and riscv_addr_checks.sail: hooks for address transformation.

    • …

    • riscv_insts_*.sail : instruction definitions and their assembly language formats.

      • riscv_insts_base.sail : base integer instruction set.
      • riscv_insts_hints.sail : Hint instructions that are not implicitly handled elsewhere are explicitly handled here.
      • each instruction is represented as a variant clause of the ast type
      • the execution semantics are represented as a clause of the execute function
      • mapping clauses specify the encoding and decoding of each instruction to and from their binary representations and assembly language formats.

    • riscv_fetch.sail : contains the instruction fetch function.

    • riscv_step.sail : top-level fetch and execute loop.

      • step function: instruction fetch, fetch error handling, decoding, dispatching, checking interrupts.
      • loop function: the execution loop. Use the same HTIF(host-target interface) mechanism to detect the termination as Spike.

    • …

    • riscv_analysis.sail : This is used in the formal operational RVWMO memory model.

    • …

    • main.sail : ?

Example:

SRET instruction def in Sail:

union clause ast = SRET : unit

mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011

function clause execute SRET() = {
  match cur_privilege {
    User       => handle_illegal(),
    Supervisor => if   mstatus.TSR() == true
                  then handle_illegal()
                  else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC),
    Machine    => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
  };
  false
}

mapping clause assembly = SRET() <-> "sret"

More

Created Jan 25, 2022 // Last Updated Dec 6, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?