Nowadays it is quite common that Cyber-Physical Systems (CPS) comprise processor sub-systems for executing domain-specific software applications. Designing processors is a hard task having high complexity, time-consuming development cycles, high costs and economic risks. Therefore, in hardware design (Application Specific Integrated Circuits, Field-Programmable Gate Arrays - “FPGA”, Systems-On-Chip FPGA), processors with surrounding peripherals (e.g., caches) and integration test suits are rather bought than developed in-house.

The recent developments in royalty free and open-source instruction set architectures (ISA) have motivated the development of various RISC-V designs, which range from freely licensed open-source cores to proprietary designs.

Off-the-shelf CPU designs may include test suites as well. However, if the designs are quite new, the question of trust in the promised quality of verification completeness and correctness remains. Cost-free cores might unluckily come without proper verification. Next to rigorous verification techniques and tools for processor designs comes the ability to adapt the verification to new situations such as the evolution of the RISC-V ISA.

In safety-critical applications, proven-in use processor cores are the natural candidates with the drawback of included license costs. Core designs based on a relatively new ISA (RISC-V) demand proper verification to be applicable in commercial solutions and have thus not reached the point when proven-in-use may be used as an argument.

One major challenge for CPU verification concerns ISA compliance. First, a reference model is needed and second, since all combinations of instructions cannot be verified in reasonable time using simulation-based verification, trade-offs must be made. Next to ensuring that software written for a specific ISA (RISC-V ISA selection) works correctly for a given CPU design, is to verify the CPU design itself with all design components and peripherals related to memory, load/store, paging, caching, pipelining, etc.

Additional challenges for CPU verification at module-level are:

• Verification effort (time) is very high compared to design efforts
• It's not decidable if different CPU architectures will behave similar in system context.
• It's expensive and there's still a lot of effort (different abstraction of models, interfaces) to go to system-level verification.

There are two main approaches to face the verification of a CPU, these are simulation-based verification and formal verification. The first is the most frequently used method, it can provide certain confidence that common functionality as well as corner cases were exercised, often measured using coverage metrics like functional coverage and structural/code coverage. Among the benefits of simulation-based verification are its high execution speed and the capability to re-use models from simulation for software verification and virtual prototyping. However, an extensive test suite must be manually written, which is a time-consuming task and more importantly, it is not complete and therefore cannot prove full compliance to a certain specification [CPU4]. On the other hand, formal verification can prove that a set of properties and assertions holds for all possible scenarios using formal engines based on mathematical techniques, e.g., property checking (also called model checking), which is of vital importance for safety-critical requirements. The drawback of formal verification is that, depending on the formal engine, it may not be able to provide proofs for large designs, but modern tools claim to be able to process a CPU design (e.g., [CPU6]). In the case of RISC-V, the ISA specifications must be translated into properties or assertions in the language that the formal verification tool uses, e.g., SystemVerilog Assertions.

CPU design verification includes verification planning (define what and how should be verified), definition/development of Instruction Set Simulator (ISS) for CPU, ISA selection plus custom instructions, simulation-based verification, i.e., Constrained Random Verification with self-checking capabilities (monitors and checkers) using Universal Verification Methodology (UVM), functional coverage collection and structural coverage measurement, and application of formal techniques to prove properties of the design.

An approach for the needed main ingredients for a CPU (RISC-V) verification flow is presented in [CPU1].

For CPU verification several approaches have been subject to research and development, such as the following examples regarding RISC-V:

• Formal verification, e.g., the RISC-V ISA Formal Proof Kit by axiomise [CPU2], riscv-formal [CPU7], OneSpin 360 DV RISC-V Verification App [CPU8]
• RISC-V verification on the RTL level [CPU3]
• Model-based test generation with the Scala-based Torture Test framework for RISC-V [CPU9]