This summer, I got the opportunity to work as a Formal Verification Intern with Axiomise for six weeks. I’m a keen designer and love working in design and architecture. Although, I’ve not started my professional career yet, I have done most of my projects as a designer in my undergraduate and postgraduate studies.
Having said that, I was always curious to know – how do we test that the design works? How is verification done in the industry? I had a prior design experience in building a RISC-V core using TL-Verilog in a workshop organized by Kunal Ghosh and Steve Hoover. Extending my work, I implemented RISC-V designed during the workshop on FPGA which is described in more detail over here. But verification – God what would it be like? I was not sure how to best use the six-week time window to learn something from scratch and then apply it for verifying real processors.
When I spoke with Ashish before the internship, I told him “I’ve no background in verification, never mind formal verification, and six weeks is quite a tight deadline to achieve verification targets you’re giving me, but I’m up for the challenge!”
Face-to-face with formal verification
Before starting my Internship, I took the Formal Verification 101 designed and delivered by Dr Ashish Darbari, Founder and CEO of Axiomise.
I was not sure if an online course can be effective in delivering knowledge at a pace I can absorb. I was a little sceptic initially. I took a week to complete this course, and Ashish didn’t put any pressure on me to accelerate it.
The online training gave a great introduction to beginners such as myself about how formal verification works and a thorough understanding of why what, and how of formal?
Before I give you an outline of what I learned in this course, I’d recommend that all digital designers and verification engineers should use formal methods. It finds bugs and builds proofs of bug absence – something I don’t believe can be done without using formal.
The course covers the three pillars of Formal: Theorem Proving, Property Checking, and Equivalence Checking. Some of the highlights of this course are described here in case someone finds it useful.
Mathematics in action: I got to see how proofs can be built interactively using a theorem prover, where we are able to visualize the entire proof. By using HOL 4 – an open-source theorem prover, I was able to see mathematics in action, specifying designs and verifying them through proofs.
Model checking: How can we write System Verilog assertions and use them to perform exhaustive and unbounded proofs? Some of the reasons for using SVA are:
- Improve the design observability: Using assertions, we can focus our checks anywhere in the design which in turn helps in data path analysis.
- Improve the debugging capability: Assertions are capable of finding bugs faster hence reduces the debug time.
- Improve the design documentation: Assertions are just simple statements that will state and verify the design behaviour.
ABC of Formal: Abstraction, Bug Hunting & absence, and Coverage: This module provided a great overview of how SVA-based formal verification can leverage abstraction, and coverage to enhance bug hunting and building proofs of bug absence. I was fascinated by the fact that with formal we can actually build proofs that bugs don’t exist! The interactive quiz used in this module kept me focussed and provided me opportunities to check my understanding.
Coverage: Finding bugs is one thing, establishing proofs of bug absence is another great reason for using formal, but how do we know we have not missed a bug? How do we know we are complete? This is where coverage comes in. The coverage module describes a flow that I used later in my practical work to expose blind spots in formal verification such as over-constraints and finding incomplete checkers.
RISC-V Formal Verification: Towards the end, the course takes a deep-dive into how formal verification can be done on RISC-V processors, focusing on methodology and coverage. I was able to see how cv32e40p and other RISC-V cores were verified using the automated formal app formalISA® from Axiomise. I was feeling excited to start my own work on WARPV processor verification, but I’ll be honest, I was also nervous if I could deliver in the time that I had.
WARPV formal verification using formalISA®
Using the skills and knowledge gained from the training, my task was to verify WARP-V 6-stage pipelined core written in TL-Verilog using formalISA app.
Along with this, I was also able to verify 2-stage and 4-stage pipelined versions of WARP-V core. As WARP-V core is highly parameterizable, we could get the design module easily using WARP-V Configurator. On the other side, although I had inherited a significant code base of formalISA® app, in no time, I was able to understand and modify the code to align with the requirements needed for WARP-V i.e., to work for different pipeline stages.
First, I did the verification of RV32I which is the base integer instruction set – 32 bit for all cores and found several new bugs. WARPV has no implementation of compressed instructions. Initially, both Ashish and I were surprised as these cores have been formally verified before using the riscv-formal testbench. We were not expecting to see any bug, after all I just learnt in the course that formal verification provides guarantees of bug absence!
For many of these violations were that the designer’s interpretation of the RISC-V specification was incorrect – the designer assumed that the program counter always remained byte aligned. We arranged meetings with the designer so we could confirm that these issues are legitimate design issues. Steve Hoover, the designer of the WARPV core said that at the time of the design he was not sure about certain choices and he went ahead with whatever would make the riscv-formal testbench happy. Effectively, the riscv-formal testbench also has the same bugs as the WARPV core. A detailed account of all the bugs we have found so far is available at Github.
Ashish asked me if I wanted to build the property set for the M-extension. I wanted to certainly give it a try. I successfully implemented the properties and to our surprise again found new bugs in the core. We again contacted the designer and learnt that they never exhaustively verified the M-extension with riscv-formal before although they had used some directed tests to check that the M-extension instructions worked correctly. I could also perform exhaustive proofs for the areas where the core was working correctly.
Six weeks of non-stop fun and learning
Talking about my learning experience in this internship, it was easy for me to grab the flow of how formalISA® works as I have a designer background. As the tool flow was automatic, I had to provide the design files and a setup file that would map the testbench signals to appropriate design signals. And believe me, writing assertions is as easy as writing the test case in a plain English statement.
For the first time, I tried concept of pair programming with Ashish, and it helped me a lot to accelerate my learning curve. For those who don’t know what pair programming is, it is an agile software development technique in which two programmers work together. One, the driver writes the code and the other, the observer reviews each line of code as it is typed in. This helps in reducing mistakes and bugs.
Apart from this, I also learned about RISC-V architecture and micro-architecture concepts in more detail. Using formal, gave me an opportunity to see up close how processors are built? how the micro-architecture optimizations are done for pipelined processors to avoid hazards such as forwarding, stalling, and the Load Store architecture. Specific to RISC-V ISA, I got to know more about how ‘I’ and ‘M’ extensions of RISC-V ISA are built. How to handle exceptions, and when to raise a trap/exception signal according to the RISC-V ISA definition.
Designer’s perspective on formal methods
At last, I would like to pen down a designer’s perspective on formal. Adopt formal instead of simulation as dynamic simulation is a random approach where we can only provide a bounded test case. On the other side, formal verification is a systematic approach in which we can use assertions to perform exhaustive and unbounded proof. I would strongly recommend to at least all VLSI engineers to know what formal is, as it provides value to designers and architects along with verification engineers.
Acknowledgement
I would like to thank Dr Ashish Darbari for providing me a great opportunity. It was a great time working with him and learning formal verification from a practicing expert!!