Tom Anderson, OneSpin Solutions
Applying formal verification to thoroughly verify a RISC-V processor design.
Not so long ago, many semiconductor and system suppliers developed their own processors, often with unique features geared toward specific target applications. Although this innovation has continued for specialty processors such as digital signal-processing (DSP) engines and graphics processing units (GPUs), central processing units (CPUs) largely turned into a two-contestant race between x86 and ARM designs. More recently, there has been increased interest in the design and verification of highly customized processors. This is partly due to the open nature and flexibility of the RISC-V standard, and partly to the demands placed on processors by artificial intelligence (AI), the Internet of Things (IoT), and other advanced applications.
At OneSpin’s recent Osmosis users’ group meeting in Munich, one of our expert users presented a fascinating talk on applying formal verification to thoroughly verify a RISC-V processor design. Keerthi Devarajegowda is a researcher at Infineon Technologies who is pursuing his Ph.D. at TU Kaiserslautern, Germany. He developed his talk on “GapFree Processor Verification by S²QED and Property Generation” with several colleagues from Infineon and TU Kaiserslautern. He acknowledged PhD student Mohammad R. Fadiheh as one of the key contributors of this approach. Keerthi began by discussing processor verification using simulation, which allows bugs to escape to silicon, and formal verification, which traditionally requires a high level of manual effort and formal expertise. His primary research interest is automation of property generation for pre-silicon verification, making formal easier to use and more effective.