SOURCE ARCHIVE
EXTRACTED CONTENT
133,752 charsJournal of Electronic Testing (2025) 41:111–138
https://doi.org/10.1007/s10836-025-06169-3
RESEARCH
Survey of Verification of RISC‑V Processors
Chloe Tain1 · Savita Patil1 · Hussain Al‑Asaad1
Received: 19 August 2024 / Accepted: 8 April 2025 / Published online: 24 May 2025 © The Author(s) 2025
Abstract This paper is a survey of the various verification methods available for RISC based processors. The RISC-V processors are open standard that can have user-based extensions. This makes their verification complex and prone to errors. There is ongo- ing research in this area. This paper illustrates the criteria for deciding a Verification Plan while considering various available verification methods, verification time, and software costs. Several hardware design verification approaches from Formal Verification to Simulation based, Fully Automated Verification Plan to Security and Trojans are discussed. A Comparison between features and verification methods employed for Intel, ARM and RISC based processors is also done. The current RISC-V hardware design verification methods in use like self-checking tests, testbench use of standards, virtual verification peripherals and many more along with the required software and tools are described. In depth analysis of previous and cur- rent research on various available and newly developed RISC-V processors is chronicled with their code coverage, functional coverage, limitations and bug detection details.
Keywords RISC · Processor Verification · Functional Verification · Formal verification · Transaction level
1 Introduction as well as convene and govern related technical, industry, domain, and special interest groups. 1.1 Brief history of RISC‑V processor 1.2 Motivation RISC-V had humble beginnings. It started as a five-year pro- ject funded by Intel and Microsoft in the Parallel Computing RISC-V is a novel open instruction set architecture that sup- Lab (Par Lab) [1] at University of California, Berkeley in ports multiple platforms while maintaining simplicity and reli- 2010. In 2011, the first RISC-V instruction set was pub- ability. This universal ISA [5] supports numerous processor lished [2]. RISC-V International [3] was formed in 2015 as sizes, from embedded controllers, to high-performance com- a nonprofit organization that is the caretaker of the RISC- puters, and a wide variety of software stacks and program- V instruction set. Currently, the RISC-V landscape [4] has ming languages, Internet-of-Things (IoT) devices and personal more than 4,500 members across 70 countries, which con- mobiles. It is projected that more than 62.4 billion RISC-V tribute and collaborate to define RISC-V open specifications cores will be consumed by the market by 2025 (Fig 1). Android phones like Samsung, [6] are focusing on using RISC-V processors. Alibaba produced the first working Android 10 port for the RISC-V ISA [7], with GPU driv- Responsible Editor: D. Gizopoulos. ers; the T-Head XuanTie board booted Android in 2020 [8]. The major RISC-V manufacturer Sipeed showed a full
Savita Patil Android 10 system running quite smoothly on the XuanTie sypatil@ucdavis.edu C901 attached to a 7-inch-ish touchscreen. Chloe Tain NVIDIA is known for designing accelerators for AI and cltain@ucdavis.edu graphics processing that require up to tens of thousands of Hussain Al-Asaad cores. To manage these cores, NVIDIA has developed a hsalasaad@ucdavis.edu custom RISC-V processor called "NV-RISCV,"[10]. NV- 1 ECE Department, University of California, Davis, RISCV is based on an open-source ISA and is customized CA 95616, USA
Vol.:(0123456789)112 Journal of Electronic Testing (2025) 41:111–138
45,000 40,000 35,0002 30,000 2 H 25.000 § 20,000
15,000 10,000 5,000 0 2019* 2023* 2024* 2025* ®Computer ® Communications ® Transportation ® Industrial Other RISC-VFig. 1 Graph showing the potential growth of RISC-V in the CPU market. Adapted from [9]
much more deeply, with features like more customized devices before being made available to the user [12]. The caches and special instructions. NVIDIA Shipped One user then has to only do integration tests. Billion RISC-V Cores in 2024. Qualcomm is also already There are two forms of CPU design, CISC (Complex developing a RISC-V-based processor for Wear OS smart- Instruction Set Computer) and RISC-V (Reduced Instruction watches. The PULPino [11] processor from the Swiss Set Computer-V). CISC processors like Intel X86 proces- Federal Institute of Technology (ETH Zurich) is ready for sors, Motorola 68,000 family, AMD etc. have been in the industrial standards. PULPino is designed for low power market for a long time. RISC-V processors on the other hand consumption focusing on IoT applications. Dependable were developed to support the growing demand of proces- Real -time Infrastructure for Safety–critical Computer (De- sors for embedded systems. They were made open source RISC) project is using fault-tolerant techniques in RISC-V and free, with the focus on minimalism, modularity and cus- architecture for aviation and space environments. tomizable expansivity [13]. Other advantages of RISC-V are simplicity or commonality, no gap between education and 1.3 Comparison of CISC, RISC and ARM industry, openness/extensibility, and high programming effi- ciency [14]. RISC instructions started being used over CISC With the progress in information technology, the era of because of the ease of implementation, faster speed, and processors was influenced by large scale integrated technol- instructions function better when in parallel as in Table 1. ogy, and the processors have evolved over time. A proces- These features are not present in typical embedded system sor consists of a CPU (Central Processing Unit) also called ~~ development. Using different ISAs affect the performance the core, ALU (Arithmetic and Logic Unit) and Registers. and power consumption of applications, although different Traditionally, a CPU is single sourced and comes from the ~~ microarchitectural changes have a stronger effect [15]. ISA (Instruction Set Architecture) owner fully verified and The RISC-V hardware and software system is well docu- compliant to that particular ISA. An ISA is the specification ~~ mented, and the open design of RISC-V makes it able to that processors follow to verify instructions, hardware and adapt to diverse requirements in different fields. Active users software interactions, and several processor states. Around include NVIDIA Networking, Seagate, NSITEXE/Denso, 10 peta (10^15) cycles of tests are performed on the ARM Google Cloud, Chips Alliance, lowRISC, OpenHW Group, Andes, Valtrix, Nagra/Kudelski, Silicon Labs, multiple
4 Springer
Journal of Electronic Testing (2025) 41:111–138 113
Table 1 Comparison between Intel, ARM and RISC-V processor. Source: Adapted from [16]
× 86 ARM RISC-V
Origin Intel and AMD Arm Ltd RISC-V International
Instruction Set CISC RISC RISC
Byte Order Little- endian Typically big-endian (user configurable) Typically little-endian (user- configur-
able)
Applications Desktops, laptops, servers, workstations Mobile devices, embedded systems, low Embedded systems, IoT devices, custom
power servers solutions
Licensing Model Intel and AMD produce their chips ARM licenses its designs to manufac- Open-source, royalty -free licensing
turers
Ecosystem Large software and hardware ecosystem Large ecosystem, extensive third party Developing ecosystem, open-source
support initiatives
Code Density Higher than RISC-V Not competitive with variable length Lowest
instructions ISAs
RISC-V International Working Groups, and many others hypervisor support; and S, for supervisor-level instructions that are yet to be made public [17]. [18]. Table 2. describes selected RISC-V cores for both aca- demic and open source designs. 1.4 RISC‑V Base ISA The first two columns of Table 2. lists the core and sup- ported base ISA and possible extensions. Then the number The base RISC-V ISA is RV32I (primary base Integer) of pipeline stages and some of the implemented core fea- which has four primary base integer (I) variants: RV32I tures, e.g., branch prediction (b.p.) or out-of-order (OoO) (for 32-bit), RV32E (for 32-bit with 16 registers), RV64I execution, and available interfaces; the latter is of impor- (for 64-bit), and RV128I (for 128-bit). More functionali- tance for System-on-Chips (SoCs), ISA extensions and ties can be added through extension modules, such as M, coprocessor designs. opt. is from optional features; means for multiplication and division instructions; A, for atomic many core possible or only manycore; is in-order issue, com- instructions; F, for floating-point instructions; D, for dou- mit, OoO write back; 1.0 is a prefetch buffer for I cache. ble-precision floating-point instructions; G, comprising Finally, technology with ✓ denotes fabricated ASIC chips. the group of previously mentioned extensions; Q, for quad Some of the standard instruction extensions include float- precision floating-point instructions; L, for decimal floating ing Point, Bit Manipulation, DSP, Cryptographic, Vectors, point instructions; C, for compressed instructions; B, for Machine learning, Artificial Intelligence etc. Capturing the bit manipulation instructions; J, for dynamically translated value added to the users by using an extensible and custom- languages support; T, for transactional memory support; P, izable open source ISA,, the software community then can for packed-Single Instruction Multiple Data (SIMD) (Single focus resources on building a rich software ecosystem that Instruction/Multiple Data) instructions; V, for vector opera- has application and operating system portability across dif- tion instructions; N, for user-level interrupt support; H, for ferent implementations.
Table 2 Selected RISC-V cores: academic and open source. Source: Adapted from [17]
Core ISA # st Comments Interface Tech
Rocket RV64G,C 5 variable cache, opt. 1.2, MMU, b.p Tilelink Crossbar, RoCC ASIC ✓
BOOM (v1/v2/v3) RV64G,C 6/9/11 variable cache, opt. 1.2, MMU, b.p., Tilelink Crossbar, RoCC, integrated ASIC ✓ FPGA
OoO RoCC
Ibex (Zero—RISCV) RV32 I/E, C,M,B 2 + 1 opt. b.p., opt. L0, LSU PULP OpenHW eXtension, AX14, APB, FPGA ASIC ✓
crossbar
CV32E40P (RI5 CY) RV32IMCF 4 opt. L0, LSU, opt. L2, PULP AX14, APB, crossbar ASIC ✓
CVA6 (Ariane) RV64GC RV64IMC 6 variable cache, LSU, b.p., PULP AX14, APB ASIC ✓
VexRiscv RV32I MAFDC 2 + 3 opt. I/D cache, opt. LSU, OoO AX14, Avalon, wishbone FPGA ASIC ✓
PicoRV32 RV32I EMC 1 opt. I/D cache, AX14, MM, PCPI FPGA ASIC
SCARV RV32I IMC 5 side-channel hardened, LSU mem, mapped FPGA ASIC
SweRV (VeeR EL2) RV32I IMC 4 ultra-low-power core, I cache AX14, AHB—lite, mem, mapped FPGA ASIC
114 Journal of Electronic Testing (2025) 41:111–138
The base specification of RISC-V has been verified exten- methods such as theorem-proving, equivalence checking, sively and is frozen. There is a large and growing set of and language containment. standard and custom extensions available. With each cus- The advantages of formal verification are the exhaus- tomization, a highly optimized specialized design of the pro- tive state space coverage, no need for golden reference as cessor is created which is called Profile [19]. This Profile is designs are guaranteed mathematically, and no requirement unique and is application specific. The RISC-V Architectural for a generation of stimulus. The disadvantages of formal tests provide minimal verification to gain a RISC-V trade- verification are it uses memory extensively and has a longer, mark license for that particular RISC-V Profile. Although no upper bound runtime until the verification decision is RISC-V architectural tests are updated, they are created to made. This means that the designs have to be limited to help ensure that software written for a given RISC-V Pro- small state spaces. Also the specifications of the design need file will run on all implementations that comply with that to be translated into properties as formal verification will profile. Rigorous design verification is still needed for the exhaustively verify the properties and not the input vectors. RISC-V profile from the user side. In this paper, we will be The disadvantages can be complemented by using simula- discussing the various design verification strategies that are tion methods. The semi-formal verification method includes implemented currently across various RISC-V processors both simulation and formal verification to increase the state like Alpha, ARC, ARM, AVR, MIPS, PA-RISC, PIC and space restriction and perform an exhaustive test at these new SPARC. states. Assertion-based verification can also be applied by This paper is organized as follows: Section II describes adding assertions, statements about the design behavior that various methods that are used for verifying a hardware need to be verified. design. Section III explains what a verification plan is and proposes a plan for verifying a RISC-V processor. Section 2.2 Functional Verification IV gives a brief overview of prevalent approaches with their setup for verification of available RISC-V processors. Sec- In Functional verification, simulation of the operation of tion V of the paper compares verification of RISC-V pro- the design is done to ensure that the design behaves as cessors with critiques. The analysis is tabulated for ease of mentioned in the specifications. Test stimuli to the Design reference. Finally, section VI concludes the paper with direc- Under Test (DUT) is applied, and the outputs are observed to tion on future work. confirm that the specifications are met. The stimulus inputs applied to the DUT can be either directed tests or random tests [22]. [23] implements functional verification using Uni- 2 Verification Methods versal Verification Methodology (UVM) with System Ver- ilog. There is also an open-sourced riscv-formal [24] frame- This section describes the various design verification meth- work used by many in the RISC-V community. Functional ods for verifying a hardware design. Different methodologies verification can test more scenarios and use cases because for verification are available to verify hardware more effi- of the ease of simulations/testbenches but with the main ciently than using just simulation and testing. These include disadvantage of not having the same level of exhaustive formal verification, functional verification, coverage, error verification as formal verification methods. Advantages of modeling, golden reference model and compliance testing. functional verification include being time saving, less com- We have briefly explained them in this section. plex, and more flexible. Even complex and large designs can be verified using functional verification as waveforms and 2.1 Formal verification logs are provided which can be analyzed. Other disadvan- tages include incomplete coverage as not all possible input Formal verification is a way to check the functionality and scenarios are explored; and heavy reliance on the quality and correctness of a design through mathematical methods. completeness of the testbench. Typically, verification starts with a top-down approach where a high-level block diagram of a design is verified 2.3 Coverage with mathematical specifications and then a more detailed dive into different blocks to be verified is done. The main Different types of coverage are used to check that all pos- piece of formal verification is to focus on the properties one sible inputs and specific errors have been verified through wants to verify in the design. [20] explores model checking, the testing methodologies used. Functional coverage of test automata-theoretic approaches, deductive methods, and a cases describes the amount of states or specifications exer- combination of model checking and deductive reasoning as cised out of all possible paths. FSM (Finite State Machine) some of the different techniques to prove if an implementa- coverage helps in functional coverage verification by assign- tion agrees with the specifications. [21] mentions other proof ing states and transitions to be traversed.
Journal of Electronic Testing (2025) 41:111–138 115
- Fault coverage verifies the physical hardware errors in CPU as the features we choose impact its verification and the system through manufacturing tests. consequently the verification plan. Developing your own
- Test coverage looks at the extent to which design errors CPU adds incremental schedule, resources, and quality are detected and how well tests verify functionality [25]. challenges. Existing DV methodologies do not completely
- Code coverage checks how much of the test code is exer- address these challenges. Until 2021, there were no com- cised during verification. The main steps of coverage mercial products available to support DV of RISC-V pro- verification include a verification plan, coverage metrics, cessors [27]. test generation, coverage tests checked and modified A typical CPU hardware design verification involves depending on the metrics. making a verification plan on what needs to be verified and then developing the measurement metrics. The veri-
2.4 Error Modelling fication plan is a comprehensive document that contains the decisions on which EDA tools, models, and methods Error Modelling is used to bridge the gap between test gen- to be used. It will also contain the simulation choices, it eration and tests not covering certain design errors. Com- will involve open source, commercial, bespoke, System parison for errors is done between the implementation in Verilog, UVM, FPGA (Field Programmable Gate Arrays), a hardware description language (HDL) and specification, Emulation and Formal Verification etc. Then, procurement which is usually the ISA. The basic error models cover bus of the tools, testbenches and reference models is done. solid state logic (SSL), module substitution, bus order, bus After the reusable tests for subcircuits are obtained, new source, and bus driver errors with manual test generation tests are created according to the verification plan. [26]. For more complex error models to target more specific A huge number of pseudo random tests are generated errors, a condition is implemented for a basic error to be and verified until functional and code coverage metrics are activated only if the condition is satisfied. High coverage of reached. A processor verification plan typically focuses on actual design errors is achieved with tests generated for these key metrics for coverage, but while selecting a verifica- basic and conditional error models. tion methodology, the efficiency of finding and investi- gating the divergence should also be considered. Lastly, 2.5 Golden Reference Model benchmark, soak and integration testing is performed [28]. Benchmark measures the performance of a proces- A golden reference model (high level descriptions of the sor against industry standards, soak sees the performance design) is typically used to verify the outputs from a sim- after putting stress/a large load for a long period of time, ulation against a high level model implementation of the and integration attempts to expose faults between interac- original design at the transaction level (e.g. read transaction/ tions of different integrated units. The Verification plan write transaction), instead of signal level. At the end of each also contains criteria for completeness, tasks priorities, transaction the outputs for the DUT and the reference model the schedules and milestones. are compared and logged to the simulation log file. The need for standardization that is good for both IP users and vendors arose and UVM [29] standard came into pic- 2.6 Compliance Testing ture. UVM standardization effort lowers verification costs and improves design quality throughout the industry with Compliance testing [27] is a verification task that serves its reuse and portability feature and the ease of customer to see if a design meets certain standards. The verification support. RISC-V Verification Interface (RVVI) from 2020 process is explained in detail in the verification plan below. has worked on standardization of communication between To see if a processor meets RISC-V standards, a nonfunc- testbench and RISC-V Verification IP from companies like tional compliance test is performed to see if a specification Imperas, EM Micro, SiLabs and OpenHW [28]. has been interpreted correctly and the DUT can be declared SystemVerilog is the hardware description and verifi- as RISC-V compliant. cation language mainly used today as it captures both the design and verification environment. The advantage of SystemVerilog over Verilog is the OOP (Object Oriented 3 Verification Plan Programming) aspect and enhanced verification resources. Some of the major components of a SystemVerilog testbench In this section we cover what a verification plan is and why as in Fig. 2 include a stimulus generator, a driver to direct there is a need for one. When we use a traditional CISC stimulus to the DUT, a monitor to check the behaviour of the CPU, 50% of the SoC cost goes towards HW DV (Hard- DUT, a scoreboard to compare between the monitor data and Ware Design Verification) even though they have a proven a reference model, assertions for debug ability/observability, IP. There are several challenges while verifying a RISC-V coverage, an agent that groups together the major classes in
116 Journal of Electronic Testing (2025) 41:111–138
flexibility when developing and validating RISC-V func-
tional test programs.
The design verification module for RISC-V processor
consists of a reference model, verification IP (Intellectual
— Property), and tools/simulators as shown in Fig. 3. A proces-
sor has a more extensive state space, which requires more
1 tools to account for asynchronous events, synchronization
between the processor and reference model, and state com-
Reference | |Comparison| parisons between the two. Additional requirements include
functional coverage of the full instruction set and custom
instructions provided by a user as well as a comprehensive
vee | wer architecture of a reference model [24]. Usually, the RISC-V
processor used is in RTL. A comparison between verifica-
tion of an SoC and a RISC-V processor can be performed.
Verification IP is a type of reusable IP that can gener-
ate comprehensive tests for shortening SoC verification and
increasing test coverage. Verification IP is often used to
verify standard bus protocols.
Fig. 2 UVM SystemVerilog Testbench. Source: Adapted from [23]
4.1 Stage 0: Entry Level “hello world” test
UVM (sequencer, monitor, driver), and other components to This novice approach where running a basic program like
be customized in the test environment. printing “hello world” confirms that the CPU is working
correctly. This method can be used for testing of chips in
research, academics or by hobbyists but cannot be used for
products that require higher quality [28]. The test requires an
4 RISC‑V CPU HW DV Approaches HDL Simulator, FPGA, or silicon, and a test harness to run
programs. This can not be considered as DV but shows the
In this section we will discuss the hardware design verifica- design is ready for a more robust test plan with software as
tion approaches specifically for RISC-V processors that have input stimulus that can now exercise the design more com-
been used till date. Starting with the most basic to the latest pletely [29].
research going on in this area. Processors are expected to have the highest level of quality IP. But RISC-V processors ~~ 4.2 Stage 1: Simple Level, Self checking tests users can have the same flexibility in verification as they get while designing the processor. Some of the tools of the ~~ 4.2.1 Simple Check RISC-V ecosystem include compiler, instruction set simu- lator, virtual prototype etc. [18], along with the electronic A simple but not robust DV solution that needs basic ISS design automation (EDA) software. These tools provide (Instruction Set Simulator) and toolchains for simple test
Fig. 3 Basis of verification
block diagram. Source: Adapted
from [24]
Platform
HW-SW CPU Model
DV Use Case Simulation -
Emulation for
Reference) (Verification
4 Springer
Journal of Electronic Testing (2025) 41:111–138 117
runs and basic functionality testing. It still needs an accu- checksum), which were added recently. It is a free and open rate, configurable, version selectable and complete refer- source generator [33]. ence model [28]. The RISC-V OVP (OPNFV Verification Program) sim ISS is one such free closed source ISS from 4.2.4 Compliance Tests Imperas that works with no compiling, no fiddling and no external dependencies. In Fig. 4, it is used as an architec- After running RTL DUT in testbench, the ISS is run and log tural reference or even as a golden simulator to verify their or signature files are written on. The file results are com- RTL in a hardware design verification methodology. They pared or differentiated. This approach is taken by RISC-V implement the full and complete functionality of the RISC-V International for their architectural validation or “compli- Foundation’s public User and Privilege specifications [30] ance tests”. The RISC-V international architectural compli- and [31]. ance test suites are configured as tests with an integrated Another approach with the test program is to build in signature to indicate a pass. The test suites are designed to a self-test or signature result to indicate a satisfactory illustrate a basic level of conformance to the RISC-V speci- conclusion. fication without any attempt at detailed functional verifica- tion [29]. 4.2.2 U.C. Berkeley’s Torture Test These signature file comparison approaches do not give a robust DV solution. Their shortfalls are compensated with The RISC-V torture test generator creates a single random the following methods. torture test, which is run on particular simulators using 4.3 Stage 2: Post Simulation Trace log File Compare testrun sub-project. The resulting signature is then com- pared with the ISA simulator to determine how or where A Sophisticated method to do comparison testing to extend they differ. The Overnight sub project allows repeated test the comparison over full instruction trace-level analysis [29]. runs for a given duration or until a failure count is reached. Tests are created using a random generator, ISG (Instruc- The torture test framework is written in Scala [22] and needs tion Stream Generator) and applied to both RTL under test to be updated periodically [32]. and ISS, reference mode. Separate trace log files are written when simulating ISS and RTL and run through a compare 4.2.3 Shakti’s AAPG Tool program to observe differences or failures [28]. Several cor- ner cases are covered by the random yet constrained genera- The Automated Assembly Program Generator tool generates tor to provide both legal and valid instruction sequences. random RISC-V programs to test RISC-V cores. It is actively To support this trace-based f low, Imperas has maintained and contains features of self-checking tests (via free reference model riscvOVPsimPlus (Fig. 5). The
Fig. 4 Simple log or signature Imperas riscvOVP sim compliance simulator file comparison method with free riscvOVPsim from GitHub. CPU model variant Source: Adapted from [28] selection and configuration
— riscvOVPsim= = 3
RISC-V reference model
(CPU &
Application Semihosted File
<cross>.elf 1/0 File Compare
Application RISC-V.org Signature
4 Springer
118 Journal of Electronic Testing (2025) 41:111–138
Fig. 5 Design verification RTL
using Co-Sim with reference Simulation
model. The post-simulation —
trace-compare method with the ® 0
free riscvOVPsimPlus. Source: Memory i
Adapted from [29]
LLVM ‘Compare’
(CPU+ Memory
RISCV.c RISCV.elf Imperas.log
riscvOVPsimPlus [34] extends the functionality of riscvO- compares Program counter (PC), Control and Status Register
VPsim with more features such as fully configurable instruc- (CSRs), General Purpose Register (GPRs) and other inter-
tion trace, GDB/Eclipse debug, and memory configuration nal states, instruction by instruction to look at the execution
options. Additionally in the model are: CLIC, Debug Mod- flow, program data, and programmers/internal state (Fig. 6).
ule/Mode, multi-hart, H-hypervisor simulation, and also ~~ The immediate comparison allows for debug examination
the recently ratified ISA extensions: V-vector, B-bitmanip, directly at failure. The drawback is that it will not work for
K-crypto (scalar), and Zfinx, and the'near-ratified'P-SIMD/ asynchronous events, control flow, and hardware real time
DSP, Zmmul [35]. effects. The reference models and optional development are
Google’s risc-dv instruction stream generator, COREV- not open source yet. The method was used for CV32E40P
DV is implemented as a collection of SystemVerilog classes in OpenHW 1H 2020 [28].
extending from uvm_object [36]. This approach can be applied with increasing levels of analysis starting with the ~~ 4.5 Stage 4: Async‑lock‑step‑compare DV program flow, basic PC (Program Counter) monitoring, pro- gram data, and monitoring all of the processor registers and ~~ This approach derives from the industrial quality sync-lock- memory changes [29]. However, it has efficiency limitations step-compare to add asynchronous events. Instruction by and bulky trace files which make it harder to manage and instruction analysis helps us verify several processor archi- analyze and therefore considered suitable for simple proces- tectural features such as hardware multithreading, debug sors. Also, the cause of the error generated cannot be found mode, interrupts, out-of-order (superscalar), multiproces- as only trace files are there that generated the error. sor, and heterogeneous arrays, plus the flexibility of the RISC-V Vectors specification for AI (Artificial Intelligence) 4.4 Stage 3: Sync‑Lock‑Step‑Compare or Data‑Path and Deep Learning compute engines. Some SystemVerilog Lockstep‑Compare components used are a report of instructions and registering writebacks, a functionality check and reference model man- In the lockstep synchronization, two or more similar devices ~~ agement, and properties for interrupt and debug coverage/ share the same timing and triggering, acting as a single checking. This approach is costly and complex as it deals device. Both the reference and DUT are run together, and with asynchronous information. CV32E40P in OpenHW 2H this setup requires no data-saving and has a simplistic setup, ~~ H2020 has used the Async-lock-step-compare DV approach depending on the RTL DUT tracer features. This test process in Fig. 7. This approach is considered the gold standard in
Fig. 6 Coverage Driven Veri- [SystemVerilog Test Bench
fication of RISC-V processor [own |
in a SystemVerilog test bench
using Imperas RISC-V Golden @ |
Reference Model for step-and-
compare. Source: Adapted from Geel Step |
[28] Ref a
results.log
4 Springer
Journal of Electronic Testing (2025) 41:111–138 119
Fig. 7 The OpenHW CORE-V- Testbench
VERIF test bench as used for
CV32E40P. Source: Adapted
from [29]
CORE-V
1 RTL
EEE
|nterruj
Reference Model
dynamic (simulation based) verification and represents the Testbench
best DV environment currently available for RISC-V [28]. Vip driver
4.6 Using Standards Based DV Products and VIP HH using he | Model
Functions 0 |<
H
(ImperasDV) 18
H
ImperasDV provides integrated solutions for RISC-V pro- [|
cessor verification for both RTL bug detection and analysis, || [RE suchasclient
when combined with design flow integration for the leading vial vinual fre
EDA SystemVerilog environments with Cadence, Siemens
EDA, and Synopsys [37]. The ImperasDV Verification IP Verilog Verilog or
options have been extended to include riscvISACOV [38], a
set of SystemVerilog source functional coverage libraries for Fig. 8 Testbench for Advanced RISC-V Design Verification. Source:
all of the ratified instruction extensions like interrupts and ~~ Adapted from [37] dynamic effects, and the first release of the privilege mode libraries to be used in conjunction with the effects of asyn- models to fully support the ‘lock-step-compare’ verification chronous events during verification. Imperas also include approach [37]. architectural validation test suites for RV32E, RV64E, Zc, Imperas provides examples of use of RVVI with its and Zmmul specifications [31]. ImperasDV product with C/C + + for Verilator designs and SystemVerilog for use with Xcelium, VCS, Questa from 4.7 Test Bench Use of Standards (RVVI) Cadence, Synopsys, Siemens EDA respectively. OpenHW is using RVVI in its CV32E40X open source SystemVerilog The RISC-V Verification interface (RVVI) is a draft open test bench. standard that makes reuse of testbenches, test generators, Currently, RVVI addresses three different areas as shown functional coverage and other testing methodologies pos- in Fig. 9 and described below. sible (Fig. 8). RISC-V CPU RTL verification in a Verilog Simulator needs an interface between the core RTL, the test ~~ 4.8 RVVI‑Trace bench and other verification components [39]. Currently, RISC-V components have their own specific test benches ~~ The core DUT RTL Trace interface that gives signal level as seen in Fig. 8 and hence require their own custom inter- interface to RISC-V VIP (Fig. 10). It defines information to faces. The process is inefficient and time-consuming so be extracted by tracer while using SystemVerilog interface RVVI makes re-use of interfaces possible among several of and includes functions to handle asynchronous events like the subsystems of RISC-V processor DV. RVVI provides a interrupts, debug requests etc. common methodology for the key components of the test- The primary RVVI-TRACE interface, rvviTrace, asks bench to connect the RTL instruction trace and reference ~~ for a number of parameters like maximum permissible
4 Springer
120 Journal of Electronic Testing (2025) 41:111–138
Testbench Imperas as part of ImperasDV) and issues the appropri-
[ ate calls.
I
control (= 4.10 RVVI‑VVP (Virtual Verification Peripherals)
When testing a processor there are components needed in
5 Q the test bench to interact with the processor—for example a
= = virtual UART to print information from the program opera-
= tion, and timers to generate asynchronous interrupts. These
x components [42] are being defined so that they can be used
in C/C + +, SystemVerilog, test benches, and also in some
cases within ISS—to allow ease of test creation. This RVVI-
VVP is currently a work in progress and is looking to cover:
Fig. 9 Three different areas addressed by RVVI. Source: Adapted timers, interrupts, debug, random event generators, and
from [28] printer/log/UART capabilities.
valid | 5 Comparison of Verification of Various
msl 9 RISC‑V Processors
I = J This section discusses the various verification methodolo-
= = 2 gies used in the last 5 + years for the RISC-V processors cur-
netpop) | fy rently in the market. We have tabulated the findings which
cover the framework used and discuss important metrics. In
Fig. 10 RVVI Trace Interface. Source: Adapted from [27] Table 3 placed before Reference, code coverage, functional
coverage, bugs detected, extensibility to other processors,
limitations, and other benefits are cataloged. Functional
instruction length in bits and then provides internal visibil- and code coverage provide a measure of completeness with
ity of the state of the RISC-V device for observing the state ~~ which the design has been tested by the verification tests. transitions and state values [40] in waveforms. The data con- Areas of low coverage can indicate vulnerabilities to bugs veyed on this interface should not be relied upon to persist ~~ and corner cases. To mitigate this concern of a verifica- beyond an individual event. tion method with low coverage, bug detection also has to be taken into account. Another important column is if the verification environment be extensible to other processors, 4.9 RVVI‑API which means the same environment can be applied for other subsequent designs or versions of processors, making it very The function level standard interface for lockstep compari- cost efficient. son between RISC-V VIP core and a reference mode DV The research area of verification is known to be challeng- subsystem for DV purposes. The RVVI-API interface con- ing, but the extent of this challenge is addressed in [43]. Few tains a set of API function calls that abstract away many of challenges in verification are reducing test power for testing the details of the operation of processor reference models integrated circuits, concurrency of software on multicore and decouples the test bench from any specific reference systems, integration validation and IP reuse in SoC designs, mode [41]. generation of complete assertions, and synchronization of The RVVI-API is a C/C + + API and can be used with analog and mixed-signal designs. It is common to mitigate C/C + + test benches. RVVI-API also is defined with a Sys- these challenges through domain-specific tools, theories, and temVerilog DPI wrapper to be used in SystemVerilog test ~~ methodologies, but there needs to be a united framework to benches. address all these issues. [44] has classified and evaluated the There are two general approaches for driving the RVVI- survey of RISC-V architecture software support into four API interface: main categories: application fields, RISC-V implementa- tions, software architecture, and deployment features. This a) Directly from a test bench via DPI calls. work gives a comprehensive overview of the RISC-V soft- b) Indirectly by a SystemVerilog module which monitors ~~ ware support for various processor cores, SOC platforms, the rvviTrace interface (such as trace2api provided by emulators and simulators, highlighting the recent software
4 Springer
Table main methods utilized for the verification. Subsequent columns contain code coverage, functional coverage, bugs detected, extensibility to other processors, limitations, and other benefits 3 No Tabulation of verification of RISC, MIPS and extensions discussed in the paper. The second column contains the processors with added extensions if applied. Third column has the Processor Proposed Verification 1 Chipcraft Sp. z o. o. method Code Coverage Functional coverage Bugs detected Extensible Limitations Other Benefits Ref company’s CC100- sembler used for one instruction per functional verifica- N/A N/A Identified accurate clock cycle on a N/A [22] C processor Emulator and disas- tion positions of errors Yes Can execute only for CSRs 2 RISC-V 32I based single processor age different for dif- tion: not completely Concise, cost efficient [46] processor Siwa Block and chip level core. Little support functional verifica- random programs; tion; SystemVer- Yes (amount of cov- ferent instructions) N/A Yes Chip level verifica- ilog/UVM erage not specified) Yes (amount of cover- considered many communication 3 32-bit RISC processor protocol interfaces; IP core Coverage driven N/A Yes (instructions N/A N/A OVM lacks support/ constraint random registers accessed coverage not speci- capabilities UVM temVerilog/OVM fied) 4 verification; Sys- internally only Flexible/open- [48] MIPS (Million can provide sourced OVM verification to can be handled at Instructions Per Constrained random validate functional in future works) Yes (100% functional Second) Micro- N/A (will implement verified; amount of behavior of all coverage) N/A N/A Only one instruction processor (16 bit, a time Mostly automated, 5 stage pipelined data dependent accurate [49] processor) high speed and End-to-end testing 5 A-Core (open-source instructions, units, for RTL taking Code flexibility, environment; test 32-bit RISC-V pro- and instruction cessor w/AXI4-Lite combinations interface to self- memory bus ASIC); Python longer for C vs. structure and JTAG parts of design N/A N/A N/A Yes Simulation run time programming flow (RTL, FPGA, interactive user [50] (SyDeKick) w/test- interface) ASIC framework Assembly programs write programs benches and tests
Journal of Electronic Testing (2025) 41:111–138 121
Table (continued) Proposed Verification No Processor3 6 Newly designed method Code Coverage Functional coverage Bugs detected Extensible Limitations Other Benefits Ref form; CoreMark RISC-V processor; Testbench plat- three-stage pipeline debug in ARM in Harvard (measures the N/A N/A N/A N/A Lack of memory architecture; based performance of the speed Allows users to easily benchmark); Self- on RV32IM processor across a simulate tests and [13] checking to check that the processor follows the instruc- tion set architecture; ROM and RAM verified for storage data 7 RISC-V processor and communication different RTL that boots linux, protocols to transfer ency on hardware Comprehensive levels; simulation of N/A Yes N/A N/A Time and resource preDAC ISA testing for RISC-V ISA tests, intensive, depend- RISC-V lowRISC across RTL stages, and booting the early detection of [51] linux kernel 8 64 bit high perfor- tests, torture tests, issues mance RISC-V and FPGA proto- processor support- Dynamic simulation ing B-extension type verification N/A Yes N/A N/A Time consuming, Low power con- 9 MINRES The Good may not cover all 32 bit pipelined targeting RISC-V immediate values implementation as performance, small core(ISA and CSR Yes Complexity of the High performance RISC-V core of Cross level testing N/A Yes (99.6% possible 10 bugs in RTL edge cases sumption, good [52] across all instruc- handling); 1 bug in Folk (TGF) Series ISA tions) reference ISS; all the main challenges code size [53] bugs found in less completed instruc- tion in the RTL and than 5 min are detection of a utilization of the stream b/w the RTL and ISS 10 RISC-V base instruc- same instruction tion Automatic verifica- operation, genera- tion for instructions N/A N/A N/A Yes Lack of directed tests and functional tion of files in vari- [54] coverage Flexible, ease of ous formats
122 Journal of Electronic Testing (2025) 41:111–138
Table (continued) Proposed Verification No Processor3 11 Open-source 64-bit method Code Coverage Functional coverage Bugs detected Extensible Limitations Other Benefits Ref RISC-V proces- mal verification; sequence dependent bug detection; iden- N/A No proof for existing translation of Sail N/A N/A Single instruction and sor Flute with a End-to-end for- tify most bugs in RISC-V instructions five-stage, in-order as the focus is more N/A [56] specification to CHERI instructions on CHERI instruc- pipeline CHERI-RISC-V SystemVerilog between bugs and Assertions; proof of and can distinguish 12 CHERI-Flute prop- tions MIPS and RISC-V engineering features tion with property gates for opcode processors(16-bit to erties with proof trojans within Yes Verification time checking N/A N/A Verified 400,000 128-bit) Formal verifica- 10–30 s complexity; many 13 VAMP (Verified increases with Efficient [57] Architecture Micro- tion by theorem- specification func- other trojans to be tion in execution N/A N/A Required 60% prover PVS N/A Verified completely processor) 32 bit Gate- level verifica- RISC-V processor, detected a DLX processor fication System). interrupts interface to specifi- Verified modules units and only 3% for Explorer tool that variant w/a Toma- (Prototype Veri- in execution units of execution units, provides intuitive [60] sulo scheduler, verification effort Developed VAMP- precise and nested cation and verifica- interrupts the parameterized tion of VAMP rithm, actual data pipeline without interrupts 14 Tomasulo algo- RISC-V RV32I pro- management of the cessor Polynomial formal verification based N/A N/A N/A Yes Complexity of BDDs Simplify complexity on Binary Deci- sion Diagrams; ITE of CPU verifica- operator (If–Then- tion; fast and use [61] Else) is used to little memory calculate the results of the logic opera- tions in BDDs
Journal of Electronic Testing (2025) 41:111–138 123
Table (continued) Proposed Verification No Processor3 15 RV32I based method Code Coverage Functional coverage Bugs detected Extensible Limitations Other Benefits Ref MicroRV32 Polynomial Formal cation of multi- Verification method using BDD and Yes Yes (complete verifi- time for ALU = equivalence check- cost. Verification ing. Used SYSSIM cycle processor) N/A Yes N/A Efficient and low to verify sequential multi-cycle proces- ns 200 [55] sor 16 Commercial RISC-V sub-circuits of the bugs Yes Need for extra processor Model checking based blackboxing for High security stand- formal verification N/A N/A Detection of design using Jasper some properties to 17 32-bit ISA RISC-V successfully prove ards [62] processor Combination of Yes (amount of cov- N/A ALU misbehaviour, Yes Cost: μGP needs a simulation- and them within a 24 h formal-verification; time frame Maximized processor ruption execution simulation environ- simulation: drives erage not specified) faulty comparisons, state coverage [65, 66] automatic program data hazards, inter- generation using detected ment, RAM, and the RISC-V Formal genetic algorithms software adapta- to maximize cover- verification needs age of the test and tions; formal contrast against an ISS; formal: Interface (RVFI) for 450 individuals interface carries and hardware adap- specific processor tations; Run time states according to min for 51 tests ISA spec for μGP is 90 min 18 single-issue in-order code coverage) N/A 10 bugs in RTL core and formal is 45 (SIIO) 32-bit, 5 odology with three Yes (93% for total stage RISC-V ISA Functional/formal Low cost, no time- based processor verification meth- tional verification ISS; all bugs found formal and func- verification stage 1 bug in reference implemented in mainly from ISA to detect bugs as Chisel HDL step pre-silicon ISA and CSR handling; Yes High effort for early as possible; in less than 5 min methods made testbenches [67] coverage driven complex designs in consuming human framework
124 Journal of Electronic Testing (2025) 41:111–138
Table 3 (continued) No Processor Proposed Verification Code Coverage Functional coverage Bugs detected Extensible Limitations Other Benefits Ref 19 RISC-V base with any method extensions Generate Software- N/A N/A N/A Yes Ongoing research to Typical testing times [18] based Self-Test automatically gen- for SLT range from (SBST), Self Test erate SLT programs 15 min to up to 2 h libraries (STL) instead of manually and Burn-In (BI) programs using 20 CHERI with security Chipyard extension Used TestRIG N/A N/A Discovered cache Yes Ongoing research to Detects problems [68] with QuickCheck bugs in memory extend it to several with micro-archi- VEngine to com- mistakes other RISC proces- tectural mistakes municate over RVFI sors (register forwarding and DII sockets to and flushing the exhaustively testing pipeline); memory faulty instructions mistakes and unex- in pipeline pected interactions
Journal of Electronic Testing (2025) 41:111–138 125
architectures, development tools and operating system archi-
tectures in detail.
We have divided the section into three subsections—func-
tional, formal and combination of both functional and formal
verification. Each subsection is subdivided into the main
methods that were used for verification.
5.1 Functional Verification
This subsection covers the various functional verification
methods used for verification of a RISC processor.
5.1.1 Emulator and Dissassembler
One implementation of a RISC-V Processor Core verifica-
tion done on Chipcraft Sp. z o. o. company’s CC100-C pro-
cessor [22] includes an emulator and disassembler written in
Verilog. The verification environment implements an emula-
tor golden reference model (Fig. 11) to check for errors in
the instruction flow of the processor RTL and a disassembler
to output executed instructions. There are many resources
to support the environment, including a framework for for-
mal verification, direct and random test generators for func-
tional verification, and compliance tests. The overall result
is a successfully implemented master (processor)—checker
(emulator) verification. The processor tests were written in
assembly or C code and used the Newlib cross-compiler
from the RISCV repository. Positions of errors were identi-
fied accurately, which helped in fixing bugs. However, only
one instruction per clock cycle can be executed on a single
processor core, and there is very little support for Control
and Status Registers (CSRs). CSRs [45] contain additional
information about the results of instructions in the CPU,
and the emulator can only use whatever is provided from
the processor without access to the CSRs information. The
design environment created by [33] can be used to design
and verify several other RISC-V processors too.
5.1.2 Block and Chip Level Functional
Another implementation of functional verification [46]
uses SystemVerilog and UVM on a RISC-V 32I based
processor, called Siwa, which is the main controller core
of a medical implantable tissue stimulator. UVM provides
the advantage of being standardized with online support,
a workspace for reusable code, and constraining and ran-
domizing test cases for maximal coverage. The processor
environment gets split up according to hierarchical lev-
els into block and chip level verification. For block level
verification, an arithmetic logic unit ALU, memory bus
controller (BMC), system bus, and Universal Asynchro-
nous Receiver-Transmitter (UART) port were implemented
with UVM with individual architecture specifications and
126 Journal of Electronic Testing (2025) 41:111–138
Fig. 11 Emulator connection
with processor under test.
Source: Adapted from [33] emu_proc
| 086
Local Coherent Interconnect Matrix
Interrupt Controller ae On-Chip Data’ Scratch-Pad MPU Controller Controller RAM RAM 0
Local Coherent Interconnect
a transaction-based reference model as seen in Fig. 12. The Some restrictions that come with the chip level verifica-
tests generated were randomly generated and constrained tion environment [46] are that programs may not be com-
based on the verification plan. For chip level verification, pletely random, many communication protocol interfaces are
the RISC-V core DUT has a standardized golden refer- to be considered (SPI [47], UART, GPIO), and registers may
ence model where handmade tests are developed using only be internally accessed. Basic shell programming was
a C Assembler compiler from the Sifive Toolchain. The used for regression testing with seeds generated from python
RISC-V simulator RV8 is used in tandem with a custom for pseudo random tests. The user specifies the number of
reference model written in SV, validating itself against tests to run for coverage, and regression testing is used to
RV8 simulation results. continually run the tests specified number of times. Benefits
Fig. 12 Block level verification,
testbench implementation using
UVM architecture. Source:
Adapted from [46] Reference Model
1
gent (TX) UVM_Agent (RX)
UVM_Sequence UVM_Sequence
Test TUM Test LE TM
UVM_Driver Monitor UVM_Driver Monitor
Simulus
4 Springer
Journal of Electronic Testing (2025) 41:111–138 127
of this implementation include flexibility to be applied to verification environment and processor. An analysis layer, other digital designs/different tools, conciseness and cost reports output comparisons between the processor and the efficiency, and availability of coverage metrics when per- predictions. The operational layer is a set of components that forming hierarchical verification/regressions. provides the necessities for the processor to operate includ- ing transactions. Transactors convert between transaction 5.1.3 Constrained Random Verification level and pin-level worlds. To test and validate functional behavior of all data In [48], the approach is to implement coverage driven con- dependent instructions, units, and instruction combinations straint random verification with SystemVerilog and Open in a MIPS (Million Instructions Per Second) Microproces- Verification Methodology (OVM). OVM is very similar to sor (16 bit, first 5 stage pipelined processor-instruction UVM as both are based on a SystemVerilog standard, incor- fetch, decode, execution, memory access and write back) porate OOP and reusability, and include functional coverage ~~ [49], UVM was used with SystemVerilog using CRV (Con- with constrained-random inputs. UVM is more popular as strained Random Verification) approach. Limitation in the it is based on SystemVerilog libraries and has more sup- ~~ CRV approach is that only one instruction can be handled at port/capabilities. However, OVM is open-sourced for easy a time. Individual instructions and data dependent instruc- accessibility and has a layered approach to the verification tions are verified separately with functional coverage in cov- environment/testbench, which makes it flexible and matches erage bins implemented in EDA playground using Aldec with the architecture of RISC-V and breaks down the dif- Riviera Pro 2022.04 tool. Every instruction set in the pro- ferent parts needed for verification as shown in Fig. 13. The cessor is covered and verified through the coverage module processor acts as the DUT and interacts with the following in Fig. 14. This verification method is mostly automated, layers. The control layer allows communication between the high-speed, and accurate.
Fig. 13 Architecture of the OVM testbench. Source: Adapted from [48] 5
Q
oO
[=
© f= B o
a= @ [=]
4 Springer
128 Journal of Electronic Testing (2025) 41:111–138
Fig. 14 Coverage module for
UVM using CRV. Source:
Adapted from [49]
— Master Agent |]
©
232
I<) a |
Slave Agent
5.1.4 End‑to‑End Python ASIC Framework with AXI4-Lite memory bus structure and JTAG (Joint Test Action Group) programming interface which is a Having a flexible choice of specifications on a RISC-V custom, extensible and configurable RISC-V micropro- processor is very beneficial. The verification environment cessor targeted for controlling communication, cryptog- in [50] aims to provide users the opportunity to self-write ~~ raphy, and machine learning hardware accelerators, and programs for end-to-end testing to test various parts of setups for RTL, FPGA, and ASIC simulations. There is the design flow (RTL, FPGA, ASIC). The environment plenty of support for an interactive user interface and code built from a Python ASIC framework (SyDeKick) includes flexibility. The result is an end-to-end environment that testbenches and tests designed for the A-Core (Fig. 15) allows testing on multiple configurations of the proces- an open-source 32-bit RISC-V processor implementation sor with different simulation execution times displayed. A
Fig. 15 Block diagram of Programming Interface
A-Core SoC. Source: Adapted
from [50] = ACore CHIP
1 enable ACoreBase —IN\ | 8 ] “\5H a |
— al LL =
4 Springer
Journal of Electronic Testing (2025) 41:111–138 129
drawback is the simulation run time for RTL takes longer 5.1.6 Cross Level Testing for C vs Assembly programs. Many RISC-V processor verification plans use simula- 5.1.5 Simulation, Testbench, and Self‑Checking tion testing to detect bugs with a need for ideal test case generations. Cross level testing aims to provide an end- Verification using simulation testing and downloading less generation of instructions for test cases that can adapt debugging to verify a newly designed RISC-V processor is during simulation depending on the instruction stream discussed in [13]. The processor consists of a three-stage requirements in ISA [53]. Cross level testing consists of pipeline by ARM in Harvard architecture to allow independ- co-simulation to send the instruction stream to the RTL ent parallel processing and storage of instructions and data and reference ISS for comparisons (Fig. 16). To generate in separate memories. For verification, first the performance the instructions for testing, randomization is used with of the processor across a benchmark is measured using Core- the following modifications: random instruction opcode Mark. Self-checking is then used to check that the processor injected to specify a valid instruction, mutated instruc- follows the ISA. ROM and RAM, memory storage units, tion fields implemented depending on structure and value are also verified for storage and communication protocols rules, and instruction sequences created for specific tasks. to transfer data. This RISC-V DV allows users to easily Several bugs were found with this method for both the simulate tests and debug. The only downside is the lack of 32 bit pipelined RISC-V core of MINRES The Good Folk memory speed, which they propose to fix in the future by (TGF) Series and the ISS with over 200 million processed adding a cache. Embedded system support development will instructions per hour. This verification method shows a also be needed in the FPGA later. very high performance with high coverage and can be A verification approach built upon a RISC-V processor extended to other RISC-V ISA configurations easily. How- that boots linux, called preDAC, is presented in [51]. The ever, the implementation of the method is very complex, verification process is broken down into RTL, post-synthe- making detection of completed RTL instructions difficult. sis, and post-place and route. For RTL, 395 ISA tests were The paper identifies these challenges and addresses them performed to check if instructions were executed properly. with solutions successfully. In addition, an extra gate simulation test was performed for activity and power estimation information. FPGAs were then used to mimic the final design and self-test the SoC. 5.1.7 Automatic Verification RISC-V ISA tests, RISC-V lowRISC tests, torture tests, and booting the linux kernel were executed on the FPGAs. A With verification becoming more complex due to an increase debug infrastructure is also used to verify the state of the in design complexity, an automatic verification plan for SoC at run-time while injecting internal tests. The debug instructions is presented in [54]. The automatic verification infrastructure is based on the Open SoC Debug Library and platform (Fig. 17) consists of a compilation environment Generic Logic Interfacing Project that gives a plug and play to compile and convert between verification files written communication and FIFO queue data exchange method. with Assembly/C language and simulation/memory/circuits Synthesis, physical design, and post-silicon tests are also implemented in Verilog. The automatic verification environ- run to complete the RISC-V processor design. ment covers functions by adding test modules with different IoT technology is continuing to grow, and edge comput- parameters instead of manually creating a test stimulus envi- ing and high-performance computing is emerging. RISC- ronment for individual tests on the circuit. Automatic verifi- V 64-bit processors can process large data sets with lots cation provides increased flexibility, ease of use, automatic of flexibility for embedded applications, so [52] explains a conversion between different formats of files, and only few design of a 64-bit high performance embedded processor changes in parameters to test a wide range. However, there that supports the B-extension. The B-extension is developed is a lack of directed tests and functional coverage. to reduce code size, improve performance, reduce power consumption, and realize the acceleration of bit manipula- tion instructions. The verification used for this processor 5.2 Formal Verification is dynamic simulation and FPGA prototype verification. RISC-V instruction self-checking test set and imperas-riscv This subsection covers the verification of various RISC tests are used to supplement riscv-tests to cover B-extension. processors for which formal verification methods were used FPGA prototyping is used to test the stability and correct- primarily. In classical formal verification techniques Binary ness of processor operation. Performance is also measured Decision Diagram (BDD), Binary Moment Diagram (BMD), by different metrics of Dhrystone, CoreMark, and Compre- Boolean Satisfiability (SAT), or Symbolic Computer Alge- hensive Analysis tests. bra (SCA) are used [55].
130 Journal of Electronic Testing (2025) 41:111–138
RTL and ISS Test Memory behave in the same way
read/write generate read/write
memory next instr. memo
RTL Data ISS Data Memory If. Memory If. next next RTL signal: ies ISS to to TLM RTL ! TLM interface insty, instr. interface RTL Instr. ISS Instr. Memory If. Memory If. rocess System ey execute next based instr. | access Simulatjé Core y signalsᴬ ISS data Test provide Result/ Controller Metrics access RTL Core data/ notify instr. completed
Fig. 16 Used Cross-Level testing of both RTL core and reference ISS in co-simulation setting. Source: Adapted from [53]
Fig. 17 Schematic diagram of the verification platform. Assembly Cc Source: Adapted from [54] Language Language File(.s) File(.c)
Compile
Environment
Circuit Verilog FPGA Chip Designᶠ Simulationⁱ 5 Hardware erification|
4 Springer
Journal of Electronic Testing (2025) 41:111–138 131
5.2.1 Property Checking and Theorem Proving and a cache memory interface (with TLB). The VAMP float- ing point unit supports addition/subtraction, multiplication/ An implementation of formal verification can be shown in division, comparison and type conversions. Verification is [56] based on CHERI-Flute. CHERI (Capability Hardware done on gate level using SRI's PVS theorem prover [59]. Enhanced RISC Instructions) is based on ISAs with capa- They developed a tool that automatically translates the PVS bilities that extend pointers with more data and instructions hardware specifications to Verilog HDL. The verified VAMP for altering data. Flute is the RISC-V processor used in this core is then implemented on a Xilinx FPGA. design environment that can be extended to support CHERI- The formal verification of a complete microprocessor RISC-V capabilities. The formal verification approach is [60], VAMP involves design and verification hierarchy. At imported on the JasperGold platform that integrates the the lower hierarchical level, theorem-prover PVS (Proto- design in SystemVerilog with assertions (SVA) and com- type Verification System), verified the VAMP on gate level pares it against the manually translated Sail CHERI-RISC-V which contains a Tomasulo scheduler with reorder buffer specifications. The steps of the verification flow include: an supporting multiple results, issuing into the reorder buffer, abstraction function mapping states across CHERI-Flute to and reordering of instructions in execution units. About 5% CHERI-RISC-V, instruction property checking for correct- of the overall proof effort was spent on this step. In the next ness, mapping specifications to properties, verification of step, modules of complete execution units (specification register-only/branching/memory CHERI instructions, check- functions) and uninterpreted functions as execution units ing for processor freezes in operation. To prove these prop- were verified at a higher abstraction level. More than 60% erties, proof engineering was used, which includes prov- of the proof effort was spent on the complex execution units. ing lemmas in a previous stage of the pipeline to confirm it Another 15% of verification effort went to the parameterized is correct in a later stage. A major obstacle in verification Tomasulo algorithm. The actual data management of the comes when there are unrepresentable capabilities in the pipeline is verified next without interrupts. Finally, inter- hardware, so CHERI-Flute is designed to prevent genera- rupts that are verified take 3% of the effort. tions of these capabilities. The end-to-end verification has The VAMPExplorer tool developed by [60], provides an successfully implemented unbounded proofs of properties intuitive interface to the specification, the implementation with single-instruction and sequence-dependent bug detec- and the verification of the VAMP. The VAMPExplorer visu- tion. Several bugs were successfully identified in most of alizes the general implementation and verification structure the CHERI instructions and bugs and features were distin- and improves accessibility to expert and non-expert users. guished. The focus of the research was on CHERI instruc- tions and not RISCV instructions in particular though. Another formal verification approach for a RISC-V pro- 5.2.2 Polynomial Formal cessor detects a different type of error called opcode trojans [57]. An opcode trojan is a modification in the processor Polynomial formal verification method [61] is used to triggered by opcodes (instructions to be performed) that can specify the space and time complexity of the order of O(nc) expose data, change data, or cause denial of service. Sev- to simplify the complexity of a CPU verification. Binary eral opcode instructions are defined in ISA, but any instruc- Decision Diagrams (BDD) used for verification are directed tions outside of this specification that affect the processor graphs with no cycles that have a minimum number of are labelled as trojans. For their detection, the trojan circuit nodes, where each node has two edges representing a 0 or 1. was embedded in the instruction decoder circuitry of the Some challenges that come with BDDs are the size of BDDs processor under test. Using the Z3 SMT solver to implement extending to greater than the polynomial and the need for property checking, reachable processor states are checked a golden reference model BDD that is hard to obtain. To for invalid instructions used to prove if opcode trojans exist mitigate the size challenge, a divide and conquer method or not. Any invalid opcode trojans were efficiently and suc- is applied in Fig. 18 to partially simulate the RISC-V RTL, cessfully identified in MIPS and RISC for 16 bits to 128 bit produce the instruction hardware, and run a symbolic simu- processors along with counter examples and error messages lation to obtain an output BDD (top path BDD). For the printed. This method efficiently worked for benchmark cir- reference model problem, a reference BDD model (bottom cuits with as many as 400,000 gates within 10–30 s. There path BDD) is generated piece by piece for each individual are several more trojans that can be explored and identified instruction. After equivalence checking the two BDDs, the through this formal verification method. polynomial formal verification is performed. Instructions VAMP (Verified Architecture Microprocessor) Proces- are grouped into logic, addition, subtraction, and shifting sor [58] is 32-bit RISC processor,a DLX processor variant to perform theoretical and simulation proofs to show the with a Tomasulo scheduler, precise and nested interrupts, a polynomial time complexities of each one. This verification 5-stage pipeline, a fully IEEE compliant floating point unit, method took less time (16 min) and utilized less memory too
132 Journal of Electronic Testing (2025) 41:111–138
Fig. 18 Proposed verification methodology overview for | Polynomial formal verification Verilog AIG |Reduced Sond method. Source: Adapted from 2 Symbolic Simulator AIG Simulation [61] Stimuli| | Partial
BDD
Function Reference BDD quivalence
for the 32-bit single-cycle RISC-V processor (RV32I) while security-critical properties were classified into 9 catego- addressing the challenges of BDDs very well. ries which focused on different security aspects of Aka- [55] successfully verified all functional units of the multi- ria NS31 A (licensed from NSITEXE, Inc.). NS31 A is a cycle, MicroRV32 processor completely with sequential 32-bit single issue RISCV compliant ISA with four stage sub-circuits. Using Polynomial Formal verification (PFV) pipeline processor. A negative aspect of this approach is gave an upper bound with respect to the time and space the need for extra black-boxing for some properties to suc- complexity for the given function for many subcircuits. The cessfully prove them within a 24 h time frame. Verification methodology is explained in detail in the paper SystemC is another verification language used to create and is summarized in Fig. 19. A pre-processing step was formal models with an existing model checker called SMV performed to generate the AIG of the processor and then (Symbolic Model Verification) for verification [63]. The to extract the functionalities, partial simulator was used. verification method used is based on the semantic transla- BDDs using SYMSIM tool were used to verify the extracted tion method that transforms sequential execution statements functionalities of the processor. Results for all four stages to the more hardware implementation counterpart. SystemC of MicroRV32 processor (Fetch, Control, Execute (ALU), processes and modules are translated to SMV modules for Decode and Extension unit (DEU)) are presented. The code semantic consistency, while following several translation base was extended to incorporate sequential elements (like rules including different data types, sensitive variables, latches and flip-flops) successfully and shown with the encapsulated functions, and classes. Assumptions and basic example of 2-bit left/right shift circuit with memory ele- statements are used for simplification. A successful SMV ment. The total verification time for the ALU was 200 ms. model for the SystemC design is built and evaluated with experiments to test the quality of the verification of SystemC 5.2.3 Model Checking Formal designs at different levels of abstraction. Assertions that express design specifications can be auto- Using model checking based formal verification with the ~~ matically generated from transaction level model (TLM) formal verification tool Jasper, security-critical function- simulation traces [64]. Assertions are first generated in the ality [62] of a commercial RISC-V processor is verified. ~~ form of frequent patterns of function calls in simulation Several design bugs were detected, which were confirmed traces. Real time parameters are also taken into account with by the design team of the processor. To ensure high secu- time constraints. TLMs can abstract different details of com- rity standards and compliance to the open source RISC-V munication in different modules, which improves simulation processor, validation can be done during pre-silicon and performance and verification efficiency. Symbolic execution post-silicon. For pre-silicon verification, a fully-automatic simulates different paths with symbolic inputs that get trig- approach for formal verification called Model Checking gered by the testbench to capture strange behaviors. This can be used. It uses a mathematical model of a system and technique helps improve accuracy. Episode mining that gen- systematically explains and explores all possible behav- erates assertions, reduces the number of assertions while iors of the system to target directly and exhaustively the including time annotations that represent performance con- security-critical functionality with properties, instead of straints. SystemC designs are then used to test if high-quality using Bounded Model Checking. In the paper [62], the assertions are generated correctly.
4 Springer
Journal of Electronic Testing (2025) 41:111–138 133
Spinal HDL [cas SBT Fetch 1 Verilos
Decode | AIG Verification!|
Verilog Variable
Order FUNC |
Extension | |
verilo9g Ai (Psi) || BDD BDD
| Check |
Execute | quivalence~quivalent/ |
Verilog | Not-Equivalent/ |
Ar
Control Sequential Simulation (SSIM)
yd
Init FE DE EX WB
Check Control Signal
Signals Juivalence Libr:ary
Equivalent/
Not-Equivalent/
Abort
Fig. 19 The Verification methodology. Source: Adapted from [55]
5.3 Combination of Formal and Functional be compared with a Spike golden reference model. The sec-
ond approach uses a formal verification methodology with
This subsection describes the use of both formal as well as Yosys [66] to compare between an IP with formal properties,
functional verification methods to verify a RISC processor. for the internal states of the processor, to an ISA specifica-
tion. Both approaches aim to cover as many states as pos-
5.3.1 Simulation and Formal Property Checking sible with μGP generating the largest coverage metrics and
the formal verification Yosys framework covering assump-
Simulation and formal verification can be combined to verify ~~ tions/assertions. Certain flaws were added to the processor a 32-bit ISA RISC-V processor [65]. To verify against ISA, to see if these could be detected by either approach. ALU a verification plan combining two functional approaches is ~~ misbehavior were detected by both, faulty comparisons were used. The first approach uses a genetic algorithm from a μGP detected through formal verification, data hazards detected generator that generates high coverage RISC-V programs to by μGP torture tests, and interrupt execution was detected
4 springer
134 Journal of Electronic Testing (2025) 41:111–138
by the μGP simulations as well. Combining both simulation The single-issue in-order (SIIO) 32-bit, 5 stage RISC-V and formal verification is beneficial to cover different types ~~ ISA based processor with a 2-bit saturating counter branch of error detection. However, they are costly as μGP needs predictor is implemented in Chisel HDL, [67]. Correct- a simulation environment, RAM, and software adaptations, ness is shown through assumptions and assertions (formal and formal verification needs the RISC-V Formal Interface properties). Formal verification is performed with riscv- (RVFI) and hardware adaptations. Run time for μGP is 90 formal using SystemVerilog/Verilog to check instructions min for 450 individuals and for formal verification is 45 min ~~ one by one. Spike ISA golden reference comparison is for 51 tests. made along with coverage metrics. To increase cover- Typically testbenches are custom built, which is time con- age, an algorithm to generate programs through mutation suming and costly due to additions and changes in design to and crossover called μGP is used (Fig. 21). The results of detect any bugs [67]. Handmade testbenches can be replaced this proposed verification methodology when compared with constrained-random instruction generators that increase to widely used RISC-V torture unit tests achieved fewer bug detection and coverage and use cloud-based frameworks instructions, higher coverage, earlier/better detection to accelerate the process. The later the bug is detected in the of hard-to-detect bugs, and cheaper method without the design cycle, the more costly detecting bugs becomes, but time-consuming human made testbenches. This approach, having a completely exhaustive testbench is also not feasible. ~~ however, does require high effort for complex designs in The new formal verification methodology to address these ~~ formal and functional verification methods. concerns contains a three step pre-silicon ISA verification stage (Fig. 20) to detect bugs as early as possible.
Fig. 20 Overview of the pro-
posed verification methodology. A . Chisel HDL blocks design
Source: Adapted from [67] £ « Assertions and Assumptions
5 2 I~ | «Single instruction ref. model in
SE
@ | HGP |
Framework * Evolutionary algorithm - max coverage
Fig. 21 Coverage driven frame-
work overview. Assembly test
program (individual) creations,
assembler, and linker. Parallel
execution in the processor under
verification (PUV) and Spike,
the golden RISC-V ISA simula-
tor. Coverage extraction and
fitness function to direct μGP.
Source: Adapted from [67] AJ] fA]
EEENEEEE
4 Springer
Journal of Electronic Testing (2025) 41:111–138 135
5.3.2 Fault Tolerance and Error Detection random test generation and directed tests to generate diverse sequences and specific corner cases to exercise critical parts [18] talks about RISC-V implementation with integrated of a processor design. In the case of the registers only being fault tolerance and error detection mechanisms. Fault detec- able to be accessed internally, the verification environment tion mechanisms in CPU architectures include watchdog needs to be able to exercise the register file adequately to timers, performance monitoring (profiling), trace and debug check for functionality so assertions can be added to check support units. for proper register file operation and consistency throughout Software-Based Self-Test (SBST) finds permanent faults the verification process. at-speed in-ifield testing of processors, which prevents over- When looking at the best formal method, formal verifi- testing of manufactured chips. Self-Test libraries (STLs) or cation methodology on a 32-bit 5-stage RISCV ISA based SBST programs need to be manually developed by using processor implemented in Chisel HDL [67] with three step the existent formal specifications of the RISCV ISA. STLs pre-silicon ISA verification stage to detect bugs as early improve the quality assurance of complex SOCs. Typical as possible is chosen. This framework has code coverage, testing times for SLT range from 15 min to upto 2 h. There bug detection, and extensibility to other processors, while is ongoing research on methods to automatically generate being low cost and having no time-consuming, man-made the SLT programs. testbenches. The downside of this is that it is a high effort Another safety critical, Burn-In test (BI) [18] requires for complex designs in formal form, so incorporating some functional stress-inducing stimuli, which can be optimized functional verification methods can help in that. due to incremental ISA-structure of RISC-V. Strategies like SAT-solvers, evolutionary algorithms etc. can be used to identify the sub-set of instructions needed for an efficient 6 Conclusion stress program for the DUT. In conclusion, the formal speci- fications of RISC-V provide a direct transition to functional RISC-V processors are open-source CPUs, and features can test generation. be configured on them according to application require- The PULP project implements hybrid modular redun- ments. The limitations of proper verification strategies is dancy as fault injection (FI) experiment with lockstep execu- currently a work under progress. There have been several tion to flexibly integrate fault tolerance and error detection major RISC-V processors in the market since 2011 [69], mechanisms in its RISC-V cluster based project. when the RISC32I base integer set, RISC-V ISA was Testing with Random Instruction Generation (TestRIG), released. In this paper, we explained the struggles of verify- [68], developed by researchers at University of Cambridge, ing RISC-V, various available DV approaches and imple- can be used for exhaustively testing faulty instructions in the mentation of these approaches on various RISC-V proces- pipeline of the CHERI processor. TestRIG used QuickCheck sors. Selected verification methods are highlighted with the VEngine to communicate over RVFI and DII sockets and processor used, type of verification technique used, as well detected problems with micro-architectural mistakes (regis- as advantages and disadvantages. ter forwarding and flushing the pipeline); memory mistakes Although there is no set standard, there are many different (discover cache bugs and memory speculations) and unex- levels of RISC-V processor verification that increase in com- pected interactions. plexity and coverage. It starts with a simple “Hello World” that implements the RTL and written ISA spec, a simple 5.3.3 Best Approaches check that runs RTL DUT in testbench, trace-compare to use a random generator for tests and compares log files, Out of the various approaches discussed above, the best data-path lockstep-compare where a reference model and functional and formal implementation have been chosen DUT are run together for comparison, and an asynchronous based on the metrics. For the best functional method, block lockstep that adds asynchronous events to the previous level and chip level functional verification on a RISCV 32I based of DV [28, 70] processor [46] called Siwa with SystemVerilog and UVM From finding non-trivial bugs [48] in a 32—bit RISC succeeds as it has code coverage, functional coverage, and is V based processor using cloud-based frameworks with the extensible to other processors. It is a concise implementation application of constrained-random instruction generators, that is cost efficient with the benefits of using a standardized formal verification was performed on CHERI RISC-V- Flute method with UVM. The only limitations are that programs with use of Proof Engineering and JasperGold. Sometimes may not be completely random, and registers may only be a simple comparison-based trace analysis will be suffi- internally accessed. cient to confirm a level of basic operation of the processor To address these limitations, the proposed verifica- [29]. Formal Verification methods make sure the proces- tion method can be improved by including more pseudo sor works correctly for all processor states, while functional
136 Journal of Electronic Testing (2025) 41:111–138
verification and simulation-based methods give full func- Computing Machinery, New York, NY, USA, pp.12–20. https:// tional coverage and full code coverage. doi.org/10.1145/3457388.3458657 The work discussed above either focuses only on one ISA: 2. Waterman A, Lee Y, Patterson DA, Asanović K (2011) The RISC- 3 stage ARM processor with RV32IM [13], generic RISC- V Instruction Set Manual, Volume I: Base User-Level ISA. Tech- nical Report UCB/EECS-2011–62, EECS Department, University V ISA [33, 49, 54, 61, 65, 67], target particular ISA: Siwa of California, Berkeley, May 13ᵗʰ [46], A-core [50], MINRES The Good Folk (TGF) Series 3. RISC-V Int. [Online]. Available: https://riscv.org/. Accessed 15ᵗʰ [53], CHERI RISC-V [56], preDAC [51], VAMP [61] or 4. Mar 2025 certain ISA features: B-extension [52] There are few stud- RISC-V Landscape. [Online]. Available: https://riscv.landscape2. io/?view-mode=grid. Accessed 5th Mar 2025 ies that compare recent ISA such as Intel Haswell (OoO), 5. Alexander D, Albers M, Kleinbeck B, Guan Y, Michalik H, Klink Intel Atom (InO), ARM Cortex A15 (OoO), ARM Cortex R, Blochwitz C, Nechi A, and Berekovic M. (2021). A compara- A8 (InO), Alpha 21264 (OoO) and Alpha 21164 (InO) tive survey of open-source application-class RISC-V processor [15], Flute and Sail CHERI-RISC-V specification [56], implementations. In Proceedings of the 18th ACM International Conference on Computing Frontiers (CF '21). Association for MIPS (16, 32, 64, and 128 bits) and RISC-V (32, 64, and Computing Machinery, New York, NY, USA, pp. 12–20. https:// 128 bits) architecture benchmarks [57]. Several techniques doi.org/10.1145/3457388.3458657 of verification are compared and discussed in [43] too. 6. Shaik AI (n.d.) A major change could come to Android phones in the coming years,” news article in SAMMOBILE, published on Nov 3ʳᵈ, 2023. [Online]. Available: https://www.sammobile.com/ 6.1 Future Work news/android-phones-risc-v-processors-coming-years/. Accessed6th Mar 2025 In this paper we have not covered vulnerability analysis 7. Hughes M (n.d.) Android 10 ported to homegrown multi-core RISC-V system-on- chip by Alibaba biz, source code released. like clock glitching nor non-functional properties like tem- Article in The Register, published on Jan 21ˢᵗ, 2021. [Online]. perature or power consumption of RISC-V processors. The Available: https://www.theregister.com/2021/01/21/android_ field of RISC-V research is growing and new methods or riscv_port/. Accessed 7th Mar 2025 improvements are continuously happening. 8. The world's first RISC-V phone might be just around the corner. [Online]. Available: https://tuxphones.com/sipeed-rv64-first-risc- v-rv64-phone-linux-2022-2023/. Accessed 6th Mar 2025 9. Gibbond A (n.d.) A RISC-V Future? SiFive and Andes Aim to Funding No funds, grants, or other support was received. Shake Up the Processor Industry,” news article in All About Cir- cuits, published on Jun 25ᵗʰ, 2021. [Online]. Available: https:// Declarations www.allaboutcircuits.com/news/a-risc-v-future-sifive-and-andes- aim-to-shake-up-the-processor-industry/. Accessed 1st Mar 2025 Competing interests All authors certify that they have no affiliations 10. Aleksandar K (n.d.) NVIDIA Shipped One Billion RISC-V Cores with or involvement in any organization or entity with any financial This year inside its Accelerators, up to 40 cores per chip. Arti- interest or non-financial interest in the subject matter or materials dis- cle in TECHPOWERUP, published on Oct 23ʳᵈ, 2024. [Online]. cussed in this manuscript. Available: https://www.techpowerup.com/328026/nvidia-ships- over-one-billion-risc-v-cores-this-year-inside-its-accelerators-up- Financial interest The authors have no relevant financial or non-finan- to-40-cores-per-chip. Accessed 6th Mar 2025 cial interests to disclose. 11. Pulpino, developed by ETH Zurich. [Online]. Available :https:// github.com/pulp-platform/pulpino. Accessed 24th Mar 2025 Open Access This article is licensed under a Creative Commons Attri- 12. Semiconductor Engineering. Verifying a RISC-V Processor. You- bution 4.0 International License, which permits use, sharing, adapta- Tube, (Oct 17ᵗʰ, 2023). [Online Video]. Available: https://youtu. tion, distribution and reproduction in any medium or format, as long be/Hg3O4Ti92gk?si=XvDMA3nwgZE8HK1I. Accessed 27th Dec as you give appropriate credit to the original author(s) and the source, 13. 2023 provide a link to the Creative Commons licence, and indicate if changes Zhang W, Zhang Y, Zhao K (2021) Design and Verification of were made. The images or other third party material in this article are Three-stage Pipeline CPU Based on RISC-V Architecture. Pro- included in the article’s Creative Commons licence, unless indicated ceedings of 2021 5th Asian Conference on Artificial Intelligence otherwise in a credit line to the material. If material is not included in 14. Technology, ACAIT 697–703 the article’s Creative Commons licence and your intended use is not Opiah A (2024) What is RISC-V and why is it important? Article permitted by statutory regulation or exceeds the permitted use, you will in edgeIR.com Industry review [Online]. Available: https://www. need to obtain permission directly from the copyright holder. To view a edgeir.com/what-is-risc-v-and-whyis-it-important-20240109. copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. 15. Accessed 1 Nov 2023 Akram A, Sawalha L (2019) A study of performance and power consumption differences among different ISAs 22nd euromicro conference on digital system design (DSD), Kallithea, Greece, References 16. pp 628-632. https://doi.org/10.1109/DSD.2019.00098 x86, ARM and RISC-V, how to choose the optimal architecture for your AI applications? [Online]. Available: https://www.dfrob
- Dörflinger A, Albers M, Kleinbeck B, Guan Y, Michalik H, ot.com/blog-13494.html. Accessed 12 Dec 2023 Klink R, Blochwitz C, Nechi A, Berekovic M (2021) A compara- 17. RISC-V verification: the 5 levels of simulation-based processor tive survey of open-source application-class RISC-V processor hardware DV. [Online]. Available: https://semiengineering.com/ implementations. In: Proceedings of the 18th ACM International risc-v-verification-the-5-levels-of-simulation-based-processor- Conference on Computing Frontiers (CF '21). Association for hardware-dv/. Accessed 13 Dec 2023
Journal of Electronic Testing (2025) 41:111–138 137
- Anders J, Andreu P, Becker B, Becker S, Cantoro R, Deligiannis 36. COREV-DV a library of extensions to the Google riscv-dv instruc- NI, Elhamawy N, Faller T, Hernandez C, Mentens N, Rizi MN, tion stream generator [Online]. Available: https://github.com/ Polian I, Sajadi A, Sauer M, Schwachhofer D, Reorda MS, Ste- openhwgroup/core-v-verif/blob/master/docs/VerifStrat/source/ fanov T, Tuzov I, Wagner S, Zidarič N (2023) A survey of recent corev_dv.rst. Accessed 20 Dec 2023 developments in testability, safety and security of risc-v proces- 37. Imperas releases new updates, test suites, and functional coverage sors. 2023 IEEE European Test Symposium (ETS), Venezia, Italy. library to support the rapid growth in RISC-V verification. Design 1-10. https://doi.org/10.1109/ETS56758.2023.10174099 and Reuse. [Online]. Available: https://www.design-reuse.com/
- RISC-V profiles [Online]. Available: https://github.com/riscv/ news/53178/imperas-risc-v-verification.html. Accessed 16 Dec riscv-profiles/blob/main/ profiles.adoc#profiles-versus-platf 2023 orms. Accessed 13 Dec 2023 38. riscvISACOV, systemVerilog functional coverage for RISC-V
- Kern C, Greenstreet MR (1999) Formal verification in hardware ISA. [Online]. Available: https://github.com/riscv-verification/ design: a survey. ACM Transactions on Design Automation of riscvISACOV. Accessed 20 Dec 2023 Electronic Systems 4(2):123–193 39. Riscv-V verification interface (RVVI) [Online]. Available: https://
- Gupta A (1992) Formal hardware verification methods: a sur- github.com/riscv-verification/RVVI. Accessed 20 Dec 2023 vey. Form Method Syst Des 1:151–238. https://doi.org/10.1007/ 40. RVVI-Trace RISC-V verification interface, [Online]. Available: BF00121125 https://github.com/riscv-verification/RVVI/tree/main/RVVI-
- Oleksiak A, Cieślak S, Marcinek K, Pleskacz WA (2019) Design TRACE. Accessed 20 Dec 2023 and verification environment for RISC-V Processor Cores. 2019 41. RVVI-API RISC-V verification interface, [Online]. Available: MIXDES - 26th International Conference “Mixed Design of https://github.com/riscv-verification/RVVI/blob/main/RVVI-API/ Integrated Circuits and Systems,” Rzeszow, Poland, 206–209. README.md. Accessed 20 Dec 2023 https://doi.org/10.23919/MIXDES.2019.8787108 42. The virtual verification peripherals used in the test bench - RVVI-
- Sivakumar PR (n.d.) System verilog testbench / verification VVP [Online]. Available: https://github.com/riscv-verification/ environment architecture. [Online]. Available: https://www. RVVI/blob/main/RVVI-VVP/README.md. Accessed 22 Dec maven-silicon.com/blog/systemverilog-testbench-verification- 2023 environment-architecture/. Accessed 14 Dec 2023 43. Ray S, Bhadra J, Abadir MS, Wang LC (2013) Guest editorial:
- Wolf C (n.d.) RISC-V formal verification framework. test and verification challenges for future microprocessors and [Online]. Available: https://github.com/cliffordwolf/riscv-for- SoC designs. J Electron Test 29:621–623. https://doi.org/10.1007/ mal. Accessed 15 Dec 2023 s10836-013-5411-y
- Moundanos D, Abraham JA, Hoskote YV (1998) Abstraction 44. Mezger BW, Santos DA, Dilillo L, Zeferino CA, Melo DR (2022) techniques for validation coverage analysis and test generation. A survey of the RISC-V architecture software support. IEEE IEEE Trans Comput 47(1):2–14. https://doi.org/10.1109/12. Access 10:51394–51411. https://doi.org/10.1109/ACCESS.2022. 656068 3174125.22
- Van Campenhout D, Al-Asaad H, Hayes JP, Mudge T, Brown 45. “Writing a RISC-V emulator in rust.” Available online: https:// R (1998) High-level design verification of microprocessors via book.rvemu.app/hardware-components/03-csrs.html. Accessed error modeling. ACM Trans Design Automation Electron Syst 27 Dec 2023 3(4):581–599. https://doi.org/10.1145/296333.296347 46. Molina-Robles R, Solera-Bolanos E, García-Ramírez R, Chacón-
- RISC-V International (n.d.) Tutorial Getting Started with RISC Rodríguez A, Arnaud A, Rimolo-Donadio R (2020) A compact V Verification. youtube, Mar 17th , 2021. [Online Video]. Avail- functional verification flow for a RISC-V 32I based core. 2020 able: https://youtu.be/G2IE7DM-tjE?si=0CkuTnpdqZpugph6. IEEE 3rd Conference on PhD Research in Microelectronics and Accessed 21st Nov 2023 Electronics in Latin America (PRIME-LA). San Jose, Costa Rica.
- DVCon (2022) Tutorial- 5 levels of RISC-V processor verifica- 1- 4. https://doi.org/10.1109/PRIME-LA47693.2020.9062717 tion with imperas, synopsys, youtube, 6th Nov 2024. [Online 47. SPI summary. RISC-V-Linux, from Western digital corporation, Video]. Available: https://www.youtube.com/watch?v=o_ [Online]. Available: https://github.com/westerndigitalcorporation/ DQvH9jIJU. Accessed 10 Nov 2023 RISC-V-Linux/blob/master/linux/Documentation/spi/spi-summa
- IEEE Standard for Universal Verification Methodology Lan- ry. Accessed 29 Dec 2023 guage Reference Manual, in IEEE Std 1800.2–2020 (Revision of 48. Sethulekshmi R, Jazir, Rahiman RA, Karthik R, Abdulla MS, IEEE Std 1800.2–2017) , vol., no., pp.1–458, Sept. 14ᵗʰ, 2020, Swathy SS (2016) Verification of a RISC processor IP Core using https://doi.org/10.1109/IEEESTD.2020.9195920. SystemVerilog. IEEE WiSPNET 2016, International Conference
- A complete, fully functional, configurable RISC-V simulator. on Wireless Communications, Signal Processing and Networking [Online]. Available: https://github.com/riscv-ovpsim. Accessed (WiSPNET), Chennai, India. 1490–1493. https://doi.org/10.1109/ 16 Dec 2023 WiSPNET.2016.7566385
- Imperas RISC-V riscvOVPsim reference simulator and archi- 49. Pandiaraj K, Kumar CP, Attar M, Naidu S, Hajipeera D (2023) tectural validation tests, [Online]. Available: https://github.com/ Five Stage Pipelined MIPS Processor Verification Coverage Mod- riscv-ovpsim/imperas-riscv-tests. Accessed 16 Dec 2023 ule Using UVM. 2023 9th International Conference on Advanced
- RISCV- torture tests pre 2018. [Online]. Available: https:// Computing and Communication Systems (ICACCS), Coimbatore, github.com/ucb-bar/riscv-torture. Accessed 16 Dec 2023 India. 1482–1485. https://doi.org/10.1109/ICACCS57279.2023.
- Automated assembly program generator [Online]. Available: 10112791 https://gitlab.com/shaktiproject/tools/aapg. Accessed 17 Dec 50. Korsman A, Hirvonen V, Simola O, Tarkka A, Kosunen M, 2023 Ryynänen J (2023) End-to-End Multi-Target Verification Envi-
- riscvOVPsimPlus, a complete, fully functional, configurable ronment for a RISC-V Microprocessor. 2023 19th International RISC-V simulator. [Online]. Available: https://github.com/riscv- Conference on Synthesis, Modeling, Analysis and Simulation admin/riscv-ovpsim. Accessed 16 Dec 2023 Methods and Applications to Circuit Design (SMACD), Funchal,
- Open Virtual Platforms - the source of FAst processor models & Portugal. 1–4. https://doi.org/10.1109/SMACD58065.2023.10192 platforms. [Online]. Available: https://www.ovpworld.org/riscv 249 OVPsimPlus/. Accessed 17 Dec 2023 51. Abella J, Bulla C, Cabo G, Cazorla FJ, Cristal A, Doblas M (2020) An Academic RISC-V Silicon Implementation Based on
138 Journal of Electronic Testing (2025) 41:111–138
Open-Source Components. 2020 XXXV Conference on Design 64. Liu L, Vasudevan S (2013) Automatic Generation of System
of Circuits and Integrated Systems (DCIS), Segovia, Spain. 1–6. Level Assertions from Transaction Level Models. J Electron Test
https://doi.org/10.1109/DCIS51330.2020.9268664 29:669–684. https://doi.org/10.1007/s10836-013-5403-y
- Meng Z, Zhang Y, Zhou J, Guo Z (2022) Design of 64-Bit High- 65. Duran C, Morales H, Rojas C, Ruospo A, Sanchez E, Roa E (2020) Performance Embedded Processor Supporting RISC-V B-Exten- Simulation and formal: the best of both domains for instruction set sion. 2022 IEEE 16th International Conference on Anti-coun- verification of RISC-V Based Processors. 2020 IEEE International terfeiting, Security, and Identification (ASID), Xiamen, China. Symposium on Circuits and Systems (ISCAS), Seville, Spain, 1-4. 28–32. https://doi.org/10.1109/ASID56930.2022.9995771 https://doi.org/10.1109/ISCAS45731.2020.9180589
- Herdt V, Große D, Jentzsch E, Drechsler R (2020) Efficient cross- 66. Wolf C (n.d.) Yosys open SYnthesis suite. [Online]. Available: level testing for processor verification: a RISC- V Case-Study. http://www.clifford.at/yosys/. Accessed 15 Jan 2024 2020 Forum for Specification and Design Languages (FDL), Kiel, 67. Rojas C, Morales H, Roa E (2021) A Low-Cost Bug Hunting Germany. 1-7. https://doi.org/10.1109/FDL50818.2020.9232941 Verification Methodology for RISC-V-Based Processors. 2021
- Qiu J, Ye F, Zhou H (2021) Automatic Verification Platform IEEE International Symposium on Circuits and Systems (ISCAS), Based on RISC-V Architecture Microprocessor. 2021 Interna- Daegu, Korea, 1-5. https://doi.org/10.1109/ISCAS51556.2021. tional Conference on Networking Systems of AI (INSAI), Shang- 9401510 hai, China 157–160, https://doi.org/10.1109/INSAI54028.2021. 68. Tovar B, Yee C, Ng R, Al-Asaad H, Patil S (2025) Survey of 00037 RISC-V pipelines and testers. 2025 IEEE 15th Annual Comput-
- Weingarten L, Datta K, Kole A, Drechsler R (2024) Complete ing and Communication Workshop and Conference (CCWC), Las and Efficient Verification for a RISC-V Processor Using Formal Vegas, NV, USA, 00885-00895. https://doi.org/10.1109/CCWC6 Verification. 2024 Design, Automation & Test in Europe Confer- 2904.2025.10903846 ence & Exhibition (DATE), Valencia, Spain, 1–6. https://doi.org/ 69. Chen T, Patterson DA (n.d.) RISC-V genealogy. Electrical 10.23919/DATE58400.2024.10546693 Engineering and Computer Sciences University of California at
- Gao D, Melham T (2021) End-to-End Formal Verification of Berkeley Technical Report No. UCB/EECS-2016–6, [Online]. a RISC-V Processor Extended with Capability Pointers. 2021 Available: http://www.eecs.berkeley.edu/Pubs/TechRpts/2016/ Formal Methods in Computer Aided Design (FMCAD), New EECS-2016-6.html. Accessed 24 Jan 2016 Haven, CT, USA 24–33. https://doi.org/10.34727/2021/isbn.978- 70. RISC-V International (2021) “Demo: brief introduction to the 3-85448-046-4_10 5 levels of RISC-V processor verification- Kevin McDermott,
- Mathure N, Srinivasan SK, Ponugoti KK, Malik A, Quanbeck S Imperas” Youtube. [Online Video]. Available: https://youtu.be/ (2020) A Formal Verification Approach for Detecting Opcode Nh9Ksftb1t4?si=_e0GX4HU8xTfrVuB. Accessed 5 Jan 2024 Trojans. 2020 27th IEEE International Conference on Electronics, Circuits and Systems (ICECS), Glasgow, UK, 1–4. https://doi.org/ Publisher's Note Springer Nature remains neutral with regard to 10.1109/ICECS49266.2020.9294803 jurisdictional claims in published maps and institutional affiliations.
- VAMP, research project, by institute for computer architecture and parallel computing. University of Saarland, Deutsch, [Online]. Available: https://www-wjp.cs.uni-saarland.de/forschung/proje kte/VAMP/index.php?lang=en. Accessed 7 Jan 2024
- PVS, a mechanized environment for formal specification and veri- Chloe Tain received her MS degree from the University of California at fication, [Online]. Available: https://pvs.csl.sri.com/. Accessed 7 Davis in Electrical and Computer Engineering. She worked as a Prod- Jan 2024 uct Engineering Intern and DRAM Applications Engineering Intern,
- Ayewah N, Kikkeri N, Seidel PM, Beyer S (2005) Challenges in and is currently a full-time Hardware Engineer. Her research and career the formal verification of complete state-of-the-art processors. interests are in memory/RISCV verification, digital/electronic system 2005 International Conference on Computer Design, San Jose, design, GPUs, and VLSI design/DSP. Contact: tainchloe8@gmail.com. CA, USA, 2005, pp 603–606. https://doi.org/10.1109/ICCD.2005. 37 Savita Patil is a PhD student in Electrical and Computer Engineering
- Weingarten L, Mahzoon A, Goli M, Drechsler R (2023) Poly- department of University of California, Davis. Her research interests nomial formal verification of a processor: a RISC-V Case Study. are verification of Processors, Testing and Error modelling. Contact: 2023 24th International Symposium on Quality Electronic Design sypatil@ucdavis.edu (ISQED), San Francisco, CA, USA, 1-7. https://doi.org/10.1109/ ISQED57927.2023.10129397 Hussain Al‑Asaad holds a PhD and is a Professor and Vice Chair for
- Chuah CS, Appold C, Leinmueller T (2023) Formal Verification Undergraduate Studies in Electrical and Computer Engineering Depart- of Security Properties on RISC-V Processors. 2023 21st ACM- ment of University of California, Davis. His research interests are com- IEEE International Symposium on Formal Methods and Models puter-aided design and testing of digital systems, and fault-tolerant for System Design (MEMOCODE), Hamburg, Germany, 159-168. computing and VLSI architectures. Contact: hsalasaad@ucdavis.edu https://doi.org/10.1145/3610579.3611085
- Gao Y, Li X (2013) A Semantics-based Translation Method for Automated Verification of SystemC TLM Designs. J Electron Test 29:685–695. https://doi.org/10.1007/s10836-013-5406-8