GapFree Processor Verification

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.

He classified logic bugs in a processor into two categories. Single instruction bugs occur when an instruction delivers the wrong results regardless of program context, the sequence of previously executed instructions. Multiple instruction bugs occur only when sequences of instructions execute in a specific order. For example, a pipeline hazard detection unit might have a bug that results in an instruction receiving the old value of a register before it has been updated by an earlier instruction. Single instruction bugs can be detected if a single property is written and formally proven for each instruction. For multiple instructions, it is difficult to imagine all possible program context and to manually specify all properties to be proven. This challenge was the spur for his research on automated property generation.

Keerthi walked the audience through a series of techniques leading up to the approach he used to verify the Infineon processor. He started by describing Quick Error Detection (QED), a post-silicon processor validation technique that instruments a software test with various transformations and checks. Each instruction sequence test is transformed to use different registers, and the results from the original and modified tests are compared. Any difference indicates a multiple instruction bug related to a specific sequence involving multiple registers. QED is effective at finding bugs with short error detection latency.

Symbolic Quick Error Detection (SQED) takes this general idea and moves it into pre-silicon verification using formal verification methods. The processor design is instrumented to split the register files into two halves, and formal analysis considers all possible QED tests up to a length “k” that could be run on both halves. Any disagreement (formal counterexample) indicates a multiple instruction bug. If no bugs are found, the formal engine can provide a bounded proof of correctness to depth “k” so bugs could still be missed. Thus, SQED is efficient for finding multiple instruction bugs but not for proving their absence. Obtaining full (unbounded) proofs requires the use of SQED with Symbolic initial states (S²QED).

Keerthi explained that S²QED formally considers the same test executing in parallel on two independent and identical instances of the processor. Assuming consistent register values and identical instruction sequences between the two instances, a formal engine can prove that the two register sets will be consistent at the end of each sequence. As with SQED, any counterexample found by formal analysis reveals a multiple instruction bug. Keerthi then posed the question of how to achieve complete processor verification (C-S²QED) so that single instructions are verified, and the user knows that the properties completely cover all processor behavior. This can be accomplished by generating an S²QED property for each instruction class plus a reset property, and applying a set of completeness checks.

Keerthi closed with an actual example of verifying a CPU using the C-S²QED approach. The design was a 32-bit Infineon RISC-V processor with integer instructions, implemented with a five-stage pipeline with in-order fetch and in-order commit. As a measure of complexity, the design contains 3472 state bits. It took about five engineer-days to set up and run the formal verification, plus an additional day for a new instruction extension. The formal runs found design bugs within 30 seconds of runtime. Once all bugs were found, an unbounded formal proof was obtained in only 18 minutes of runtime. Simulation would have taken many weeks or months and, of course, could never have proven the absence of bugs.

All the properties were automatically generated using an Infineon metamodeling framework. All formal analysis was performed with the OneSpin 360 DV-Certify solution, including the GapFreeVerification App to ensure that the set of generated properties was complete. Keerthi’s conclusion was that this highly automated formal technique for processor verification produced “very good improvement in verification productivity.” We’d like to thank him for joining Osmosis and for sharing this innovative use of OneSpin’s products. A video of his full presentation is available at https://onespin.com/resources/videos/osmosis-2019/keerthi-devarajegowda-infineon-technologies. We hope that you enjoy it as much as we did.