Verifying RISC-V SoCs
By: Rob van Blommestein
SoC developers give little thought to re-verifying a licensed core, trusting the vendor to perform thorough verification of functional correctness, and other aspects of integrity.
Each instruction in the RISC-V ISA is captured in a single Operational Assertion. These assertions capture the high-level operational view, and map to sequential or pipelined implementation, out-of-order execution and other possible options in the RTL core. A solution like the RISC-V Verification App from OneSpin includes privileged ISA, Control and Status Registers (CSRs), an exception mechanism and other extensions. Its verification framework splits the specification side from mapping to implementation, to enable full SVA re-use. Regardless of the approach used, it should be flexible enough to ensure that nothing is broken if custom extensions are added, and powerful enough to verify the new functionality.
[...]
RISC-V has great potential in the industry, but it must meet significant verification challenges to succeed against entrenched processor competition. This means verifying functional correctness, ensuring proper operation in safetycritical applications, checking that designs are secure and trusted, free of unintentional or deliberate vulnerabilities, and establishing proof of compliance to the ISA. SoC teams evaluating RISC-V cores should demand that their providers run complete integrity verification and document the results. This process must include automated code inspection, RISC-V verification and any other applicable formal method to prove functional correctness. Verification of safety, security and trust must also be performed when the requirements of the end application demand it. SoC teams should be able to re-run all these verification steps themselves as part of their acceptance criteria for RISC-V cores.
