Forvis

Tool

Forvis is a Haskell-based RISC-V instruction-set simulator/formal ISA specification. A 2019 coverage-guided fuzzing study used it as a reference ISS and reported two Forvis issues involving privileged CSR access and RV32 REMU behavior.

First seen 5/28/2026

Last seen 6/9/2026

Evidence 9 chunks

Wiki v1

WIKI

Overview

Forvis is described in the RISC-V ISS fuzzing literature as an instruction set simulator (ISS) implemented in Haskell and intended to serve as a formal specification of the RISC-V ISA. The associated public GitHub repository is described as a "Formal specification of RISC-V Instruction Set" and is primarily Haskell.

Use in ISS verification research

READ FULL ARTICLE →

NEIGHBORHOOD

6 nodes · 7 edges

graph · Forvis · depth=1

RELATIONSHIPS

7 connections

Verifying Instruction Set Simulators using Coverage-guided Fuzzing ← evaluates 100% 5e

The paper evaluates Forvis as a reference ISS.

Instruction Set Architecture implements → 100% 2e

Forvis is an ISS aiming to be a formal specification of the RISC-V ISA.

Minimally Invasive Generation of RISC-V Instruction Set Simulators from Formal ISA Models ← compares with 85% 1e

The paper compares LIBRISCV with Forvis as a related Haskell-based RISC-V model

Formal ISA Model implements → 100% 1e

Forvis is a formal RISC-V ISA specification

Haskell uses → 100% 1e

Forvis is implemented in a restricted subset of Haskell

Instruction Set Simulator implements → 100% 1e

Forvis is an instruction set simulator for RISC-V.

Control and Status Register mentions → 90% 1e

Forvis has an error related to CSR access privileges.

LINKED ENTITIES

3 links

Verifying Instruction Set Simulators using Coverage-guided Fuzzing EVALUATES Extracted graph relationship

Instruction Set Architecture IMPLEMENTS Extracted graph relationship

Control and Status Register MENTIONS Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] Forvis is an ISS implemented in Haskell and intended as a formal specification of the RISC-V ISA. Verifying Instruction Set Simulators using Coverage-guided Fuzzing

[2] The public GitHub repository describes Forvis as a formal specification of the RISC-V instruction set and identifies Haskell as its language. rsnikhil/Forvis_RISCV-ISA-Spec

[3] The coverage-guided fuzzing paper used Forvis as a reference ISS alongside Spike in a RISC-V case study based on libFuzzer and an RV32IMA ISS. Verifying Instruction Set Simulators using Coverage-guided Fuzzing

[4] The study reported errors in Forvis, including H1 for privileged CSR access and H2 for REMU behavior in RV32 mode. Verifying Instruction Set Simulators using Coverage-guided Fuzzing

[5] In the evaluation table, RISC-V Torture detected Forvis H2, coverage-guided fuzzing detected Forvis H1 and H2, and the official RISC-V ISA tests reported no Forvis issue. Verifying Instruction Set Simulators using Coverage-guided Fuzzing