Skip to content

Latest commit

 

History

History
51 lines (42 loc) · 2.75 KB

README.md

File metadata and controls

51 lines (42 loc) · 2.75 KB
Raw

KRISC-V: Semantics of RISC-V in K

This repository presents an executable formal semantics of the RISC-V ISA using the K framework. It is currently under construction.

Presently, we support the unprivileged RV32E base ISA under the following assumptions:

  • Memory is little-endian.
  • There is a single hart with access to all of physical memory.
  • All memory is readable, writeable, and executable.
  • Instruction fetch is the only implicit memory access.
  • Instruction memory is always coherent with main memory.

Repository Structure

The following files constitute the KRISC-V semantics:

  • word.md provides a Word datatype representing XLEN-bit values, along with associated numeric operations.
  • riscv-instructions.md defines the syntax of disassembled instructions.
  • riscv-disassemble.md implements the disassembler.
  • riscv.md is the main KRISC-V semantics, defining the configuration and transition rules to fetch and execute instructions.

Installation

Prerequsites: python >= 3.10, pip >= 20.0.2, poetry >= 1.3.2.

poetry install
make kdist-build

Usage

Execute a compiled RISC-V ELF file with the following command:

poetry -C kriscv run kriscv run test.elf

The output shows the final K configuration, including the state of memory, all registers, and any encountered errors. Execution can also be halted at a particular global symbol by providing the --end-symbol flag.

For Developers

Use make to run common tasks (see the Makefile for a complete list of available targets).

  • make build: Build wheel
  • make check: Check code style
  • make format: Format code
  • make test-unit: Run unit tests
  • make test-integration: Run integration tests
  • make test-architectural: Run the RISC-V Architectural Test Suite For interactive use, spawn a shell with poetry shell (after poetry install), then run an interpreter.

Running Tests

The integration and architectural tests require the RISC-V GNU Toolchain. During installation, follow instructions to build the Newlib-based cross-compiler. The riscv64-unknown-elf-* binaries must be available on your PATH.

Prior to running make test-architectural, you must also fetch the RISC-V Architectural Test Suite

git submodule update --init --recursive -- tests/riscv-arch-test

and install the Sail RISC-V model for use as a reference implementation.