SOURCE ARCHIVE
EXTRACTED CONTENT
52,920 chars FP-RVVTS: Sail-guided Verification of
RISC-V Floating-Point Implementations
Katharina Ruep, Manfred Schlägl, Daniel Große
Institute for Complex Systems, Johannes Kepler University Linz, Austria {katharina.ruep, manfred.schlaegl, daniel.grosse}@jku.at
Abstract—This paper presents a Sail-guided FP-RVVTS flow but it also risks turning simulator-specific behavior into the that uses Sail RISC-V as an executable RISC-V specification de facto specification. This is particularly problematic for FP for differential verification of RISC-V Floating-Point (FP) im- instructions, where the corner cases described above often plementations, from Instruction Set Simulators (ISSs) to Register Transfer Level (RTL) designs. FP-RVVTS generates positive and appear only in rare operand combinations and can therefore negative tests for RV32/RV64 F, D, and Zfh, executes them against be missed by conventional testing. Sail RISC-V and a Design Under Test (DUT), and compares the This paper therefore takes Sail RISC-V [5] as the golden resulting architectural state. Observed mismatches are minimized reference for FP verification. Unlike a conventional reference to compact, self-contained failing test cases and characterized simulator, Sail RISC-V is the Sail formal specification of the by affected state, flags, exceptions, special values, and precision interactions to support root-cause analysis. We evaluate ISSs, FP- RISC-V architecture adopted by RISC-V International [5]. library integrations, and the PULP ARA RTL implementation. It defines instruction formats, encoders and decoders, and The generated tests achieve very high F/D functional coverage instruction semantics in a language designed for precise ISA and expose 9 non-trivial bugs, including 5 newly discovered descriptions, and can be compiled into an executable model issues. These results demonstrate that the Sail-guided FP-RVVTS while also serving as a basis for formal artifacts [6]. This flow enables practical RISC-V FP verification across ISSs, FP- library integrations, and RTL implementations. changes the role of the oracle in the verification flow: gener- ated tests are checked against an executable form of the archi- I. INTRODUCTION tectural model rather than against another implementation that Although Floating-Point (FP) instructions constitute only a may encode its own design choices. For FP behavior, where modest fraction of an Instruction Set Architecture (ISA) by in- architecturally relevant mismatches may arise only for rare struction count, their semantics make them disproportionately operand combinations and manifest as bit-level deviations, this difficult to implement correctly. Their behavior is governed distinction is essential, as it enables deviations in simulators, by a dense combination of finite precision, multiple rounding FP libraries, and RTL implementations to be evaluated with modes, exception flags, subnormal numbers, infinities, signed respect to the architectural model. zeros, and not-a-number values (NaNs) [1]. These semantic The starting point of our work is RVVTS, an open-source features are central to IEEE-754-compatible numerical and framework built around a grammar-based RISC-V Instruc- data-intensive software, including scientific computing, signal tion Sequence Generator (ISG) and supporting positive and processing, graphics, and machine-learning workloads. At the negative testing, differential execution, failure isolation, and same time, they create corner cases in which a single result bit, minimization [7], [8]. Recent late-breaking work introduced exception flag, or NaN-boxed value can determine whether an FP-RVVTS as a FP extension of this framework [9]. It added implementation is architecturally correct. For RISC-V [2], [3], a context-free grammar for the RV32/RV64 F, D, and Zfh this challenge is amplified by an open and rapidly evolving FP extensions and enriched the grammar with dependency ecosystem: simulators, software FP libraries, processor gen- annotations to derive compact test cases that reproduce ob- erators, and Register Transfer Level (RTL) implementations served failures. That work demonstrated high-coverage test are developed by different communities and are often used generation for RISC-V simulators and their FP backends, interchangeably as reference models, validation targets, or including SoftFloat (SF) [10] and FloppyFloat (FF) [11]. execution platforms. However, it used Spike as the reference simulator and was Testing FP support in this setting is not only a matter limited to simulator DUTs, leaving formal specification-guided of producing many random instructions [4]. The generated and RTL-level verification open. programs must be architecturally valid, exercise exceptional Contribution: This paper advances FP-RVVTS in two com- behavior deliberately, cover interactions between the RISC-V plementary directions: toward specification-driven verification F, D, and Zfh extensions, and preserve enough state to make by replacing the simulator-based oracle with Sail RISC-V , failures reproducible. At the same time, a test oracle must and toward implementation-level verification by including be trusted across heterogeneous Design Under Tests (DUTs). RTL DUTs as verification targets. We integrate Sail RISC-V Using one simulator as the golden reference can be practical, into FP-RVVTS as an executable architectural reference for test-set generation and differential test-set execution. The 979-8-3195-3997-7/26/$31.00 ©2026 IEEE grammar-based FP ISG and dependency annotations from
prior FP-RVVTS work are refined and used for compact failure streams on an RTL core and an ISS reference [20], [21], while
reduction through Dependency-Based Test-Case Minimization. recent verification environments for RISC-V vector accelera-
In addition, we introduce Automated Failure Characterization tors combine random instruction generation, scoreboards, and
to group failures by instruction, affected architectural state, functional coverage for complex vector RTL targets [28]. Such
exception behavior, FP flags, special-value handling, and preci- flows are effective for exposing implementation mismatches,
sion interactions, thereby supporting root-cause analysis across but their oracles are typically conventional simulators, manu-
simulators, FP-library integrations, and RTL targets. ally constructed checkers, or design-specific scoreboards. At
We evaluate FP-RVVTS on a heterogeneous set of RISC-V the specification level, Sail provides executable and mecha- FP implementations spanning Instruction Set Simulators nized ISA semantics for architectures including RISC-V [6], (ISSs), FP-library integrations, and RTL. As simulators we and Sail RISC-V has been adopted as the RISC-V architectural include Spike [12], RISC-V VP++ [13], [14], QEMU [15], and model [5]. This work uses Sail RISC-V as the golden reference configurations based on SF and FF, covering both simulator- for both test-set generation and differential test-set execution. level behavior and the effect of different FP backends. For Thus, mismatches are evaluated against an executable archi- the simulator configurations, the Sail-guided flow confirms tectural specification rather than against another simulator or the failures previously observed with a Spike-based reference, a design-specific reference model. Moreover, the Sail-guided showing that these issues are not artifacts of a simulator- FP-RVVTS flow applies one executable architectural oracle specific oracle but also hold with respect to the executable across simulators, FP-library integrations, and RTL imple- architectural specification. To demonstrate FP-RVVTS be- mentations. It retains failure isolation and state minimization yond simulators, we apply it to the RTL implementation of for compact instruction-level debugging, and adds automated PULP ARA [16], a silicon-proven and representative high- failure characterization to support root-cause analysis. performance RISC-V vector processor. The ARA case study FP verification has also been studied for dedicated hardware exposes HW-specific FP failures, including missing Not a blocks and for RISC-V FP instructions. For instance, Kaiser et Number (NaN)-boxing checks, incorrect exception-flag be- al. [29] verify a RISC-V-compatible fused multiply-add unit havior, and critical deviations in division and square-root using a UVM-based environment and an external processor operations. Overall, this demonstrates the value of and need Floating-Point Unit (FPU) as reference model. A closely for a Sail-guided methodology targeting the full spectrum from related RISC-V-specific work is the coverage- and constraint- simulators to RTL. based RV32F test-generation approach by Lu et al. [30], The complete FP-RVVTS framework, including all pre- which explicitly targets FP instruction verification for one sented extensions and evaluation artifacts for the investigated concrete RTL processor. Unlike this RV32F-specific approach, DUTs, are available as open source on GitHub1. FP-RVVTS covers RV32/RV64 F, D, and Zfh, is available as II. RELATED WORK open source, uses Sail RISC-V as the executable architectural model rather than a simulator or processor FPU, and targets Verification of RISC-V processors has been addressed ISSs, FP-library integrations, and RTL. by a broad range of simulation-based, formal, and hybrid III. FP-RVVTS techniques [17]. Existing work includes compliance-oriented test generation [18], mutation-based compliance testing [19], FP-RVVTS automates the generation, execution, and failure cross-level simulation between ISSs and RTL models [20], isolation of FP test cases through a systematic multi-stage [21], equivalent-program and metamorphic testing [22], [23], verification flow that maximizes coverage while minimiz- open validation suites [24], constrained-random generation ing manual effort. In this section, we present the complete such as Google’s RISCV-DV [25], and recent processor FP-RVVTS verification flow and its associated extensions and fuzzing approaches [4], [26], [27]. These methods target broad enhancements. ISA correctness, compliance, or RTL bring-up across many We begin in Section III-A by introducing the two primary instruction classes. They may expose FP failures when such FP-RVVTS sub-flows, Test-Set Generation and Test-Set Exe- instructions occur in generated programs, but they do not make cution. Next, Section III-B describes the integration of our the RISC-V FP extensions, exception flags, rounding modes, new golden reference model, Sail RISC-V , into FP-RVVTS. NaN-boxing, or FP-library behavior the central coverage ob- In Section III-C, we introduce the grammar-based ISG used jective. For example, RISCV-DV initializes FP registers with to randomly generate valid FP code sequences. Subsequently, special values at the beginning of a test, which limits operand Section III-D describes the Dependency-Based Test-Case Min- diversity during later execution, whereas processor fuzzers imization used for compact failure reduction, and Section III-E such as Cascade [27] treat FP behavior as one part of a larger presents our Automated Failure Characterization approach for processor state space. accelerating root-cause analysis. Beyond instruction generation, prior work has also stud- A. Primary FP-RVVTS Sub-Flows ied cross-level checking and verification infrastructure for RTL targets. Cross-level testing executes generated instruction The first sub-flow, Test-Set Generation, shown in Fig. 1, generates high-coverage test sets for both positive and negative 1https://github.com/ics-jku/FP-RVVTS testing of RISC-V FP implementations. Starting from an
pos
only new code
execute test keep ...
no ex- yes "<instr_f_calc>": [
add new on Sail ception? block
code test RISC-V no yes "<instr_f_calc1><flen> <frd>, <frs1><rm>",
sequence set valid? "<instr_f_calc2><flen> <frd>, <frs1>, <frs2><rm>",
via
FP ISG execute no discard "<instr_f_calc3><flen> <frd>, <frs1>, <frs2>, <frs3><rm>",
cov. in- yes new code ],
on crement?
OVPSim no block "<instr_f_calc2>": [" fadd ", "fsub", "fmul", "fdiv"],
...
Fig. 1: Overview of FP-RVVTS’s Test-Set Generation sub-flow. Listing 1: Arithmetic instruction subset of the FP grammar.
execute continue get annotation of in FP-RVVTS requires implementing an ExecutionRunner that
with next
on DUT test case failing instruction executes compiled test cases on the target model and extracts
test set partition test compare no create new the resulting Machine State for use by FP-RVVTS, as described
test set case output any diff? minimized failing in Section III-A.
yes test case
execute isolate To integrate Sail RISC-V as a golden reference model, we
on Sail failing rerun DUT w/o
RISC-V instruction failing instruction implement the SailRunner as a dedicated ExecutionRunner.
Fig. 2: Overview of FP-RVVTS’s Test-Set Execution sub-flow. The extraction of the Machine State from Sail RISC-V
is realized through two complementary mechanisms. First,
empty test set, the grammar-based FP ISG (see Section III-C) FP-RVVTS instruments each test case with code that, im-
randomly generates code sequences that are added to the test mediately after the test-case section completes, stores the
set. The resulting test set is then executed on the golden relevant architectural state in a dedicated memory region on
reference Sail RISC-V (see Section III-B) for validation and the target. Second, we extend Sail RISC-V with a mechanism
on riscvOVPSim [31] for functional coverage measurement, that generates a memory dump file containing the stored state
as shown by the two execution paths in Fig. 1. Based on this, before Sail RISC-V terminates. This memory dump file is
FP-RVVTS verifies that the augmented test set remains valid subsequently parsed by FP-RVVTS to reconstruct the corre-
and that overall coverage improves. In pos mode, only code sponding Machine State for automated state comparison, test-
sequences that do not raise exceptions are admitted, ensuring case minimization, and analysis.
that the resulting test set targets positive testing exclusively. If
all conditions are met, the new code sequences are retained; C. Random FP Instruction Sequence Generation
otherwise, the added code sequences are discarded and the In this section we introduce the grammar-based ISG, which
previous state of the test set is restored. This process repeats underpins the high-coverage FP Test-Set Generation sub-flow
until the test set reaches a predefined coverage threshold. presented in Section III-A.
The second sub-flow, Test-Set Execution, shown in Fig. 2, The FP grammar is structured as a production system where
applies a pre-generated test set to the DUT, compares out- non-terminals map to either string templates, instruction lists
comes to the reference model, and drives failure isolation or callable generators. Configuration parameters (e.g., enabled
and failing test-case minimization: The sub-flow partitions the extensions, base ISA width) decide which productions are
given test set into small, self-contained test cases of config- valid, ensuring all generated instruction sequences respect the
urable size. Each of these test cases is executed on the DUT target ISA without manual retargeting. From the start symbol,
and the golden reference Sail RISC-V . Both executions pro- the grammar-driven ISG recursively expands non-terminals,
duce comparable architectural-state outputs (Machine States), randomly selecting instructions and operands from the FP and
comprising, for example, register values, a trap counter, and integer register files to produce valid, architecturally compliant
hashes of relevant memory regions. If differences are detected instruction sequences.
between the Machine States of the DUT and the reference, Example 1. Listing 1 shows the FP grammar for arithmetic
FP-RVVTS classifies the test case as failed and initiates instructions. The non-terminal
... // restore floating point register
" <frd> ": ("<f_reg>", {"clob": "_"}), _reg_f24:.byte 0x00,0x40,0xc7,0x44,0xff,0xff,0xff,0xff
" <frs1> ":("<f_reg>", {"dep": "_"}), la t0, _reg_f24
"<frs2>":("<f_reg>", {"dep": "_"}), fld f24 , 0(t0)
... // restore fcsr {'nx': F, 'uf': F, 'of': F, 'dz': F, 'nv': T, 'rm': 'rne', 'res': 0}
li t0, 0x10
Listing 2: Register part of the FP grammar with dependency annotation. csrrw zero, fcsr, t0
// restore mstatus.fs/vs = {'fs': 'dirty', 'vs': 'off'}
and omits double-precision instructions such as fld and fsd. li t0, 0x6600
csrc mstatus, t0
Any combination of F, D and Zfh that satisfy the architectural li t0, 0x6000
extension dependencies is supported. csrs mstatus, t0
// restore registers
In addition, both RISC-V rounding-mode mechanisms are li x27 , 0x802160ba
supported: static selection via the rm field of an instruction, // INSTR. DEP. METADATA: {'dep': {'fcsr.rm', 'mstatus.fs/vs.fs', 'x27'}, 'clob': {'f24'}}
fcvt.h.l f24 , x27 , rne
and dynamic selection via the frm field of fcsr when rm is set
to DYN. The ISG randomizes frm alongside other Control and Listing 3: Example of minimal snapshot for failing instruction.
Status Register (CSR) state, varying rounding mode and status Test-Case Minimization automatically constructs a minimized
flag combinations across test code and improving coverage failing test case containing only the required architectural-state
over [9]. initialization and the single failing instruction.
D. Dependency-Based Test-Case Minimization Example 3. Listing 3 shows a minimized test case. The last
As introduced in the Test-Set Execution sub-flow in Sec- line contains the failing instruction fcvt.h.l, which converts
tion III-A, Dependency-Based Test-Case Minimization reduces the integer in x27 to a half-precision FP in f24 . The
an isolated failure to a compact, self-contained test case. highlighted comment above it lists its dependency metadata:
After FP-RVVTS has isolated the failing instruction, the dep (CSRs, source register) and clob (destination register).
instruction’s dependency metadata, derived from the depen- To reconstruct the Machine State before execution, f24 is
dency annotations during generation, is used to determine the restored to its pre-instruction value, followed by the CSRs
Machine State elements required to reproduce its behavior. fcsr and mstatus, and finally x27 . The result is a compact,
This metadata is generated by the ISG from the FP grammar self-contained test case that reliably reproduces the failure,
during Test-Set Generation and captures both dependencies greatly aiding debugging.
(e.g., source registers, CSRs) and potential effects (e.g., desti- E. Automated Failure Characterization
nation registers). The original test case is then re-executed on In this section we introduce our Automated Failure Charac-
Sail RISC-V with the failing instruction removed, yielding the terization method, which post-processes failures to summarize
pre-failure Machine State, i.e., the Machine State immediately key attributes and accelerate root-cause analysis. For each
before the failing instruction would have executed. From detected failure, FP-RVVTS generates a report containing
this state, FP-RVVTS extracts the values referenced by the the instruction, rounding mode, state differences, affected
failing instruction’s metadata and synthesizes minimal state- registers, and attributes such as exceptions, FP flags, special
initialization code, which is combined with the isolated failing values (NaN, Infinity (Inf), zero), and precision mismatches.
instruction to form the minimized failing test case. Affected registers provide information about their values and
In the following, we describe how the FP grammar is reveal the precision stored in each register (e.g., h for
annotated with dependency information and how the ISG half-precision). Assigned attributes help identify similarities
propagates this information to instruction-level dependency between failures, enabling them to be automatically grouped to
metadata. Relevant grammar entries are labeled as either dep find the common root causes. Together, these reports facilitate
or clob. The dep label denotes state required to reproduce root-cause analysis by connecting observable differences to
the instruction’s behavior, while the clob label identifies state their underlying causes.
modified by the instruction whose pre-instruction value must Example 4. Listing 4 shows the report of the failed minimized
be captured to make the failure observable. test case introduced in Listing 3. This test case is part of
Example 2. Listing 2 shows a snippet of the FP grammar. The the set that exposed bug6 in PULP ARA, discussed later in
destination register
+======================================================+ results from [9] while providing a stronger, specification-
Instruction : fcvt.h.l f24 , x27 , rne aligned foundation. The failures in the remaining 8 test setups
+======================================================+
Attributes : fcsr ['invalid ', 'overflow', 'inexact '] (3–8, 11, 12) are analyzed next.
special values ['inf']
+------------------------------------------------------+ B. Failure Characterization and Bug Analysis
diffs:
REG REF DUT DIFF Using the Automated Failure Characterization introduced
fcsr.of True False X in Section III-E and similarity checks of the resulting reports,
+------------------------------------------------------+
Registers : f24 , x27 we identified the dedicated bugs summarized in Table II.
REG REF DUT Before discussing the newly discovered bugs, we briefly
+------------------------------------------------------+
x27 0 x00000000802160ba 0 x00000000802160ba revisit bug1–4, which were first reported in [9] using Spike as
f24 0 xffffffffffff7c00 /inf_h 0 xffffffffffff7c00 /inf_h the golden reference. Our Sail-guided flow confirms that all
+======================================================+ four are genuine ISA non-conformances rather than artifacts of
Listing 4: Example report for a failure. (excerpt) a simulator-specific oracle: bug1 occurs in RISC-V VP++ SF,
IV. EVALUATION when at least one input is NaN, the DUT returns NaN
instead of the non-NaN operand, implementing the pre-v2.2
For evaluation, we consider 12 test setups, formed by pair- RISC-V specification behavior rather than the current seman- ing 6 DUT configurations with 2 test sets. As DUTs we include tics introduced in v2.2. bug2a/b affect FP load/store instruc- three RISC-V simulators: Spike [12], RISC-V VP++ [13], and tions in RISC-V VP++, when the FP extension is disabled, QEMU [15], with FP libraries SF [10] and FF [11] integrated RISC-V VP++ omits the required extension-enabled check into the first two. Additionally, we include the RTL imple- and executes the instruction instead of raising an exception, mentation of PULP ARA [16]. We used the RV64IFD_Zfh whereas Sail RISC-V correctly signals a fault. bug3 reveals configuration to provide the broadest FP coverage supported that RISC-V VP++ FF correctly computes the NaN result but across all tested DUTs, covering single-precision (F, FP32), then zero-extends the 32-bit value to 64 bits instead of sign- double-precision (D, FP64), and half-precision (Zfh, FP16). extending it as required by the RISC-V specification. bug4 The test sets consist of a positive (pos) and a negative (neg) shows an incorrectly generated OF flag, with Sail RISC-V test set. Both are generated using the Test-Set Generation sub- setting the flag as required while the Spike FF does not. We flow presented in Section III, with Sail RISC-V serving as now discuss the newly discovered bug5–9 in more detail. the validation model and riscvOVPSim used for functional bug5 affects fmv.x.h in RISC-V VP++. When the source coverage measurement. The positive test set comprises code FP register holds an invalidly NaN-boxed FP16 value, the that executes without exceptions, validating correct execution DUT incorrectly substitutes a canonical quiet NaN before paths; the negative test set includes code that triggers excep- extracting the bits, producing 0x7E00 instead of the correct tions, ensuring proper exception handling and fault detection. sign-extended lower 16 bits. Per the RISC-V specification, fmv Coverage measurement is restricted to F and D extensions, as instructions are explicitly exempt from NaN-boxing checks the Zfh extension is not supported by riscvOVPSim. Instruction and must transfer raw bits directly without reinterpretation [2]. coverage reaches 100%. Functional coverage reaches 99.94% bug6 exposes incorrect exception flag generation in ARA’s with 5 108 test cases in the negative test set with only one FP conversion module for integer-to-float cast instructions. case uncovered: For load/store instructions, the zero register When an integer value exceeds the destination format’s rep- x0 is never used as rs1. Addresses for these instructions resentable range, IEEE 754 requires the OF flag to be set are computed beforehand in the ISG, so rs1 always holds while NV must remain clear [1]. In ARA the two flags are a valid and non-zero base address. For the positive test swapped due to an erroneous gate in the flag assignment logic set, coverage reaches 98.87% with 5 271 test cases because of the shared cast unit in the FPU. Although the defect exists reserved rounding modes (rm) would raise exceptions and are in shared code affecting all integer-to-float widths, it only therefore excluded by construction. manifests for FP16 destinations. FP32 and FP64 can represent A. Application on DUTs and Results (although potentially inexact) the entire range of any 64-bit integer, so overflow never occurs and the swapped flags are Using the Test-Set Execution sub-flow and its Dependency- never triggered. FP16’s limited range overflows with even Based Test-Case Minimization, presented in Section III, we modest inputs, exposing the bug. The presence of OF and evaluate all considered DUTs with the generated test sets. NV flag discrepancies with the destination register agreeing Table I summarizes the observed failures, indexed by test between the golden reference and ARA confirms that only flag setup ID, DUT, and test set (pos or neg). The remaining generation is affected. columns list the isolated failing instructions, with each cell bug7 corresponds to a missing NaN-boxing check in ARA. reporting the number of failures (architectural state differences When a FP register holds a narrow-format value (e.g., FP32) between Sail RISC-V and the DUT). Both Spike SF (1, 2) and in a wider register file (e.g., 64-bit), the RISC-V specifica- QEMU (9, 10) match Sail RISC-V across both test sets, thus tion requires the unused upper bits to be all ones, which produce no failures. This supports our choice of Sail RISC-V is known as NaN-boxing [2]. The div/sqrt module in ARA as the golden reference, since it confirms the Spike-based fails to validate this condition before consuming operands.
TABLE I: Reported failures for different test setups
Test Setup Isolated Failing Instructions
ID DUT TS fcvt.h.l fcvt.h.lufcvt.h.w fcvt.h.wufcvt.wu.dfcvt.wu.sfdiv.d fdiv.h fdiv.s fld flh flw fmax.d fmax.s fmin.d fmin.s fmul.d fmv.x.h fnmsub.d fsd fsh fsw fsqrt.d fsqrt.h fsqrt.s
1 Spike SF pos - - - - - - - - - - - - - - - - - - - - - - - - -
2 Spike SF neg - - - - - - - - - - - - - - - - - - - - - - - - -
3 Spike FF pos - - - - - - - - - - - - - - - - 1 - 1 - - - - - -
4 Spike FF neg - - - - - - 1 - - - - - - - - - - - - - - - - - -
5 VP++ SF pos - - - - - - - - - - - - 95 108 107 108 - - - - - - - - -
6 VP++ SF neg - - - - - - - - - 344 125 418 27 20 19 15 - 23 - 352 179 398 - - -
7 VP++ FF pos - - - - 368 324 - - - - - - - - - - - - - - - - - - -
8 VP++ FF neg - - - - 69 84 - - - 343 125 418 - - - - - 22 - 352 138 397 - - -
9 QEMU pos - - - - - - - - - - - - - - - - - - - - - - - - -
10 QEMU neg - - - - - - - - - - - - - - - - - - - - - - - - -
11 ARA pos - - - - - - 6 - 44 - - - - - - - - - - - - - 23 - 266
12 ARA neg 3 3 2 1 - - 4 5 212 - - - - - - - - - - - - - 5 16 63
TABLE II: Bugs identified using Automated Failure Characterization
bug-ID DUT Affected Instructions Diff Attributes Bug
bug1 VP++ SF fmax.d/s, fmin.d/s float destination reg. NaN NaN handling
bug2a VP++ SF/FF fld/h/w float destination reg., exception - FP enable check
bug2b VP++ SF/FF fsd/h/w memory, exception -
bug3 VP++ FF fcvt.wu.d/s int. destination reg. precision mismatch NaN handling
bug4 VP++ FF fdiv/fmul/fnmsub.d OF flag OF flag OF flag generation
bug5 VP++ SF/FF fmv.x.h int. destination reg. precision mismatch precision-mismatch handling
bug6 ARA fcvt.h.l/lu/w/wu OF flag OF/NV/NX flag OF & NV flag generation
bug7 ARA fdiv.s/d, fsqrt.s/d FP destination reg. NaN, precision mismatch NaN-boxed check is missing
bug8 ARA fdiv.s/d DZ/NV flag DZ/NV flag incorrect behavior for 0.0/0.0
bug9 ARA fdiv.s/d, fsqrt.s/d FP destination reg. NX flag one-ULP result error
Instead of treating an invalid boxed value as a canonical certain inexact results.
quiet NaN, the hardware interprets the raw bit pattern directly, Overall, the evaluation confirms that FP-RVVTS achieves
producing an incorrect result in the destination register. The near-complete F/D functional coverage in our coverage model
bug is consistently flagged by NaN and precision-mismatch and exposes non-trivial bugs across simulators, FP-library in-
attributes. tegrations, and silicon-proven RTL, while Dependency-Based
bug8 exposes incorrect exception flag generation in ARA Test-Case Minimization and Automated Failure Characteriza-
when both operands are zero (0.0/0.0). According to the IEEE tion accelerate root-cause analysis.
754 standard, this operation constitutes an invalid operation V. C
and must return a canonical quiet NaN with only the NV flag ONCLUSIONS
set; the DZ must remain clear, as it is reserved exclusively This paper presented FP-RVVTS, a Sail-guided verification
for nonzero dividends divided by zero [1]. The bug manifests flow for RISC-V FP implementations that uses Sail RISC-V
independently of bug7 and is confirmed by native FP64 as executable architectural specification instead of a simulator- test cases where both operands are genuine zero. The bug specific oracle. The flow combines grammar-based test genera- is additionally triggered as a secondary symptom of bug7: tion, differential execution, failure isolation, dependency-based when invalidly NaN-boxed FP32 operands are passed through minimization, and automated failure characterization. without validation, they are misinterpreted as genuine zeros We evaluated FP-RVVTS on six DUTs spanning ISSs, FP- and fall into the 0.0/0.0 path, producing the same spurious library integrations, and the silicon-proven PULP ARA RTL DZ flag. Both the standalone FP64 case and the NaN-box- implementation. The generated test sets achieve near-complete induced case are consistently detected through the spurious F/D functional coverage and expose nine non-trivial bugs, DZ flag alongside the correctly expected NV flag. four previously reported simulator bugs confirmed against bug9 captures two failure patterns in ARA’s div/sqrt round- Sail RISC-V and five newly discovered issues. ing path, both manifesting as a one-Unit in the Last Place Overall, the results show that a Sail-guided oracle, com- (ULP) error in the FP destination register with the NX flag bined with compact failure reduction and structured failure set. The first pattern is a missing rounding mode: the round- characterization, enables practical RISC-V FP verification to-nearest, ties-to-max-magnitude mode (rmm) is absent from from simulators to RTL. The complete FP-RVVTS framework, the rounding case statement and falls through to the default together with the presented extensions, versioned test sets, and truncation behavior, causing the result to be one ULP too evaluation artifacts, is available in reproducible open-source low whenever rmm is selected explicitly or via the dynamic form. rounding mode (dyn). The second pattern is an incorrect sticky ACKNOWLEDGMENTS bit computation for FP64 operands: the guard and sticky bit This work has partially been supported by the LIT Secure and Correct Systems Lab extraction range overlap by one bit position, causing rup funded by the State of Upper Austria, and the ODE4EC-DIG project funded by Chips JU rounding mode to silently truncate instead of rounding up on (Grant Agreement No. 101252715) and co-funded by the Austrian Research Promotion Agency (FFG).
REFERENCES [26] J. Xu, Y. Liu, S. He, H. Lin, Y. Zhou, and C. Wang, “MorFuzz: Fuzzing
[1] IEEE Standard for Floating-Point Arithmetic, IEEE Computer Society processor via runtime instruction morphing enhanced synchronizable co- Std. IEEE Std 754-2019, 2019. simulation,” in USENIX Security Symposium (USENIX), 2023, pp. 1307– [2] The RISC-V Instruction Set Manual Volume I: Unprivileged Architecture, [27] 1324. Version 20260120, RISC-V International, 2026. F. Solt, K. Ceesay-Seitz, and K. Razavi, “Cascade: CPU fuzzing via in- tricate program generation,” in USENIX Security Symposium (USENIX), [3] The RISC-V Instruction Set Manual Volume II: Privileged Architecture, 2024, pp. 5341–5358. Version 20260120, RISC-V International, 2026. [28] I. Diaz, J. Sans, J. Quiroga, L. Valente, M. Dominguez, M. Rodriguez, [4] A. Joannou, P. Rugg, J. Woodruff, F. A. Fuchs, M. van der Maas, M. Moreto, N. Sonmez, O. Palomar, R. I. Genovese, V. Jimenez, M. Naylor, M. Roe, R. N. M. Watson, P. G. Neumann, and S. W. and V. L. Guglielmi, “Functional verification of a RISC-V vector Moore, “Randomized testing of RISC-V CPUs using direct instruction accelerator,” IEEE Design & Test, vol. 40, no. 3, pp. 36–44, 2023. injection,” IEEE Design & Test, vol. 41, no. 1, pp. 40–49, 2024. [29] F. Kaiser, S. Kosnac, and U. Brüning, “Development of a RISC-V- [5] “RISC-V sail model,” https://github.com/riscv/sail-riscv. conform fused multiply-add floating-point unit,” Supercomputing Fron- [6] A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray, R. M. tiers and Innovations, vol. 6, no. 2, pp. 47–56, 2019. Norton, P. Mundkur, M. Wassell, J. French, C. Pulte, S. Flur, I. Stark, [30] T. Lu, A. Liu, B. Xia, and P. Liu, “Comprehensive RISC-V floating- N. Krishnaswami, and P. Sewell, “ISA semantics for ARMv8-a, RISC- point verification: Efficient coverage models and constraint-based test v, and CHERI-MIPS,” in Symposium on Principles of Programming generation,” in Design, Automation and Test in Europe Conference Languages (POPL 2019), 2019. (DATE), 2025, pp. 1–7. [7] M. Schlägl and D. Große, “Single instruction isolation for RISC- [31] Imperas, “riscvovpsim,” https://github.com/riscv-ovpsim/ V vector test failures,” in IEEE/ACM International Conference on imperas-riscv-tests, 2025. Computer-Aided Design (ICCAD), 2024, pp. 156:1–156:9. [8] M. Schlägl, J. Reichhardt, and D. Große, “From generation to failure categorization: An open-source automated RTL verification framework for RVV,” in ACM Great Lakes Symposium on VLSI (GLSVLSI), 2026, pp. 622–629. [9] K. Ruep, M. Schlägl, and D. Große, “Late breaking results: Float fight – verifying floating-point behavior in RISC-V simulators,” in Design, Automation and Test in Europe Conference (DATE), 2026, pp. 1–3. [10] J. R. Hauser, “Berkeley SoftFloat,” https://github.com/ucb-bar/ berkeley-softfloat-3. [11] N. Zurstraßen, N. Bosbach, and R. Leupers, “FloppyFloat: An open source floating point library for instruction set simulators,” in Design, Automation and Test in Europe Conference (DATE), 2025, pp. 1–6. [12] “RISC-V ISA simulator (spike),” https://github.com/riscv-software-src/ riscv-isa-sim. [13] M. Schlägl, C. Hazott, and D. Große, “RISC-V VP++: Next generation open-source virtual prototype,” in Workshop on Open-Source Design Automation (OSDA), 2024. [14] M. Schlägl and D. Große, “Fast interpreter-based instruction set simu- lation for virtual prototypes,” in Design, Automation and Test in Europe Conference (DATE), 2025, pp. 1–7. [15] “QEMU a generic and open source machine emulator and virtualizer,” https://www.qemu.org, 2025. [16] M. Cavalcante, F. Schuiki, F. Zaruba, M. Schaffner, and L. Benini, “Ara: A 1-GHz+ scalable and energy-efficient RISC-V vector processor with multiprecision floating-point support in 22-nm FD-SOI,” IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 28, no. 2, pp. 530–543, 2020. [17] C. Tain, S. Patil, and H. Al-Asaad, “Survey of verification of RISC-V processors,” Journal of Electronic Testing, vol. 41, pp. 111–138, 2025. [18] V. Herdt, D. Große, and R. Drechsler, “Towards specification and testing of RISC-V ISA compliance,” in Design, Automation and Test in Europe Conference (DATE), 2020, pp. 995–998. [19] V. Herdt, S. Tempel, D. Große, and R. Drechsler, “Mutation-based compliance testing for RISC-V,” in Asia and South Pacific Design Automation Conference (ASP-DAC), 2021, pp. 55–60. [20] V. Herdt, D. Große, E. Jentzsch, and R. Drechsler, “Efficient cross-level testing for processor verification: A RISC-V case-study,” in Forum on Specification and Design Languages (FDL), 2020, pp. 1–7. [21] N. Bruns, V. Herdt, E. Jentzsch, and R. Drechsler, “Cross-level processor verification via endless randomized instruction stream generation with coverage-guided aging,” in Design, Automation and Test in Europe Conference (DATE), 2022, pp. 1123–1126. [22] L. Klemmer and D. Große, “EPEX: processor verification by equiv- alent program execution,” in ACM Great Lakes Symposium on VLSI (GLSVLSI), 2021, pp. 33–38. [23] F. Riese, V. Herdt, D. Große, and R. Drechsler, “Metamorphic testing for processor verification: A RISC-V case study at the instruction level,” in International Conference on Very Large Scale Integration of System- on-Chip (VLSI-SoC), 2021, pp. 1–6. [24] M. Chupilko, A. Kamkin, and A. S. Protsenko, “Open-source validation suite for RISC-V,” in 2019 20th International Workshop on Micropro- cessor/SoC Test, Security and Verification (MTV), 2019, pp. 7–12. [25] “RISCV-DV,” https://github.com/google/riscv-dv, 2024.