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

The paper Verifying Instruction Set Simulators using Coverage-guided Fuzzing used Forvis as one of two reference ISSs, alongside Spike, in a RISC-V case study. The study built a coverage-guided fuzzing approach on top of libFuzzer and used it while verifying an RV32IMA ISS extracted from a RISC-V Virtual Prototype.

In that evaluation, the authors reported that errors were found not only in the ISS under test but also in both reference ISSs, including Forvis.

Reported issues

The study reported two Forvis-specific issues:

• H1 — privileged CSR access: Forvis erroneously allowed access to CSRs representing hardware performance monitoring counters, such as the cycle CSR, from a lower privileged execution mode without first enabling access via the mcounteren and scounteren CSRs.
• H2 — RV32 REMU behavior: Forvis's REMU instruction behavior failed in a 32-bit configuration because it performed a 64-bit operation even though the ISS was configured for 32-bit mode.

In the paper's evaluation table, RISC-V Torture test generation detected the Forvis H2 issue, while the coverage-guided fuzzing run detected both H1 and H2. The official RISC-V ISA tests reported no Forvis issue in that table.

Repository

The public repository listed for Forvis is rsnikhil/Forvis_RISCV-ISA-Spec, described as a formal specification of the RISC-V instruction set and implemented in Haskell.