SOURCE ARCHIVE
EXTRACTED CONTENT
55,273 chars Exploring the Parameter Space for Constrained
Random Verification of RISC-V CPUs
Sallar Ahmadi-Pour1, Luca M¨uller2, Rolf Drechsler1,2
1Institute of Computer Science, University of Bremen, Bremen, Germany
2Cyber-Physical Systems, DFKI GmbH, Bremen, Germany
{sallar, lucam, drechsler}@uni-bremen.de
Abstract—With the growing complexity of modern Integrated For VP-RTL cross-level verification, this spans a space for Circuits (ICs), cross-level verification increasingly relies on mul- verification parameters (e.g., number of generated inputs for tiple coverage metrics to assess verification progress and quality. tests, or mutation location), where understanding the impact While Virtual Prototypes (VPs) enable efficient verification across abstraction layers, the impact of verification parameters on of such parameters is crucial for the quality of verification bug-finding effectiveness remains poorly understood. This work results. With verification across abstraction layers using VPs presents an exploratory analysis of verification parameters in a and coverage-driven, parameterized tests, it is essential to Constrained Random Verification (CRV)-based cross-level setup. understand how verification parameters affect bug-finding ef- Using a RISC-V Register-Transfer Level (RTL) implementation fectiveness and coverage metrics. and a binary-compatible VP, we systematically explore a parame- terized CRV-based verification flow, varying instruction sequence To tackle this, we examine how verification parameters length, mutation location, and mutation count, and assess their affect bug-finding effectiveness and coverage behavior in a impact using mutation, functional, and code coverage metrics. cross-level CRV setup. Rather than pursuing coverage closure Our results show that different coverage metrics exhibit distinct saturation behaviors as verification parameters are varied. In or parameter optimization, we aim to systematically charac- particular, mutation coverage continues to reveal bug-finding terize how parameters such as instruction sequence length, effectiveness in scenarios where functional and code coverage and mutation location affect different coverage metrics. In stabilize, highlighting the importance of cross-checking trends this context, mutation testing is used as a practical proxy across multiple metrics rather than maximizing individual cov- for bug-finding effectiveness, capturing a broad range of fault erage values in isolation. Index Terms—Verification, Constrained Random Verification, types, including small design errors that may arise from Cross-Level, Virtual Prototype, Register-transfer Level specification misunderstandings or mistakes, while comple- mentary coverage metrics provide additional perspectives on I. INTRODUCTION verification progress. While the presented results are obtained Increasing IC complexity makes verification across abstrac- from a RISC-V processor case study, the design combines tion levels increasingly important [1]–[3]. VPs provide fast, control-intensive and datapath-intensive components, making binary-compatible executable models that can serve as early the derived insights applicable to a wider class of processor- system-level references for RTL verification [4], [5]. At the like architectures. system-level, VPs have shown immense capabilities, including 1) Propose a parameter-centric framework for evaluating the but not limited to testing and verification of Software (SW) [6], impact of verification parameters with coverage-based and [7], functional verification [8], [9], or evaluation of platform mutation-based assessment in CRV-based cross-level ver- and environment interaction [10]. In VP-RTL cross-level ver- ification using mutation, functional, and code coverage ification, the same SW binary runs on both models, and their metrics. traces are compared to spot behavioral mismatches. While 2) Systematically explore how the verification parameter promising, these flows’ effectiveness depends on verification space, such as instruction sequence length, mutation count, parameters such as program length and mutation location. and mutation location influence bug-finding effectiveness Recent works often utilize established methods from the and coverage behavior in a RISC-V VP-RTL cross-level domain of SW verification or leverage machine learning setup, and derive insights on saturation and sensitivity of techniques to address scalability or coverage closure but ignore commonly utilized coverage metrics. the various parameters available in the verification setup [11]– 3) As part of the framework, we open-source the utilized [13]. Moreover, a popular technique to quantify the bug- scripts to automatically generate and inject bugs into RTL finding capabilities is to introduce artificial bugs through designs and their submodules, allowing fine-grained control mutation of the original Device under Verification (DUV). over the location of injected mutations.1 This research has been supported by the German Ministry for Re- search, Technology and Space (BMFTR) with projects Scale4Edge (grant no. 16ME0127), ECXLplus (grant no. 01IW24001), and ExaVerse (grant no. 16IW25003). 1 https://github.com/agra-uni-bremen/fdl-2026-mutationGeneration
II. BACKGROUND AND RELATED WORK and Central Processing Unit (CPU) designs offers additional
A. Constrained Random Verification constraints applicable to families of processors to improve the
The goal of Hardware (HW) verification, to ensure correct- quality of results [11], [12], [22]. While fast, fuzzers require a
ness of a DUV and covering as many behavioral aspects as lot of guidance and additional feedback (e.g., coverage-guided
possible, comes with various challenges. Different circuits can fuzzing), and when proposed as a general framework, require a
focus mostly on data flow or control flow, respectively, while lot of tailoring. Symbolic execution formally identifies inputs
other circuits might describe programmable and modular ar- with symbolic variables that represent value sets, narrowing
chitectures with various interconnection schemes. Hence, chal- them as the behavioral description is explored. However, the
lenges, such as state space explosion [14] or the programmable thorough exploration of the input space is subject to state-
nature of a DUV, can lead to a differing effectiveness of space explosion, hence having possibly huge run times.
existing and emerging methodologies for verification. Com- CRV provides a balanced input generation approach with
monly, formal verification, such as model checking [15], [16], constraints defining legal and illegal patterns and enables
achieves full coverage of behavioral aspects and can ensure sequencing for complex circuits that would otherwise need
correctness for a DUV, but possibly suffers issues regarding extra guidance [23]. Various techniques explore extensions
scalability. In contrast, simulation-based methods involve more around CRV for modeling languages like SystemC [24], to
controllable run times, while input stimuli generation and improve the simulation run times [28], and to improve the
concluding correctness depend on expert knowledge. quality of results [29]. The introduction of HW models at
To deal with the challenges of the latter, various simulation- different levels of abstraction also proposed the need for meth- based methods have emerged with different advantages and ods covering across such levels of abstraction (e.g., system- disadvantages. Methods from the domain of SW, such as level and RTL) [30], [31]. When utilizing VPs, analyzing Fuzzing [17]–[20]; and Symbolic Execution [21], [22]; have and merging different models in Transaction Level Modeling shown to be feasible for the generation of input stimuli (TLM) inside VPs and the RTL [13] or unifying coverage for DUVs. Such methods rely on guided input generation between SW and HW of the system [32] are particularly recent through assumptions and coverage-guided feedback informa- challenges [31]. Techniques to improve CRV, particularly tion to handle larger input and state spaces. The technique of relying on machine learning, such as Bayesian networks and Constrained Random Verification (CRV) [23] enables a more Bayesian estimation [33]–[35], require knowledge about the effective constraining while being compatible with functional parameters of the verification process. Although many works and code coverage aspects of the DUV. By internally utilizing show the exploration through machine learning techniques, the SMT solvers, the constraints are turned into input stimuli effect of various parameters is often assumed or unknown, systematically and automatically. As CRV for HW verification and a systematic exploration of verification parameters is is well-established, tracking coverage metrics (functional and neglected, although realistic [31]. As a result, understanding code) through commercial RTL simulators alongside the CRV the role of verification parameters remains an open challenge methodology is possible. Various tailored variants have been in cross-level CRV-based verification. proposed for verification beyond RTL, like CRAVE [24] for In contrast to works that propose novel verification ap- the SystemC modeling language, and for specific use-cases, proaches or focus on the optimization for coverage closure, tools such as riscv-dv [25] are suitable to explore CRV for the this work takes a complementary position by systematically generation of RISC-V instructions. characterizing the impact of verification parameters within an existing CRV-based cross-level verification approach. While B. Related Work other recent approaches leverage machine learning or coverage guidance to improve verification efficiency, they typically Since verification is essential yet time-consuming in chip assume verification parameters to be fixed or implicitly tuned. development, hardware verification has accumulated extensive Our work instead focuses on understanding how parameters research on methodologies, techniques, and metrics to gauge such as instruction sequence length, mutation location, and its completeness. In this scope, HW verification is commonly mutation count influence the bug-finding effectiveness and the split into formal verification methods [15], [26], aiming for behavior of different coverage metrics. thorough proofs of HW properties, and simulation-based meth- ods [23], utilizing golden reference models and assertions III. CROSS-LEVEL VERIFICATION WITH CRV to check for behavioral correctness. Within simulation-based The framework presented in this work performs verification methods, techniques like fuzzing, symbolic execution, ma- for a given cross-level setup with CRV. It is utilized to explore chine learning techniques, and CRV are among the widely the verification parameter space, spanned through different adopted methods. Particularly, the authors of [17], [18], [20] configurations of the length of input stimuli, the amount of all describe recent state-of-the-art fuzzing-based techniques, mutations injected into the DUV, as well as the location of utilizing fuzzers from the SW domain to generate input these mutations. stimuli. Other works, such as [13], [27], explore the veri- Figure 1 shows an overview of the proposed approach, with fication of peripherals through symbolic generation of input numbered steps guiding the flow. At 1 , the figure shows the stimuli. Applying fuzzing or symbolic execution to processor explored verification parameter space: the length of instruction
Verification Cross-Level Insight
Parameter Space List of CRV Setup Analysis
1 identify & configure Strategies 2 VP 9 assess
Constraint-
Instr. Seq. based 4 (Golden Reference Trace Match
Lengths Generator generate Reference) 8 compare ==
Mutation Platform- RISC-V 6 7 Mutated DUV Trace Mismatch
Count dependent Executable simulate collect
Macros
Mutation instruct 3RTL Mutation inject 5 μRV32 RTL Functional Code Verification
Location Engine (mutated Mutation Completeness
DUVs) Coverage Measurement
Figure 1: Overview of the proposed CRV-based Cross-Level Framework for Verification Parameter Space Exploration.
sequences, the number of mutations, and the location of tion coverage, RISC-V related functional coverage, and code mutations that are injected into the DUV. These parameters coverage for RTL and VP are collected. Beyond traditional are used to configure and instruct the CRV tool ( 2 ), together RTL-centric metrics, the VP enables enhancement and cus- with the different CRV strategies, and the RTL mutation engine tomization of the coverage measurement process. This gathers ( 3 ). In particular, for this work, we explore the verification execution metrics such as value coverage and the unique parameter spaces within the riscv-dv [25] framework together sets of register and immediate values. The mutation coverage with a commercial RTL simulator. It should be noted that represents the amount of mutations killed (i.e., the framework other tools and techniques to generate RISC-V instructions, detects a mismatch), the functional coverage represents the such as Scala-based RISC-V Torture Test [36] or FORCE- different functional aspects given in the RISC-V Instruction RISCV [37], can be used instead of riscv-dv. A requirement Set Architecture (ISA), and the RTL code coverage represent for other tools is the availability of parameters (e.g., instruction metrics like statement coverage, mux and toggle coverage, sequence length) and a mechanism to execute instructions branch coverage and more. The last step ( 9 ) assesses the in the cross-level setup. The introduction of mutations is outcome of the cross-level verification (i.e., which bugs led to performed seperately from the instruction generation ( 3 ). The faulty behavior) as well as the completeness of the verification. CRV tool generates instruction sequences that are compiled to By integrating RTL-based and VP-based coverage metrics in platform specific executables ( 4 ) for the cross-level setup. In a cross-level setup, the framework offers a holistic view of this setup, we utilize a RISC-V based System-on-Chip (SoC) how verification parameters affect both coverage behavior and for the RTL, namely MicroRV32 [38], with its corresponding bug-finding effectiveness. Except for the final analysis, the RISC-V VP [39] platform. As the two platforms are binary parameter space exploration runs fully automated. compatible, the exact same executable is run on both models. IV. E Next, the RTL mutation engine injects one of the given VALUATION mutations into one of the submodules of the DUV ( 5 ). The A. Experimental Setup mutated RTL represents a DUV with a bug, hence varying For the evaluation, we explore the verification parameter the type and location of the mutation emulates a different space of our CRV-based cross-level verification with the fault. As part of this work, we provide the scripts to mutate following verification parameters: any RTL design as open source to stimulate further research. PV er1: The length of instruction sequences is varied in the The scripts utilize part of the capabilities to mutate modules provided by Yosys [40], with additional processing stages range 100, 1000 and 10 000. Resulting in three differ- added, enabling a granular choice of submodules for the P ent executable lengths. injection of mutations. The mutations flip bits, replace them V er2: To evaluate a reasonable number of faults, the number with constants, or alter logic operations in expressions. We of mutations for each mutation target is fixed at 500, then filter out ineffective mutations or those whose effects are with an exception for the Fetch Unit due to its small not observable at the outputs. Through the simulation ( 6 ) the size, where we inject 249 mutations. Resulting in 2749 VP and the DUV create execution traces, which are collected P (5 × 500 + 1 × 249) distinctly mutated DUVs. ( 7 ) for comparison ( 8 ). In this work, we utilize the pre- V er3: Mutations are targeted to the full CPU as well as defined trace format from riscv-dv, consisting of the program submodules ALU, Control Unit, Fetch Unit, Instruc- counter, the instruction, the registers used and updated by the tion Decoder and Multiply-Divide Unit, respectively. instruction, updated privileged registers by the instruction, the Resulting in six different mutation locations. instruction binary, and the immediate operands. This cross- We apply the CRV strategies Full Random, Arithmetic, level execution avoids costly RTL-RTL co-simulation and Load-Store, Jump-Branch and Loop, resulting in five different allows longer instruction sequences to be executed efficiently, types of executables with different instruction corpora per CRV while mismatches between VP and RTL directly indicate generation. Following the verification parameters above, we faulty behavior. Additionally, coverage metrics, such as muta- generate instruction sequences with each strategy, for each sequence length (PV er1) and apply them to each distinct DUV
Table I: Effect of generated instruction sequence length (PV er1) on mutation-based, functional and code coverage.
Instr. [#] Killed [#]Mutation Coverage Func. Cov. [%] RTL Code Coverage
Total [#] Killed [%] Branch Cov. [%] Statement Cov. [%] Toggle Cov. [%]
100 9663 13745 70.30 56.11 78.97 85.71 70.41
1000 9903 13745 72.05 57.61 78.84 85.53 70.64
10000 11254 13745 81.88 57.70 78.97 85.71 70.87
Table II: Breakdown of module-based mutations (PV er3) and the effect of number of generated instructions (PV er1) on mutation
coverage, functional coverage and RTL code coverage.
Module Instr. [#] Killed [#]Mutation Coverage Func. Cov. [%] RTL Code Coverage
Total [#] Killed [%] Branch Cov. [%] Statement Cov. [%] Toggle Cov. [%]
100 1963 2500 78.5 42.9 78.97 85.71 70.18
ALU 1000 2086 2500 83.4 46.4 78.58 85.36 70.60
10000 2217 2500 88.7 47.8 78.71 85.62 70.83
100 1120 2500 44.8 39.9 78.20 85.18 70.07
Control 1000 1464 2500 58.6 44.7 78.71 85.45 70.45
10000 2148 2500 85.9 44.5 78.97 85.71 70.77
100 1918 2500 76.7 42.0 78.46 85.27 70.14
Decode 1000 1578 2500 63.1 47.1 78.58 85.36 70.51
10000 1570 2500 62.8 47.3 78.20 85.18 70.16
100 1188 1245 95.4 47.0 78.20 85.18 70.06
Fetch 1000 1190 1245 95.6 49.0 78.46 85.36 70.35
10000 1206 1245 96.9 47.8 78.97 85.71 70.78
100 2116 2500 84.6 36.6 78.20 85.18 70.25
MulDiv 1000 2226 2500 89.0 44.6 78.84 85.53 70.38
10000 2378 2500 95.1 43.9 78.97 85.71 70.83
100 1358 2500 54.3 43.6 78.20 85.18 70.17
Core 1000 1359 2500 54.4 46.1 78.58 85.36 70.47
10000 1735 2500 69.4 47.3 78.97 85.71 70.85
(PV er2 and PV er3). Therefore, DUVs with 500 mutations have of detected mutations in the second column, and the relative 2500 (5 · 500) runs per instruction sequence length and 249 amount in the fourth column, the functional coverage given by mutations result in 1245 (5·249) runs per instruction sequence riscv-dv in the fifth column, and the code coverage obtained length, respectively. Summing up each of these runs per from the RTL simulation in the sixth to eighth columns. For instruction sequence length results in 13 745 runs (5 · 2500 + code coverage, branch, statement, and toggle coverage are 1 · 1245). In total, we performed 41 235 (3 · 13745) different displayed as representatives, as they feature the largest number cross-level verification runs, each resulting in coverage and of bins for the RTL core (over 1000 bins compared to 161 bins mismatch measurements. The experiments were performed on or less for the other code coverage metrics), providing more a Intel(R) Xeon(R) Gold 6240 CPU with 36 cores @ 2.6 GHz information on different parts of the RTL code. with 376 GB memory running Ubuntu 22.04. Each run took Increasing the instruction count per verification run leads to around ten seconds of walltime on our setup. Simulations were more mutations being detected through DUV-VP mismatches. performed through riscv-dv and a commercially available RTL Even for only 100 generated instructions, already over 70 % of simulation tool, while the accompanying SoC in RTL and the the 13 745 injected mutations are killed by CRV. This number corresponding VP are available as open-source. is increased to almost 82 % for 10 000 instructions. Functional B. Evaluation Results coverage ranges from 56.11 % to 57.70 %, showing only For the total 41 235 performed runs, we first break down marginal increase with increasing instruction sequence length. the effectiveness and coverage metrics of the full design, in Generally, code coverage values are much higher than func- relation to PV er1. This allows us to observe this parameter tional coverage, but once again behave very similarly between in more isolation, when applied to the full CPU. After that, the number of instructions. Values range from 70.41 % for we illustrate the results of injecting the respective number toggle coverage of 100 instructions to 85.71 % for statement of mutations (parameter PV er2) into each module separately, coverage of 10 000 instructions. Note that longer instruction as described through the parameter PV er3. To assess result sequences are not generated on the corpus of shorter sequences quality, we examine immediate value coverage in the instruc- but generated anew, hence explaining the slight drop in branch tion stream and analyze register file accesses, reporting total and statement coverage between 100 and 1000 instructions. accesses and unique values per register. Despite this fact, the results provide an indication on the effect Table I provides an overview of detected mutations (i.e., of PV er1 due to the high number of 13 745 runs per instruction mutation coverage), functional coverage and selected code length. coverage metrics (branch, statement, and toggle coverage) Table II breaks down the information summarized in Table I in relation to the verification parameter PV er1. The table is for each module (i.e., unfolding verification parameters PV er1 split into four parts: the leftmost column shows the parameter and PV er3 in one table). The table is split into five parts: length of instruction for the CRV generation, second to fourth the leftmost column shows each module from verification columns show the mutation coverage with the absolute number parameter PV er3 and the number of mutations applied to
14% 100 instructions 12% 1,000 instructions 10% 10,000 instructions 8% 6% 4% 2% 0% x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 (a) Relative number of register accesses (%) 100 instructions 10% 1,000 instructions 10,000 instructions 8%
6%
4%
2%
0% x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 (b) Relative number of unique values per register (%) Figure 2: Relative amount of generated instructions versus number of register accesses and unique values per register.
it. The second column follows with the instruction sequence Table III: Number of immediate values and unique immediate length that was used for each module, while the third to fifth values for different instruction types and fields for each columns show the mutation coverage, the sixth column shows instruction sequence length (PV er1). the functional coverage given by riscv-dv and the seventh to Imm. Type (Bits) Instr. [#] Total Values [#] Unique Values [#] Value Coverage [%] ninth columns show the RTL code coverage obtained for the Shamt (5) 100 1399 32 100% particular module. A change in coverage behavior is noted for 1000 9680 32 100% 10000 36774 32 100% different mutation locations, with a notable difference (34.1 100 4853 1117 27.27% I-Imm (12) 1000 41242 2250 54.93% percentage points), for example, between the Decode unit 10000 118662 4060 99.12% 100 4221 268 6.54% (62.8 %) and the Fetch unit (96.9 %) for an instruction se- S-Imm (12) 1000 14087 976 23.83% quence length of 10 000. Across different instruction sequence 10000 32966 3303 80.64% 100 743 63 1.54% lengths, the effects stay mostly consistent with the behavior B-Imm (13) 1000 4862 131 3.20% 10000 16667 180 4.39% observed previously in Table I, with the exception of the J-Imm (20) 100 2143 96 0.01% 1000 3698 102 0.01% Decode unit. Changes in functional coverage generally show a 10000 16088 93 0.01% slight increase with an increasing instruction sequence length, 100 3324 443 0.04% U-Imm (20) 1000 8687 543 0.05% where the starkest difference is observed for the MulDiv 10000 23139 988 0.09% unit, with 36.6 % for 100 instructions and 43.9 % for 10 000 instructions. Regarding code coverage, values behave very the I-Imm field becomes covered almost completely (99.12 %) similar across verification parameters PV er1 and PV er3. when generating 10 000 instructions, while other fields show lower values. The S-Imm field is covered to around 81 % after Table III shows the number of total immediate values and 10 000 instructions, with the remaining fields (B-Imm, J-Imm unique immediate values for the six different types of immedi- and U-Imm) staying below 5 %. The remaining fields (B-Imm, ate fields found in RISC-V instructions. The leftmost column J-Imm, U-Imm) show only a slight rise with more instructions, shows the immediate field together with its number of bits in underscoring the exponential growth of state space for each parentheses (e.g., I-Imm being the 12 bit immediate for the I- added immediate bit. The I-Imm and S-Imm fields on the type instructions), the second column breaks down the values other hand exhibit a much larger increase depending on for the different instruction sequence lengths (PV er1), the third instruction sequence length, starting from 27.27 % and 6.54 % column shows the total number of immediates of that type respectively for 100 instructions. present, while the fourth and fifth columns present the absolute Figure 2 shows two plots illustrating the different register and relative number of uniquely generated immediate values. file accesses (Figure 2a) and unique values (Figure 2b) handled The Shamt field (for shift amounts) is covered completely, and per register respectively. Both plots map relative register ac-
cesses and unique values for each instruction sequence length. for 10 000 instructions, but register distribution for generated
Note that, as x0 is a special purpose register with the constant instructions may not be as randomized.
zero value, it will always only hold one unique value. For As for PV er2, we can observe the difference between the
100 instructions, the highest percentage of register accesses Fetch unit with 249 mutations and remaining modules with for x0 is around 14 %, and for 10 000 instructions, this 500 mutations in Table II. Here, fewer mutations raise muta- number decreases to 10 %, showing lower extremes for longer tion coverage but barely affect functional or code coverage. instruction sequences (in this regard, also notice register x30). Finally, looking at PV er3, Table II shows that the location For 1000 instructions, x2 and x0 manifest as outliers, with of mutation injection can make a significant difference regard- both being responsible for around 8 % of register accesses. As ing mutation coverage. While this effect is slightly reduced for unique values, the opposite effect can be observed. Here, between instruction sequence lengths (e.g., 50.6 percentage the highest relative number for 100 instructions is around 6 % points between Control unit and Fetch unit for 100 instructions of unique values for register x1, while for 1000 instructions, and 34.1 percentage points between Decode Unit and Fetch roughly 7 % of unique values are stored in register x2 and for unit for 10 000 instructions), a divergence can still be observed. 10 000 instructions, 11 % of unique values are stored in x1. Regarding mutations injected at arbitrary locations (row Core in Table II), these are generally harder to catch, due to the in- C. Discussion of Exploration Results creased spread of mutations. The Fetch unit shows the highest Below we discuss our exploration results and the impact mutation coverage at all sequence lengths, likely because it of the three verification parameters. We examine only relative is less complex than other modules. However, these findings differences across parameters and not the coverage closure do not translate to functional or code coverage. While for to gain insight, rather than to optimize them. Also note that, the former, there are at least some minor differences between while the numbers presented are specific to our CRV setup, we mutation locations (around 10 percentage points), for the latter, expect that the use of other tools that can be plugged into our differences between modules are marginal, indicating that framework, as mentioned above, would reveal similar trends. these coverage values converge in a similar fashion. First, we consider PV er1 across all evaluations. Intuitively, In summary, our systematic exploration provides the follow- the largest effect may be expected from this parameter, as ing insights on the effect of different verification parameters it increases the chance of constrained random instruction on verification quality:• generation to hit certain coverage targets. Looking at Table I, Increased instruction count achieves higher mutation cover- increasing the number of instructions does indeed increase • age and cover a higher range of immediate values. mutation coverage, but the effect is limited, only furthering Higher instruction count does not imply more functional or coverage closure by 39 %, despite a 100 times increase in • code coverage. instruction sequence length. For functional and code coverage, The use of functional and code coverage to gauge verifi- this effect is decreased even further. However, our functional cation quality needs further investigation, considering the coverage measure contains very detailed targets (e.g., bit-wise • limited correlation with mutation coverage in our evaluation. opposite values for logical operations), as well as coverage of Mutations targeted at specific locations of a design may be Control and Status Registers (CSRs), which are not covered by • killed with higher precision than random mutation locations. the employed CRV strategies. Hence, a direct rise in this metric This divergence between locations may be a useful indicator is not guaranteed. Mutation coverage illustrates this, as it exists of which parts of the design might require further attention between RTL code coverage (offering limited interpretabil- beyond CRV during the verification process. ity) and behavior-tracking functional coverage. Regarding the V. C coverage of immediate values shown in Table III, increasing ONCLUSION instruction sequence length has a much larger effect, where In this work, we proposed a combined approach to explore almost complete coverage closure can be achieved for the I- three verification parameters for CRV in a cross-level setup be- Imm value by increasing from 100 to 10 000 instructions. A tween RTL HW and system-level VPs. Through the systematic similar effect can be observed for the S-Imm value. For the exploration of these three verification parameters, the vary- much larger coverage spaces of J-Imm and U-Imm values, ing effect of these parameters on different coverage metrics the increased coverage does not show directly, which may be has been demonstrated. Particularly, for mutation coverage, attributed to the large coverage space and the much reduced functional coverage and RTL code coverage, dependencies on number of instructions using these immediate encodings. the generated instruction sequence length and the location The generated instruction sequences use registers fairly uni- of the injected mutation were shown. By making the tool formly regarding access frequency and unique values. While for injecting the mutations with module granularity into the for the number of register accesses, less outliers occur in the designs available as open source, we aim to stimulate further relative distribution for 10 000 instructions, the distribution of research. To boost CRV-based techniques further, in the future, unique values does not seem to be more evenly distributed for we plan to explore feedback-based methods to adapt CRV increased instruction sequence lengths. A possible explanation strategies, and parameters to guide input generation towards for this might be the fact that more unique values are generated undetected mutations/bugs.
REFERENCES [25] CHIPS Alliance, “RISCV-DV.” [Online]. Available: https://github.com/
chipsalliance/riscv-dv
[1] L.-T. Wang, Y.-W. Chang, and K.-T. T. Cheng, Electronic design [26] T. Kropf, Introduction to formal hardware verification. Springer Science automation: synthesis, verification, and test. Morgan Kaufmann, 2009. & Business Media, 2013. [2] J. L. Hennessy and D. A. Patterson, “A new golden age for computer [27] P. Pieper, V. Herdt, D. Große et al., “Verifying systemc tlm peripherals architecture,” Communications of the ACM, vol. 62, no. 2, pp. 48–60, using modern c++ symbolic execution tools,” in Proceedings of the 59th 2019. ACM/IEEE Design Automation Conference, 2022, pp. 1177–1182. [3] A. Gerstlauer, C. Haubelt, A. D. Pimentel et al., “Electronic system- [28] S. M. Ambalakkat and E. G. Nelson, “Simulation runtime optimization level synthesis methodologies,” IEEE Transactions on Computer-Aided of constrained random verification using machine learning algorithms,” Design of Integrated Circuits and Systems, vol. 28, no. 10, pp. 1517– in Design and Verification Conf.(DVCON), 2019. 1530, 2009. [29] A. Nazi, Q. Huang, H. Shojaei et al., “Adaptive test generation for fast [4] B. Bailey, F. Balarin, and M. McNamara, Tlm-driven design and functional coverage closure,” DVCON USA, 2022. verification methodology. Cadence Design Systems, 2010. [30] S. Vinco, N. Bombieri, D. J. Pagliari et al., “A cross-level verification [5] “Ieee standard for standard systemc® language reference manual - methodology for digital ips augmented with embedded timing moni- corrigendum 1,” IEEE Std 1666-2023/Cor 1-2025 (Corrigendum to IEEE tors,” ACM Transactions on Design Automation of Electronic Systems Std 1666-2023), pp. 1–22, 2025. (TODAES), vol. 24, no. 3, pp. 1–23, 2019. [6] C. Hazott, F. St¨ogm¨uller, and D. Große, “Using virtual prototypes and [31] A. Mahmoudi, A. Neˇskovi´c, C. Thermann et al., “A systematic mapping metamorphic testing to verify the hardware/software-stack of embedded study on systemc/tlm modeling capabilities in new research domains,” graphics libraries,” Integration, vol. 101, p. 102320, 2025. ACM Transactions on Design Automation of Electronic Systems. [7] S. Tempel, V. Herdt, and R. Drechsler, “Symex-vp: an open source [32] C. Hazott and D. Große, “Relation coverage: A new paradigm for virtual prototype for os-agnostic concolic testing of iot firmware,” hardware/software testing,” in 2024 IEEE European Test Symposium Journal of Systems Architecture, vol. 126, p. 102456, 2022. (ETS). IEEE, 2024, pp. 1–4. [8] B. Lin and F. Xie, “A systematic investigation of state-of-the-art systemc [33] S. Fine and A. Ziv, “Coverage directed test generation for functional verification,” Journal of Circuits, Systems and Computers, vol. 29, verification using bayesian networks,” in Proceedings of the 40th annual no. 15, p. 2030013, 2020. Design Automation Conference, 2003, pp. 286–291. [9] J.-H. Oetjens, N. Bannow, M. Becker et al., “Safety evaluation of [34] Q. Huang, H. Shojaei, F. Zyda et al., “Test parameter tuning with automotive electronics using virtual prototypes: State of the art and re- blackbox optimization: A simple yet effective way to improve coverage,” search challenges,” in Proceedings of the 51st annual design automation in Proceedings of the design and verification conference and exhibition conference, 2014, pp. 1–6. [35] US (DVCon), 2022. [10] P. Pieper, V. Herdt, and R. Drechsler, “Advanced environment modeling B. Kumar, G. Parthasarathy, S. Nanda et al., “Optimizing con- and interaction in an open source risc-v virtual prototype,” in Proceed- strained random verification with ml and bayesian estimation,” in 2023 ings of the Great Lakes Symposium on VLSI 2022, 2022, pp. 193–197. ACM/IEEE 5th Workshop on Machine Learning for CAD (MLCAD). [11] N. Kabylkas, T. Thorn, S. Srinath et al., “Effective processor verification [36] IEEE, 2023, pp. 1–6. with logic fuzzer enhanced co-simulation,” in MICRO-54: 54th Annual Y. Lee and H. Cook, “RISC-V Torture Test.” [Online]. Available: IEEE/ACM International Symposium on Microarchitecture, 2021, pp. [37] https://github.com/ucb-bar/riscv-torture 667–678. OpenHW Group, “FORCE-RISCV.” [Online]. Available: https://github. [12] N. Bruns, V. Herdt, D. Große et al., “Efficient cross-level processor [38] com/openhwgroup/force-riscv verification using coverage-guided fuzzing,” in Proceedings of the Great S. Ahmadi-Pour, V. Herdt, and R. Drechsler, “The microrv32 framework: Lakes Symposium on VLSI 2022, 2022, pp. 97–103. An accessible and configurable open source risc-v cross-level platform [13] K. A. Rudkowski, S. Ahmadi-Pour, and R. Drechsler, “Crossym: Cross- for education and research,” Journal of Systems Architecture, vol. 133, level verification of systemc peripherals using symbolic execution,” in [39] p. 102757, 2022. 2025 IEEE 28th International Symposium on Design and Diagnostics of V. Herdt, D. Große, P. Pieper et al., “Risc-v based virtual prototype: An Electronic Circuits and Systems (DDECS). IEEE, 2025, pp. 153–156. extensible and configurable platform for the system-level,” Journal of [14] R. Pel´anek, “Fighting state space explosion: Review and evaluation,” [40] Systems Architecture, vol. 109, p. 101756, 2020. in International Workshop on Formal Methods for Industrial Critical D. Shah, E. Hung, C. Wolf et al., “Yosys+ nextpnr: an open source Systems. Springer, 2008, pp. 37–52. framework from verilog to bitstream for commercial fpgas,” in 2019 [15] E. M. Clarke, O. Grumberg, and D. A. Peled, “Model checking the mit IEEE 27th Annual International Symposium on Field-Programmable press,” Cambridge, Massachusetts, London, UK, vol. 988, 1999. Custom Computing Machines (FCCM). IEEE, 2019, pp. 1–4. [16] R. Drechsler, Advanced formal verification. Springer, 2004. [17] T. Trippel, K. G. Shin, A. Chernyakhovsky et al., “Fuzzing hardware like software,” in 31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 3237–3254. [18] K. Laeufer, J. Koenig, D. Kim et al., “Rfuzz: Coverage-directed fuzz testing of rtl on fpgas,” in 2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, 2018, pp. 1–8. [19] Y. Cheng, H. Zou, J. He et al., “Mmfuzz: Towards enhancing rtl fuzz testing using metric feedbacks based on markov chain,” in 2023 IEEE 32nd Asian Test Symposium (ATS). IEEE, 2023, pp. 1–6. [20] J. Hur, S. Song, D. Kwon et al., “Difuzzrtl: Differential fuzz testing to find cpu bugs,” in 2021 IEEE Symposium on Security and Privacy (SP). IEEE, 2021, pp. 1286–1303. [21] K. Ryan and C. Sturton, “Sylvia: Countering the path explosion problem in the symbolic execution of hardware designs,” in 2023 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2023, pp. 110–121. [22] N. Bruns, V. Herdt, and R. Drechsler, “Processor verification using symbolic execution: A risc-v case-study,” in 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 2023, pp. 1–6. [23] A. B. Mehta, “Asic/soc functional design verification,” A Comprehensive Guide To Technologies and Methodologies, 2018. [24] F. Haedicke, H. M. Le, D. Große et al., “Crave: An advanced constrained random verification environment for systemc,” in 2012 International Symposium on System on Chip (SoC). IEEE, 2012, pp. 1–7.