Complete Formal Verification of RISC-V Processor IPs
for Trojan-Free Trusted ICs
Electronic systems are at the core of an ever-increasing number of products and services. From power plants to automobiles, from medical devices to airplanes, from smartphones to home appliances, complex electronic systems enable an unprecedented level of automation, performance, safety, and security. Integrated circuits (ICs) are the backbone of these systems. It is of paramount importance that they can be trusted to operate in full compliance to their specifications and certifications. However, IC design, production, and distribution are surprisingly vulnerable to malicious agents that could infiltrate devices with poor performance and reliability, or even with hardware Trojans, i.e., additional, hidden functionalities designed for nefarious purposes.
OneSpin Solutions is at the forefront of the effort to develop solutions that measure and ensure hardware trustworthiness.
Download our paper that was delivered at the 2019 Government Microcircuit Applications & Critical Technology (GOMACTech) conference.
Complete Formal Verification of RISC V Processor IPs for Trojan-Free Trusted ICs
Abstract—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 formalized 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.