Learn about a method for securing RISC-V IP that uses Operational SVA to formalize the RISC-V ISA. This paper says the resulting set of assertions is free from gaps and inconsistencies.
RISC-V processor IPs are increasingly being integrated into system-on-chip designs for a variety of applications. However, there is still a lack of dedicated functional verification solutions supporting high-integrity, trusted integrated circuits. This paper examines an efficient, novel, formal-based RISC-V processor verification methodology. The RISC-V ISA is formalised in a set of Operational SystemVerilog assertions. Each assertion is formally verified against the processor’s RTL model. Crucially, the set of assertions is then mathematically proven to be complete and free from gaps, thus ensuring that all possible RTL behaviors have been examined. This systematic verification process detects both deliberate hardware Trojans and genuine functional errors present in the RTL code. The solution is demonstrated on an open-source RISC-V implementation using a commercially available formal tool, and is arguably a significant improvement to previously published RISC-V ISA verification approaches, advancing hardware assurance and trust of RISC-V based designs.