Skip to content
STIMSMITH

SOURCE ARCHIVE

SHA256: f84d843e79f959b166d3e54335f8c60367577938360ce02a3fc4d54a8250354e
TYPE: application/pdf
SIZE: 1366.8 KB
FETCHED: 7/19/2026, 10:08:21 PM
EXTRACTOR: liteparse
CHARS: 68,151

EXTRACTED CONTENT

68,151 chars

Single Instruction Isolation for RISC-V Vector Test Failures

                           Manfred Schlägl                                               Daniel Große
                    Institute for Complex Systems                               Institute for Complex Systems
                      Johannes Kepler University                                  Johannes Kepler University
                            Linz, Austria                                               Linz, Austria
                       manfred.schlaegl@jku.at                                       daniel.grosse@jku.at

ABSTRACT However, this approach is not feasible any more for two reasons: Testing complex RISC-V extensions such as RISC-V Vector (RVV) (i) more comprehensive tests are needed, and (ii) the complexity of with its 600+ highly configurable instructions is crucial. For this the instruction sets increases. Consequently, there has been a push reason, test suites have been developed over the last years, including towards the development of automated test generation techniques, both hand-written and automatically generated tests. Although also referred as Instruction Sequence Generators (ISGs), to facilitate the process of running these tests is often highly automated, a exhaustive verification processes. Notable methods include the use significant portion of the work, namely the result analysis, has to of constraint solving techniques, guided random generation, quick be conducted manually after the run. error detection and equivalent program execution. More details are This paper introduces the modular, open-source framework given in our discussion of related work in Section 2. RVVTS for positive and negative testing of RVV implementations, Let us now specially look on the complexity challenge introduced featuring a novel technique called Single Instruction Isolation with by the RISC-V "V" Vector Extension (RVV) with its 600+ instructions. Code Minimization, which significantly reduces manual result anal- RVV allows to efficiently handle data-heavy and parallel processing ysis of failing tests. We demonstrate the effectiveness of RVVTS by tasks, making it highly adaptable for advanced applications in ma- automatically generating and applying test sets to the RISC-V VP++ chine learning, multimedia, and scientific computing. In contrast to Virtual Prototype and the QEMU emulator, achieving a functional the simple integer add example from above, the behavior of an RVV coverage of >94%. For RISC-V VP++, our framework detects and instruction depends not only on directly passed parameters, but minimizes ~1, 849 failures and associate them with 10 isolated, fail- also upon the dynamic configuration and, thus, the architectural ing instructions. Similarly, for QEMU , it detects ~19k failures and state. For example, a RVV add instruction may behave differently relates them to 168 instructions for debugging. Overall, we con- not only wrt. the directly passed parameters, but also wrt. the firmed 3 new bugs in the RISC-V VP++ and 2 in QEMU (and 7 more previously set vector length, dynamic type (8, 16, 32, 64 bit), etc. are to be analyzed). Thus, the parameter space becomes high dimensional, which makes manual test creation no longer efficient. For this reason, dedicated 1 INTRODUCTION ISGs and pre-generated test sets have been developed over the last RISC-V [39, 40], an open standard Instruction Set Architecture (ISA), years. One example is RISCV-DV , which was originally developed embodies flexibility and scalability, enabling the precise tailoring of by Google [9]. However, this ISG does not support the ratified ver- processor capabilities to meet diverse application needs without the sion 1.0 of RVV. Another example, which overcomes this problem, constraints of unnecessary features inherent in proprietary ISAs. is FORCE-RISCV , maintained by the OpenHW Group [5]. It provides RISC-V supports a range of optional extensions, such as those for an ISG for generating extensive tests and the reference simulator floating-point operations, atomic instructions and vector process- Handcar which generates execution traces for these tests. The ob- ing, enabling further customization and optimization. Each of these tained execution traces can then be compared with traces generated extensions adds a layer of functionality that must be thoroughly by a comparative run on a Device Under Test (DUT). However, a sig- tested. The verification process typically involves creating specific nificant portion of work, the analysis of the trace differences, is test sets that can handle the complexities introduced by these ex- left to the user. This analysis is largely manual work and involves tensions. Although still challenging, testing of simple instruction finding differences, eliminating irrelevant details and isolating in- sets, for example RISC-V base integer, is a well understood problem. structions, errors and states in a vast amount of traces. For example, the behavior of a simple integer add instruction may Thus far, we focused on testing with the emphasis on checking only depend on the parameters directly passed to the instruction. that instructions work as expected, called positive testing. However, The parameter space is manageable and it may be even feasible to we must also consider possibly unexpected/undesired behavior hand-craft tests for such instruction sets. The RISC-V compliance when the DUT is exposed to invalid instructions. This kind of test suite also exemplified this, being crafted by hand when it came testing is referred to as negative testing [22]. Let us now examine out [1]. the Instruction Register (IR) of a processor which stores the current instruction word to be executed. Then, for negative testing, it is necessary to distinguish between the following cases: This work is licensed under a Creative Commons Attribution International 4.0 License. • Invalid instruction word: The instruction word is not defined by any (custom) RISC-V extension. ICCAD ’24, October 27–31, 2024, New York, NY, USA • Invalid instruction because of unsupported extension: The © 2024 Copyright held by the owner/author(s). instruction is specified but not supported by the RISC-V core ACM ISBN 979-8-4007-1077-3/24/10 https://doi.org/10.1145/3676536.3676755 at hand.

ICCAD ’24, October 27–31, 2024, New York, NY, USA Manfred Schlägl and Daniel Große

• Invalid instruction because of temporarily disabled exten- focus on the novel technique, namely Single Instruction Isolation sion: For example, the instruction considers floating-point, with Code Minimization. The case studies are described in Section 5. but floating-point is temporarily disabled (done via the Finally, the paper is concluded in Section 6. Control and Status Register (CSR) mstatus). 2 RELATED WORK • Invalid instruction because of dynamic configuration: A good example is the RVV element type set to 8 bit and the current Generating tests for processors is an intensively studied research instruction performs a RVV floating-point operation (there field. For automation and efficiency, a major step was made by is no support for 8 bit floating-point elements). separating the description of the processor architecture from test • Invalid because of parameter(-values): Consider for instance generation. The approaches in [14, 16] achieved this by employing a RISC-V load instruction that is issued with a invalid load constraint solving techniques on constraints that capture the archi- address. tectural description and testing-knowledge. Test generation was fur- As we can see, the number of dimensions in the parameter space ther improved in [30] by sharing information between constraints increases further, which makes the process of testing even more solutions among multiple instructions. To increase coverage, the ap- complex. This has two major implications: (i) the ISGs must be able proach introduced in [17] formed a coverage model via constraints to generate also invalid state, instruction and parameter combina- describing execution paths of individual instructions. Also Bayesian tions in a systematic way, and (ii) the already challenging analysis networks have been used with the same goal [20]. Furthermore, of the test results becomes much harder due to increased number machine learning approaches emerged, for instance [15, 28] and of parameters and combinations to be considered. We address both also fuzzing, e.g. [27, 32]. However, all these approaches do not challenges in this work. support RVV, focus only on positive testing, and for failing tests Contribution: In this paper, we present the modular, open-source the manual analysis effort to trace down the root cause would be framework RVVTS for positive and negative testing of RVV, where far too high. at the heart is our novel Single Instruction Isolation with Code Mini- Besides this, also RISC-V specific approaches have been devel- mization technique. Besides efficient test generation, RVVTS allows oped. One of the first RISC-V ISGs was the Torture Test frame- to reduce manual result analysis of failing tests significantly. The work [2] based on Scala. RISC-V International hosts the Architec- framework supports automation of the full verification chain: ture Test Special Interest Group which provides the architectural (1) grammar-based, coverage-guided ISG, tests [7]. These tests constitute a basic suite that evaluates critical (2) instrumentation and build, components of the specification without an in-depth focus on finer (3) measurement of functional coverage, details and has been generated using constraints. Another approach (4) execution on reference simulator and DUT, was Google’s RISCV-DV [9], mentioned in Section 1. It utilizes Sys- (5) detection of differences in architectural states (fails), temVerilog alongside the Universal Verification Methodology (UVM) (6) isolation of the failing instruction (Single Instr. Isolation) and, to continuously generate RISC-V instruction sequences solving (7) creation of minimized failing test case (Code Minimization). constrained-random specifications. However, it does not support In addition, the framework can be used interactively in Jupyter RVV 1.0; the basic applicability was nevertheless shown in [29], but notebooks to support the user in tracing causes of detected fails. the effort for result analysis has already been recognized for positive In our case studies, we demonstrate the effectiveness of RVVTS. testing. Recall, that the aforementioned argument is also one major We use use the framework to generate ready-to-use test sets for problem for FORCE-RISCV . As we will show in the experiments, positive and negative testing of RVV implementations for RV32 there is an enormous amount of failed RVV tests if we consider and RV64, respectively. Each test set achieves a functional coverage both, positive and negative testing where a manual inspection is of over 94%. practical infeasible (150k+ deviations in our case study, Section 5.2). The tests sets are applied on two DUTs implementing RVV in Test generation for Instruction Set Simulators (ISSs) leveraging its ratified version 1.0, namely the open-source SystemC [4, 23] coverage-guided fuzzing has been targeted in [22, 26]. A formal TLM based RISC-V VP++ [33, 35, 36] Virtual Prototype (VP) and the constraint-based specification approach has been presented in [24]. open-source QEMU emulator [6]. Based on the obtained results, The paper [25] introduced an efficient cross-level testing approach we discuss the differences of positive and negative testing, and for ISS vs. RTL models which generates an endless instruction demonstrate the Single Instruction Isolation with Code Minimiza- stream on-the-fly during simulation. However, all these approaches tion technique. We show, for example, that we can automatically neither target RVV nor provide solutions for large number of failing minimize about 152k detected fails in the initial version of the VP test cases. and associate them with 542 isolated, failing instructions. For both An entirely different approach is formal verification, as func- DUTs, we perform a result analysis and discuss several previously tional behavior is proven. Prominent examples employing model undetected bugs. All newly found bugs are reported to the respec- checking techniques are riscv-formal [8] and Siemens EDA’s One- tive open-source projects. RVVTS, as well as the pre-generated test Spin tools [12]. riscv-formal does not support RVV, and the OneSpin sets are available as open-source on GitHub1 . tools are only commercially available. Originally designed exclu- The paper is structured as follows: First, in Section 2 we discuss sively for post-silicon verification, Quick Error Detection (QED) has related work. Thereafter, in Section 3, we briefly review RVV. In been further extended and used for pre-silicon verification [37]: it Section 4, we introduce the RVVTS framework with a particular is referred to as Symbolic Quick Error Detection (SQED), leverages Bounded Model Checking (BMC) techniques and has been applied 1https://github.com/ics-jku/RVVTS to RISC-V processors [18] and hardware accelerators [38]. The core

Single Instruction Isolation for RISC-V Vector Test Failures ICCAD ’24, October 27–31, 2024, New York, NY, USA

idea of SQED is to symbolically check whether the outputs from 4 THE RVVTS FRAMEWORK executing a specific instruction sequence are consistent when the The modular RVVTS framework is developed in Python and supports sequence is run twice, provided that the inputs for both executions integration with Jupyter notebooks. This gives the framework the are identical. The work in [31] introduced EPEX where for a given flexibility to support automated processes, such as running long test program an equivalent test program is generated using SMT. series of tests, as well as semi-automated, interactive use cases, Then, both programs are executed on two instances of the same pro- such as tracing specific issues. cessor design and the programs have to produce equal architectural states. Although formal methods offer guarantees of correctness, 4.1 Fundamental Data Structures they may suffer from scalability issues. In case of RVV, this problem is even harder as (i) very wide datapath operations typically have A central data structure of RVVTS is the Machine State, which to be performed and (ii) due to the dynamic configuration of the holds the architectural state relevant to all supported extensions. RVV instructions. The Machine State holds values of all involved registers (integer, Finally, there is the formal specification of the RISC-V ISA writ- floating-point, vector, and CSR), a trap counter, the last executed ten in Sail [10]. While the model provides the ultimate truth, cur- Program Counter (PC) address and hashes for memory areas. The rently the RVV part is still under development. If it becomes avail- data structure supports extraction from a RISC-V machine, modifi- able, we can easily integrate a reference simulator generated from cation and comparison, and includes a generator for code to bring the Sail model. a RISC-V machine to that state. For example, the framework can execute a program A on a RISC-V machine and extract the Machine 3 THE RISC-V "V" Vector Extension (RVV) State. It then can modify parts (e.g. register value) of the Machine Performance of algorithms used in image and video processing, au- State, generate the initialization code, integrate this code in an- dio manipulation, scientific simulations, and modern AI algorithms other program B and execute this program on a RISC-V machine. can be significantly increased by exploiting Data-Level Parallelism Program B would then behave as if it had run immediately after (DLP). One way to achieve this are Single Instruction, Multiple Data program A, but with the introduced change in the Machine State. (SIMD) instruction set extensions. SIMD operates by executing iden- Other key data structures are the Code Block and the Code Frag- tical operations on multiple data elements simultaneously, known ment, which are used by RVVTS to organize and handle assembler as a Vector. Initially conceived in the 1970s [21], SIMD gained code. A Code Fragment is a indivisible sequence of at least one traction in supercomputing systems pioneered by Cray, evolving assembler instruction implementing an operation. For example a into what we now recognize as vector architectures [19]. Code Fragment for a RVV add operation contains a single vector Processors have included SIMD instructions for about 25 years, add assembler instruction. A Code Fragment for a RVV bounded categorized as multimedia extensions like Intel MMX, SSE, AVX, load/store operation [34] contains multiple assembler instructions or ARM Neon. To simplify Hardware (HW) implementation, these to realize the bounding and a vector load/store instruction. classical SIMD extensions operate with fixed-size registers (vector A Code Block contains a sequence of Code Fragments and forms length). The vector length and element types are specified in the an entity that can be executed on a RISC-V machine by RVVTS. ISA and encoded directly in instructions. This has implications on The data structure provides various methods to modify the con- scalability, since every change of the vector length means changes tained code, retrieve sub-blocks, save/load to/from files, etc. Code in the ISA and previously compiled code cannot take advantage of Blocks can either be created manually, loaded from files, or cre- the larger vectors. In contrast, vector architectures such as RVV are ated automatically by the ISG or through Code Minimization by a more general. Instead of having a fixed vector length and types the framework. The latter two will be discussed in the upcoming encoded in instructions, such architectures have have dynamic Section 4.2 and Section 4.4. vectors and generic instructions. The vector length and the type of the elements are set dynamically with dedicated instructions 4.2 The Grammar-based ISG at runtime. Software (SW) can detect and utilize the maximum RVVTS comes with a grammar-based ISG for 32 bit (RV32) and 64 available vector length provided by the HW at runtime. bit (RV64) RISC-V configurations. The ISG provides support for the The ratified version 1.0 of RVV, specified in [3], adds the follow- base integer (I) and the RVV extensions, which is the focus in this ing parts to the RISC-V programming model: (i) 32 Vector registers, work. Furthermore the generator partially supports floating-point (ii) 7 CSRs, and (iii) 624 instructions. The length of the RVV regis- (F/D) as far as necessary to handle RVV floating-point. ters, VLEN, is not fixed in the ISA, but can be chosen by the designer. The ISG uses a context-free grammar to create syntactically valid In addition, registers can be grouped at runtime to increase the max- instruction sequences. The grammar consists of non-terminal and imum available vector size at the expense of a smaller number of terminal symbols. When invoked, the generator randomly selects usable registers. The 624 instructions can be categorized in configu- expansion candidates for non-terminal symbols until only terminal ration, load/store and processing. Configuration instructions, such symbols remain. The result is returned as Code Fragment. as vsetvli set the dynamic type and vector length. The extensive Context-free grammars are highly efficient for generating simple set of load/store instructions can efficiently handle even complex sequences. However, the expressiveness of such grammars is too data structures (gather/scatter). The processing instructions cover limited when it comes to more complex sequences. One example operations on integer, fixed point and floating point data types. In of this is the generation of bounded values, possibly even dynami- addition, RVV specifies vector reduction (e.g. sum, min, max, . . . ) cally parameterized, such as the generation of an address in a spe- and permutation (e.g. move, shift, . . . ) instructions. cific range. More complex examples are (address-range) bounded

ICCAD ’24, October 27–31, 2024, New York, NY, USA    Manfred Schlägl and Daniel Große

= Es Gm 1 =i | ee [> =p eri

==

=

  em



    Figure 1: CodeErrMinRunner

load/store operations, which consist of multiple instructions de- memory, (ii) the target can be stopped when reaching a specified pendent on each other. To handle such cases efficiently, we extend PC position (e.g. breakpoint), and (iii) the targets architectural state the context-free grammar with special function symbols associated can be extracted (e.g. memory dump). One way to handle these with Python functions. The ISG expands such function symbols by requirements is by utilizing the framework’s generic GNU Debugger calling the associated function, which can provide context-sensitive (GDB) client Runner. This GDBRunner is able to connect to any expressiveness. The result of the function is then integrated in the targets providing a GDB Remote Debug Protocol (RDB) interface and generated Code Fragment. In our ISG, functions are for example is also used by the Execution Runners for RISC-V VP++ and QEMU . used to generate immediate values, register allocations, valid values There is also another, special form of Execution Runner that for CSRs and bounded load/stores. is used to measure the functional coverage of the given binaries. 4.3 RVVTS’s Building Blocks: Runners This Execution Runner uses the free, but closed-source riscvOVPsim simulator from Imperas [11]. The riscvOVPsim functional coverage The RVVTS framework is designed in modular, object oriented metric for RVV measures the use (hits) of specified RVV instructions design paradigm with expandability in mind. Central elements of and their parameters. The maximum number of points of this metric the framework are the so called Runners. consists of hits on instructions, all possible integer, floating-point Basic Runners handle fundamental tasks as process execution, and vector register addresses, and positive/negative integer register timeout handling, logging and archiving of results. Extended Run- and immediate values. ners add specific functionality to the framework and are created RefCovRunner takes a ELF binary as input and uses the Execution by specializations and aggregations of basic and other extended Runners for Spike and riscvOVPsim to provide the Machine State Runners. All Runners are controlled via central configuration data and functional coverage values. structure, that contains target definitions (e.g. RISC-V configuration, CodeCheckRunner takes a Code Block as input. It first uses a memory map) and other Runner specific settings. In the following, BuildRunner for instrumentation and build. The resulting ELF bi- we provide a brief overview of the most important low- and mid- nary is then fed into a RefCovRunner which provides the Machine level Runners with regard to this paper. State and functional coverage values of the executed Code Block. BuildRunner takes a Code Block and a Machine State. The Runner CodeCompareRunner also takes a Code Block as input and uses creates a instrumented program (e.g. initialization with given Ma- the BuildRunner for instrumentation and build. The resulting ELF chine State, trap counting, dump of Machine State after execution) binary is fed in a RefCovRunner and any other given Execution and invokes a compiler to create a Executable and Linkable Format Runner , called DUT Runner in this context. The Runner provides a (ELF) binary. comparison of the resulting Machine States and also the functional Execution Runners take a ELF binary, execute that binary on a coverage values of the executed Code Block. specified target and extract the Machine State after the run. At the time of writing, RVVTS comes with Execution Runners to run Spike, 4.4 Single Instruction Isolation with Code which is used as a golden reference model, and RISC-V VP++ and QEMU as supported DUTs. Spike is the official RISC-V reference Minimization simulator maintained by RISC-V International [13]. Next, we focus on the CodeErrMinRunner which implements Support for other SW targets (e.g. simulators, emulators) or even our novel Single Instruction Isolation with Code Minimization tech- HW targets can be introduced by adding new Execution Runners. nique. The Runner is shown in Figure 1. We first consider the upper Requirements for new targets are, that (i) the target can be started part of the figure. The Runner takes a Code Block and first uses a up in a controlled way with a given ELF binary and zeroed-out CodeCompareRunner to determine, if there are any deviations in

Single Instruction Isolation for RISC-V Vector Test Failures ICCAD ’24, October 27–31, 2024, New York, NY, USA

Algorithm 1 Delta Code Reduction: Binary Search Algorithm 4.5 Coverage Guided Test Set Generation Input: Failing Code Block With the CovGuidedTestsetGenerator, the RVVTS framework pro- 1: Output: Position of the first failing Code Fragment. vides a Runner able to generate dense Code Blocks with high func- 𝑏𝑎𝑑 ← codeblock.len() 2: 𝑔𝑜𝑜𝑑 ← 0 tional coverage. Multiple, independent instances of these Runners 3: 𝑡𝑒𝑠𝑡 ← codeblock.len() can be used in parallel to generate large sets of such Code Blocks. 4:5: whileif (𝑏𝑎𝑑 − 𝑔𝑜𝑜𝑑) > 1 do Such sets are particularly useful for testing, as we will demonstrate CodeCompareRunner.run(codeblock.subpart(0, test)) == FAIL then 6: 𝑏𝑎𝑑 ← 𝑡𝑒𝑠𝑡 in our case studies in Section 5. 7: 𝑡𝑒𝑠𝑡 ← 𝑡𝑒𝑠𝑡 − ( (𝑏𝑎𝑑 − 𝑔𝑜𝑜𝑑)/2) ⊲ Reduce by half search area The generator uses the grammar-based ISG from Section 4.2 and 8:9: else𝑔𝑜𝑜𝑑 ← 𝑡𝑒𝑠𝑡 the CodeCheckRunner, presented in Section 4.3. The generation pro- 10: 𝑡𝑒𝑠𝑡 ← 𝑡𝑒𝑠𝑡 + ( (𝑏𝑎𝑑 − 𝑔𝑜𝑜𝑑)/2) ⊲ Extend by half search area cess starts with an empty Code Block with zero functional coverage 11: return 𝑏𝑎𝑑 and consists of two alternating phases: (i) The Extension phase, in the Machine State. If not, the run is considered a pass, the results which the Runner tries to extend the Code Block with new Code (e.g. functional coverage values) are documented and the run is Fragments to improve coverage, and (ii) and the Reduction phase, complete. In case of a Machine State deviation, the run is considered in which the Runner tries to densify the Code Block by removing a fail. The results, including the failing Code Block, are documented, Code Fragments without hurting coverage. Switching between these and the Code Block is given to the Delta Code Reduction stage. phases is determined by a configurable number of iterations for Delta Code Reduction is seen in the mid part of Figure 1. In this each phase. The process can be stopped at any iteration by the reduction stage, the fail in the Code Block is isolated using a binary program that instantiated the Runner. Typical examples of this search technique presented in Algorithm 1. The algorithms keeps are stopping after a certain number of iterations or time, or after track of the last found good and bad code positions, and a current test reaching a certain coverage value. code position. In each iteration, a sub-part of the Code Block starting We will now look at the two phases in more detail. At each from 0 to the test position is executed using a CodeCompareRunner. iteration of the Extension phase, the ISG generates a new Code The result is checked for a fail, the code positions are updated Fragment, which is inserted at a random position in a copy of the accordingly and the search area is halved for the next iteration. current Code Block. This new Code Block is then instrumented, The algorithm stops once it has found the earliest single bad Code compiled and executed by a CodeCheckRunner, which returns a Fragment, which is located at the bad position. The results of the Machine State and the coverage value. These results must meet two last run and the reduced failing Code Block, are documented. requirements: (i) The Machine State must be valid, which will be The Delta Code Reduction stage results in a reduced Code Block discussed below in more detail, and (ii) the coverage obtained for consisting of a number of non-failing Code Fragments and a single the new Code Block must be maintained or improved compared to failing Code Fragment at the end. Based on this information, it is the original Code Block. If one of these requirements is not met, the already possible to isolate a single failing instruction (the last Code new Code Block is rejected and the original Code Block is used in Fragment). However, the Code Block may still contain many more the next iteration. If all requirements are met, the new Code Block Code Fragments, which makes analysis difficult. The Code Block is is used for for the next iteration. therefore given to a final stage, the Code Minimization, seen in the At each iteration of the Reduction phase, a random Code Fragment lower part of Figure 1. In this stage, the Code Block is split into two is removed from a copy of the current Code Block. Also in this separate blocks: The first Code Block contains all, non-failing Code phase, the new Code Block is executed via a CodeCheckRunner. The Fragments just before the failing fragment. The second Code Block results are checked for similar requirements as above (validity and contains only the last failing Code Fragment. coverage), with one important difference: The coverage obtained The first block is executed by a CodeCheckRunner to extract the for the new Code Block must stay the same wrt. the original Code Machine State after execution of the non-failing fragments. The Block. Again the new Code Block is only used for the next iteration, initialization code generated from this Machine State is then com- if these requirements are met. bined with the second Code Block containing only the single failing The validity property mentioned above consists of at least the fragment. The result is a much easier to analyze minimized Code minimum requirements that the generated Code Block must be Block containing only the Machine State initialization and a single compilable and executable. However, additional requirements are failing Code Fragment. In a final step, this minimized Code Block configurable. At the time of writing, the only configurable property is executed by a CodeCompareRunner to obtain the final results. is a Boolean switch that controls whether the resulting Code Block These results and the minimized Code Block are then documented. is allowed to cause traps in the execution. As we will see in our case An important variant derived from the CodeErrMinRunner is the studies below, in Section 5, such a switch is crucial for generating TestsetCodeErrMinRunner, which is used to run pre-generated test sets targeted for pure positive, and positive/negative testing. test sets in our case studies, in Section 5. TestsetCodeErrMinRunner 5 CASE STUDIES executes a series of Code Blocks provided as the files and collects In this section, we demonstrate the effectiveness of RVVTS and all obtained results. The Runner takes a path and a file matching the novel Single Instruction Isolation with Code Minimization tech- pattern as input. Files matching the given pattern are loaded as nique. First, in Section 5.1, we present four test sets generated with Code Block and executed as described above. The results of all fails, CovGuidedTestsetGenerator (Section 4.5), that can be used in the including the reduced and minimized Code Blocks are documented verification process of RV32 and RV64 based RVV implementa- for later analysis. tions. After this, we use the TestsetCodeErrMinRunner (Section 4.4)

ICCAD ’24, October 27–31, 2024, New York, NY, USA Manfred Schlägl and Daniel Große

Table 1: Test Sets pre-generated with CovGuidedTestsetGenerator
                                                                                                               Functional Coverage
                                  RISC-V     Million                        Million                            (riscvOVPsim RVV)

Test set Config Code Fragments RVV Instr. Points Percent Valid Sequences (VS) RV32 1.78 1.25 30,500 / 31,894 95.63 RV64 1.69 1.21 31,410 / 33,076 94.96 Invalid+Valid Sequences (IVS) RV32 1.70 1.31 30,919 / 31,894 96.94 RV64 1.64 1.26 31,952 / 33,076 96.60 Merged Sequences (MS) RV32 3.49 2.56 30,920 / 31,894 96.95 (VS + IVS) RV64 3.33 2.47 31,952 / 33,076 96.60

including Single Instruction Isolation with Code Minimization to Table 2: Test Sets executed on RISC-V VP++ apply the pre-generated test sets on two DUTs. The first DUT, RISC-V VP Detected Isolated Failing RISC-V VP++ [36] is considered in Section 5.2. The second DUT, Test set Config Version Fails Instructions QEMU [6], is covered in Section 5.3. For both DUTs, we perform a RV32 initial N/A N/A result analysis and discuss previously undetected bugs. All newly VS latest 1,656 9 found bugs are reported to the respective open-source projects. RV64 initial 39,842 409 latest 1,301 9 5.1 Pre-Generated Testsets RV32 initial N/A N/A IVS latest 195 9 We use the CovGuidedTestsetGenerator, presented in Section 4.5 to RV64 initial 112,015 539 generate four test sets by varying two configuration settings: (i) latest 183 9 the RISC-V configuration (RV32, RV64), and (ii) the Boolean switch, RV32 initial N/A N/A that controls whether the generated test sets are allowed to contain MS latest 1,849 10 instruction sequences that trigger traps when executed. RV64 initial 151,857 542 latest 1,484 9 The former, the RISC-V configuration is varied to enable support for testing RV32 and RV64 DUTs and thus to extend the usability with support for RVV, presented in [36]. (ii) The latest version of of the pre-generated test sets. The latter switch enables support RISC-V VP++ at the time of writing (git commit hash c354bfea). Due for different test strategies, namely having separate test sets for to a fundamental bug related to the integration of RVV in the initial pure positive testing, containing only Valid Sequences (VS) and version of the RV32 VP variant, the results of the test runs are not positive/negative testing, containing Invalid+Valid Sequences (IVS). valid for this case and are therefore listed as N/A in the table. For the generation of all test sets, the following global configu- For each run, Table 2 shows the overall number of detected fails ration is chosen: (i) At least 3 MiB read/writeable memory located and the number of isolated, unique RVV instructions causing these at address 0𝑥 80020000 is expected. The memory is partitioned in these fails. As explained in Section 4.4, a fail is defined as deviating a 1, 536 KiB code, a 10 KiB dump (Machine State) and a 1, 526 KiB Machine State extracted after execution on a reference simulator data area. Generated bounded loads can access the full memory (Spike) and the DUT. area, while generated bounded stores can only access the data area. First, we focus on the differences from the initial to the latest (ii) Code is generated for RVV implementations with a VLEN of up RV64 VP version on a high level. It can be seen, that the number of to 512 bits and a ELEN of 64 bits. detected deviations and identified instructions drops significantly Table 1 summarizes the major characteristics of (i) the four gen- from the initial to latest VP version. This is not surprising due to erated test sets with Valid Sequences (VS) and with Invalid+Valid the fact that the latest version contains 42 RVV related bug fixes Sequences (IVS) for RV32 and RV64, respectively, and (ii) the merged compared to the initial version. These 42 fixes can be roughly clas- test sets with Merged Sequences (MS) (i.e. VS + IVS), for RV32 and sified in three categories: (i) 6 fixes are related to the integration RV64, respectively. For each test set, the table shows the number of of RVV in the RV32 and RV64 ISSs (e.g. access to RVV CSRs), (ii) generated code fragments, the number of generated RVV instruc- 11 fixes are related to the function of specific RVV instructions or tions, and the achieved RVV functional coverage. As can be seen in instruction groups (e.g. incorrect result for vector remainder, . . . ), Table 1, all test sets reach a functional coverage above 94%. and (iii) 25 fixes are related to handling illegal parameter combi- The pre-generated test sets can be used to test RV32 and RV64 nations or configurations for RVV instructions (e.g. invalid type based RVV implementations and are available as open-source on settings, use of invalid registers, . . . ). GitHub. Bugs in the first category usually have a major impact and their 5.2 RISC-V VP++ effects can be seen quickly in tests. For example, a generic bug in floating-point handling can affect the behaviour of many floating- In this case study, we consider the recently released RISC-V VP++ point instructions. However, bugs in this category are often hard to with support for RVV 1.0. We use the TestsetCodeErrMinRunner to track down due to their generic effects. With respect to our results apply the test sets generated in Section 5.1 on different variants in Table 2, such kind of bugs can be detected equally well with the and versions of the VP. VS and IVS test sets. Table 2 shows the result of the application of the RV32 and Bugs in the second category are related to the function of specific RV64 VS, IVS and MS test sets on RISC-V VP++. We obtained results RVV instructions or instruction groups. For example, incorrect for two versions of the VP: (i) The initial version of RISC-V VP++ results of a RVV remainder instruction for certain parameter values.

Single Instruction Isolation for RISC-V Vector Test Failures ICCAD ’24, October 27–31, 2024, New York, NY, USA

Bugs of this kind can also be detected with the VS and IVS test Table 3: Test Sets executed on QEMU (git hash 02e16ab9f4) sets. However, since the VS test set is likely to contain more valid RISC-V Detected Isolated Failing parameter combinations for RVV instructions than a IVS test set Test set Config Fails Instructions of roughly the same size, the VS test set is more suited to detect VS RV32 10,575 114 such kind of bugs. This can also be seen in Table 2 for the initial VP. RV64 6,548 112 For the VS and IVS test sets, we can identify 409 and 539 unique IVS RV32 8,667 167 instructions causing fails, respectively. However, for the merged RV64 8,463 166 MS test set we can identify 542 unique instructions causing fails. MS RV32 19,242 168 This means, that 542 − 539 = 3 instructions were identified only RV64 15,011 166 with the VS test set containing valid sequences. Bugs in the third and last category are related to illegal parameter which offer more freedom regarding the order of processing ele- combinations or configurations. The functionality of RVV instruc- ments. While the former brings the advantage of comparability tions is heavily dependent on the architectural state. Two prominent and reproducibility, the latter may offer advantages in terms of examples for this are dynamic typing and register grouping. An ex- performance. However, RVV also specifies, that ordered implemen- ample of the former, floating-point operations on 8 bit elements, tations are also valid unordered implementations. This fact is ex- was already presented in Section 1. The latter, register grouping, is ploited by the developers of RISC-V VP++, where vfredusum.vs a special feature of RVV to group the 32 available vector registers and vfwredusum.vs use the exact same implementations as together to either 16, 8 or 4 registers with 2, 4 or 8 times the size of vfredosum.vs and vfwredosum.vs, respectively. As this is a single register. For example, if register grouping is not used, the not the case for the reference simulator Spike, some results of the instruction vadd v0, v1, v2 is valid. If register grouping is set operations differ and are identified as fails by RVVTS. However, to 2, only even numbered registers are allowed. In this case, the since we have the minimized test cases and Machine States, it is easy exact same instruction is invalid and will cause a trap. to verify, that the unordered VP results match the ordered reference Instruction sequences containing illegal parameter combinations results. We semi-automatically replace the unordered variants with or configurations are by principle not included in the VS test set. the ordered variants in all generated minimized test cases and per- Bugs related to invalid sequences can only be detected with nega- form a re-run on the reference simulator. Comparing the resulting tive testing and hence with the IVS test set. This can also be seen Machine States with the states of the previous run on the VP shows in Table 2: By subtracting the number of instructions with fails no differences and therefore, all detected fails of vfredusum.vs detected by the VS test set (409) from the number detected by the and vfwredusum.vs are false-positives. merged MS test set (542), we get 542 − 409 = 133 instructions with The second type of potential bugs concerns conversion instruc- fails detected only by the IVS test set. tions of floating-point to/from integer with widening and narrow- We now focus on the results of the latest version of RISC-V VP++ ing result width (e.g. vfwcvt.f.x.v, vfncvt.x.f.w, . . . ). A in Table 2. Comparing the absolute number of fails detected by the quick analysis of the results of the corresponding minimized test VS test set (1, 656 and 1, 301), with the IVS test set (195 and 183), cases shows, that in all cases the VP has unexpected traps, while shows a large difference. The much lower values for the IVS test set the instructions are successfully executed on the reference simu- indicates, that most remaining problems in RISC-V VP++ are related lator. Since the VP can provide detailed output on causes of RVV to the first and second category described above. Overall, for the traps, and RVVTS automatically records all output of failed runs, we merged MS test set, we can observe 10 and 9 isolated instructions can easily track down the cause of all traps. Analyzing the output with fails for RV32 and RV64, respectively. By analyzing the au- shows that the cause of the traps is the same in all detected failures, tomatically generated minimized test cases and the difference of namely that half-precision floating-point is not supported. Since the extracted Machine States after the run, we can identify four half-precision floating-point is not used in any of the failing test types of potential bugs: (i) Deviations for floating-point reduction cases this must be a bug in RISC-V VP++. A code analysis of the operations, more specifically the unordered floating-point sums RVV implementation in RISC-V VP++ reveals that there is indeed a vfredusum.vs and vfwredusum.vs, (ii) Unexpected traps of faulty assertion related to detecting the use of the not-yet-supported floating-point to/from integer conversion operations, (iii) Unex- half-precision floating-point. pected traps and invalid results of vfrsqrt7.v, and (iv) Crashes of the VP related to vrem.vv. We will now analyze the first two 5.3 QEMU and most interesting types in detail. In this case study, we consider QEMU in its latest version at the time The first type can be identified as false-positive fail of the in- of writing, v9.0.0-rc3. First, we use the TestsetCodeErrMinRunner to structions vfredusum.vs and vfwredusum.vs, which are apply the test sets generated in Section 5.1 on RV32 and RV64 vari- specified to provide a sum of floating-point vector elements. It ants of the emulator. Then, we perform a result analysis leveraging is important to note that floating-point calculations are not asso- RVVTS and Single Instruction Isolation with Code Minimization. Fi- ciative. Consequently, the order in which elements are processed nally, we discuss a selection of interesting newly discovered bugs matters and can lead to different results. To avoid any potential in QEMU . ambiguities, RVV specifies two variants of these sum operations: Table 3 shows the results of the application of the RV32 and RV64 (i) the ordered variants, vfredosum.vs and vfwredosum.vs, VS, IVS and MS test stets on QEMU . For each run, the table shows which sums the values strictly in element order (0, 1, 2, . . . ), and (ii) the overall number of detected fails and the number of isolated, the unordered variants, vfredusum.vs and vfwredusum.vs, unique RVV instructions causing these these fails.

ICCAD ’24, October 27–31, 2024, New York, NY, USA Manfred Schlägl and Daniel Große

First, we focus on the difference between the VS (positive testing) Table 4: Result Analysis for QEMU and IVS (positive/negative testing) test sets. Subtracting the number RVV #Isolated #Minimized of failing instructions detected by the IVS test sets (167 and 166) Instruction Instructions Test Cases from the corresponding numbers of the merged MS test sets (168 Class (RV32/RV64) (RV32/RV64) Isolated Causes and 166), gives us 1 and 0 instructions for RV32 and RV64, which Load 80 / 78 4,492 / 3,285 RV32: 64 bit indices not supported Traps on first 4KiB of memory are detected only by the VS test sets with valid sequences. Similarly, Fractional lmul in QEMU allowed subtracting the number failing instructions of the VS test sets (114 Store 46 / 48 3,149 / 727 RV32: 64 bit indices not supported Fractional lmul in QEMU allowed and 112) from the MS test sets (168 and 166), gives us 54 instructions Reduction 16 / 16 7,095 / 6,714 Invalid behavior with vl=0 for RV32 and RV64, which are only detected by the IVS test sets Float widening 21 / 21 843 / 772 Invalid support for half-precision with invalid sequences. We can see that in the case of QEMU , the vset* 3 / 3 3,409 / 3,488 Extended support for fractional lmul IVS test sets, and therefore the negative tests, are very important. vslide1*.vx 2 / 0 226 / 0 RV32: Broken sign-extend of 32 to 64 bits We now focus on the failing instructions and perform a exem- plary analysis of the results and a cause analysis leveraging RVVTS be performed in these cases. Interestingly, the very similar vector and Jupyter notebooks. Please note that the workflow presented be- integer move instructions, which copy a scalar value from an inte- low is only one of many possible workflows supported by RVVTS. ger register (vmv.v.x) or an immediate (vmv.v.i) into a vector, (e.g.All failed instructions are classified according to their function behave as expected for negative values. load, store), or a main characteristic (e.g. float widening opera- The second bug discussed here concerns all RVV reduction in- tion). For each class, all generated minimized cases form a new test structions. As the name suggests, all these instructions reduce a set which is loaded and executed by RVVTS until the first fail. By vector to a single element. The vredsum.vs vd, vs2, vs1 studying the failing minimized test case and the resulting Machine instruction is an example for this. The instruction sums all elements State difference, assumptions of the cause and corresponding mea- in vector register vs2 and the first element of vector register vs1. sures are derived. These measures may include, for example, exper- The result is written to the first element of vector register vd. All imental fixes in the DUT, and semi-automatically applied adaption detected failing cases share one commonality: The vector length of test cases or result checks. After documenting the assumed cause (vl) is set to zero. The corresponding results show, that the refer- and implementing corresponding measures, the automated execu- ence simulator Spike does not perform a write to vd in these cases, tion of all minimized test cases is repeated. Depending on whether which is the correct behavior defined in the RVV specification. In the assumptions and measures are correct and whether all fails contrast, QEMU writes the value of the first element of vs2 to vd, are due to the same cause, none, some, or all cases may still fail. which contradicts the specification and is therefore a clear bug in These still failing test cases are again automatically documented by v9.0.0-rc3 of QEMU . A comparison run on an earlier version, v8.0.4, RVVTS and form a new (sub-)test set. The whole process is repeated of QEMU also shows that this is a new bug introduced somewhere until all causes are found. in between v8.0.4 and v9.0.0-rc3 of QEMU . Table 4 presents the result of this process for our current QEMU case study. The left-most column of the table shows the formed 6 CONCLUSIONS instruction classes. For each class the number of corresponding In this paper, we have introduced the modular and open-source isolated failing instructions and the number of minimized test cases RVVTS framework which comes with our novel Single Instruction for RV32 and RV64 is given. The right-most column of the table Isolation technique for positive and negative testing of RVV imple- represents the results of the analysis and contains a list of brief mentations, addressing the challenges posed by the complexity of descriptions of the isolated causes. In order to conclude our case the 600+ highly configuration-dependent RVV instructions. study on QEMU , we now discuss two interesting causes that have The effectiveness of RVVTS was demonstrated in our case studies, been identified as previously undetected bugs in QEMU . where we (i) generated test sets with functional coverage >94% for The first bug is related to the vslide1*.vx class of instruc- positive and negative testing of 32 and 64 bit RVV implementations, tions, vslide1up.vx and vslide1down.vx, which only fail (ii) applied the test set on the RISC-V VP++ and QEMU resulting on RV32. Both instructions slide the elements in a vector in the in minimized test cases and isolated failing instructions using our given direction by one element and insert a new vector element Single Instruction Isolation with Code Minimization technique, and from a given scalar integer register. On the affected RV32, the scalar (iii) traced down the causes of the failed isolated instructions to integer registers are 32 bit wide. All detected failing cases have find the root cause. the following characteristics: (i) vector elements are configured to Overall, we confirmed 3 new bugs in the RISC-V VP++ and 2 64 bit, and (ii) the most significant bit in the 32 bit scalar integer new bugs in QEMU (and 7 more are to be analyzed where we will register is set, which can be interpreted as negative value. The consider the formal RISC-V Sail specification model to finally clarify corresponding results show, that the reference simulator Spike and potential ambiguities in the RVV specification). The generated test QEMU provide the same result on the lower 32 bits of the newly sets and the RVVTS framework are available as open-source on introduced vector element, which also matches the value of the GitHub. Moreover, our findings are reported to the respective open- scalar integer register. However, the higher 32 bit of the value dif- source projects. fer: While these bits are all set (= 1) by the reference simulator, corresponding to a sign extension of the scalar value, they are all ACKNOWLEDGMENTS cleared (= 0) by QEMU . This is definitely a bug in QEMU , as the This work has partially been supported by the LIT Secure and Correct Systems Lab RVV specification version 1.0 clearly states that a sign-extend must funded by the State of Upper Austria.

Single Instruction Isolation for RISC-V Vector Test Failures ICCAD ’24, October 27–31, 2024, New York, NY, USA

REFERENCES Great Lakes Symposium on VLSI. 599–605. [1] 2021. RISC-V Compliance Task Group. https://github.com/riscv/riscv- [34] Manfred Schlägl and Daniel Große. 2024. Bounded Load/Stores in Grammar-based compliance. Code Generation for Testing the RISC-V Vector Extension. In RISC-V Summit [2] 2021. RISC-V Torture Test Generator. https://github.com/ucb-bar/riscv-torture. Europe. [3] 2022. RISC-V V vector extension. https://github.com/riscv/riscv-v-spec. [35] Manfred Schlägl, Christoph Hazott, and Daniel Große. 2024. RISC-V VP++: Next [4] 2023. IEEE Standard for Standard SystemC Language Reference Manual. https: Generation Open-Source Virtual Prototype. In Workshop on Open-Source Design //doi.org/10.1109/IEEESTD.2023.10246125 Automation. [5] 2024. FORCE-RISCV RISC-V Instruction Sequence Generator (ISG). https:// [36] Manfred Schlägl, Moritz Stockinger, and Daniel Große. 2024. A RISC-V “V” github.com/openhwgroup/force-riscv. VP: Unlocking Vector Processing for Evaluation at the System Level. In Design, [6] 2024. QEMU A generic and open source machine emulator and virtualizer. Automation and Test in Europe. 1–6. https://www.qemu.org. [37] Eshan Singh, David Lin, Clark W. Barrett, and Subhasish Mitra. 2018. Logic [7] 2024. RISC-V Architecture Test SIG. https://github.com/riscv-non-isa/riscv-arch- Bug Detection and Localization Using Symbolic Quick Error Detection. IEEE test. Transactions on Computer Aided Design of Circuits and Systems (2018). [8] 2024. RISC-V Formal Verification Framework. https://github.com/YosysHQ/riscv- [38] Eshan Singh, Florian Lonsing, Saranyu Chattopadhyay, Maxwell Strange, Peng formal. Wei, Xiaofan Zhang, Yuan Zhou, Deming Chen, Jason Cong, Priyanka Raina, [9] 2024. RISCV-DV. https://github.com/google/riscv-dv. Zhiru Zhang, Clark W. Barrett, and Subhasish Mitra. 2020. A-QED Verification [10] 2024. RISCV Sail Model. https://github.com/rems-project/sail-riscv. of Hardware Accelerators. In Design Automation Conf. 1–6. [11] 2024. riscvOVPsim Imperas RISC-V Instruction Set Simulator (ISS). https://www. [39] Andrew Waterman and Krste Asanović. 2019. The RISC-V Instruction Set Manual; imperas.com/riscvovpsim-free-imperas-risc-v-instruction-set-simulator. Volume I: Unprivileged ISA. SiFive Inc. and UC Berkeley. [12] 2024. Siemens EDA Questa Formal Verification Apps. https://eda.sw.siemens. [40] Andrew Waterman and Krste Asanović. 2019. The RISC-V Instruction Set Manual; com/en-US/ic/questa/formal-verification. Volume II: Privileged Architecture. SiFive Inc. and UC Berkeley. [13] 2024. Spike RISC-V ISA Simulator. https://github.com/riscv/riscv-isa-sim. [14] Allon Adir, Eli Almog, Laurent Fournier, Eitan Marcus, Michal Rimon, Michael Vinov, and Avi Ziv. 2004. Genesys-Pro: innovations in test program generation for functional processor verification. IEEE Design & Test of Comp. (2004), 84–93. [15] Niklas Bruns, Daniel Große, and Rolf Drechsler. 2020. Early Verification of ISA Extension Specifications Using Deep Reinforcement Learning. In ACM Great Lakes Symposium on VLSI. 297–302. [16] Brian Campbell and Ian Stark. 2014. Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. In Formal Methods for Industrial Critical Systems. 185–199. [17] Mikhail Chupilko, Alexander Kamkin, Artem Kotsynyak, and Andrei Tatarnikov. 2017. MicroTESK: Specification-Based Tool for Constructing Test Program Gen- erators. In Haifa Verification Conference. 217–220. [18] Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, and Wolf- gang Kunz. 2020. Gap-free Processor Verification by S2QED and Property Gener- ation. In Design, Automation and Test in Europe. 526–531. [19] Roger Espasa, Mateo Valero, and James E. Smith. 1998. Vector Architectures: Past, Present and Future. In International Conference on Supercomputing. 425–432. [20] Shai Fine and Avi Ziv. 2003. Coverage directed test generation for functional verification using Bayesian networks. In Design Automation Conf. 286–291. [21] M.J. Flynn. 1966. Very high-speed computing systems. IEEE 54, 12 (1966), 1901– 1909. [22] Vladimir Herdt, Daniel Große, and Rolf Drechsler. 2020. Closing the RISC-V Compliance Gap: Looking from the Negative Testing Side. In Design Automation Conf. 1–6. [23] Vladimir Herdt, Daniel Große, and Rolf Drechsler. 2020. Enhanced Virtual Proto- typing: Featuring RISC-V Case Studies. Springer. [24] Vladimir Herdt, Daniel Große, and Rolf Drechsler. 2020. Towards Specification and Testing of RISC-V ISA Compliance. In Design, Automation and Test in Europe. 995–998. [25] Vladimir Herdt, Daniel Große, Eyck Jentzsch, and Rolf Drechsler. 2020. Efficient Cross-Level Testing for Processor Verification: A RISC-V Case-Study. In Forum on Specification and Design Languages. 1–7. [26] Vladimir Herdt, Daniel Große, Hoang M. Le, and Rolf Drechsler. 2019. Verifying Instruction Set Simulators using Coverage-guided Fuzzing. In Design, Automation and Test in Europe. 360–365. [27] Jaewon Hur, Suhwan Song, Dongup Kwon, Eunjin Baek, Jangwoo Kim, and Byoungyoung Lee. 2021. DifuzzRTL: Differential Fuzz Testing to Find CPU Bugs. In Symposium on Security and Privacy. 1286–1303. [28] Charalambos Ioannides, Geoff Barrett, and Kerstin Eder. 2011. Feedback-Based Coverage Directed Test Generation: An Industrial Evaluation. In Haifa Verification Conference. 112–128. [29] Victor Jimenez, Mario Rodriguez, Marc Dominguez, Josep Sans, Ivan Diaz, Luca Valente, Vito Luca Guglielmi, Josue V. Quiroga, R. Ignacio Genovese, Nehir Sonmez, Oscar Palomar, and Miquel Moreto. 2023. Functional Verification of a RISC-V Vector Accelerator. IEEE Design & Test of Comp. 40, 3 (2023), 36–44. [30] Yoav Katz, Michal Rimon, and Avi Ziv. 2012. Generating instruction streams using abstract CSP. In Design, Automation and Test in Europe. 15–20. [31] Lucas Klemmer and Daniel Große. 2021. EPEX: Processor Verification by Equiva- lent Program Execution. In ACM Great Lakes Symposium on VLSI. 33–38. [32] Lorenzo Martignoni, Roberto Paleari, Giampaolo Fresi Roglia, and Danilo Bruschi. 2009. Testing CPU Emulators. In International Symposium on Software Testing and Analysis. 261–272. [33] Manfred Schlägl and Daniel Große. 2023. GUI-VP Kit: A RISC-V VP Meets Linux Graphics - Enabling Interactive Graphical Application Development. In ACM