This blog was originally published on the Axiomise website. Read the original blog.
Who wants to have bug escapes? Nobody. Who wants to have bugs in the design? Nobody. Who wants to find bugs in the design? I do. Finding bugs is every verification engineer’s dream, in my case establishing bug absence is as well via mathematical proof.
Designers don’t want bugs in the design – they’re a nightmare for them.
Verification engineers love them – don’t we?
The question is how?
The answer is simple: deploying skilled engineers using a great methodology & tool chain and focussing on requirements – both architectural as well as
What are we doing about it?
At Axiomise we are enabling and empowering DV teams around the world on how to do this through our unique training, consulting, services and custom solutions for RISC-V. Last week, we launched the world’s first online & on-demand formal verification course Formal Verification 101, supported with videos, demos, labs and quizzes leading to a certification. The training covers all the three pillars of theorem proving, property checking and equivalence checking. The course is designed to keep accessibility in mind, all our video content comes with closed captions.
Having trained 200 engineers in the art of scalable & predictable formal verification face-to-face, we recognized that we needed to scale the training to a much bigger pool and offer it at a price that works for everyone.
Recently, in the annual RISC-V summit, as well as in a webinar held in March, we showcased our high-end methodology for RISC-V processor verification leveraging our in-house vendor-independent formalISA app.
However, what happens when there is no readymade proof kit to be rolled out just yet – how to find the bugs in a limited time, with limited resources (both human and computer) and ensure you can have a Happy Diwali not just on Diwali but every day.
I always talk about two approaches – one is a detective approach and another a lawyer’s one. Both these styles are complementary and very effective and can and should be used in tandem.
The detective’s approach
What happens when Sherlock Holmes walks into a crime scene? What happened, what else can happen, what if the criminal is just hanging around out there (more bugs and what you missed wasn’t the only one). Being good at forensics and decoding everything about the crime scene uses skills that very few good detectives have. Asking the right first few questions often opens invaluable leads. In the context of verification, this is exactly what needs to happen. Asking the right questions of the design, will open different paths to investigation. This doesn’t have to be only for post-silicon bugs, but also when we are looking to adopt a bug hunting approach upfront on a design. But bear in mind, that when this is being done upfront questions have to be asked for end-to-end requirements and behaviour which is when this approach needs to be done in tandem with the other style – the lawyer’s approach.
The lawyer’s approach
Lawyers are great at working out complex inter-dependencies in a case and its relationship with law. Of course, there is a famous joke on “how do you tell if a lawyer is lying?” and the answer given is “see if the lips are moving”. But I’m not talking about this approach to law. I’m suggesting we take the brighter side of a lawyer’s approach to solving the cases.
A good lawyer starts from fundamental rules, applies logical systematic reasoning to deduce more information and applying rules of consistency and law. In our context, the law becomes the fundamental architectural and microarchitectural rules of design. Now, whereas a law in any society is often documented very well, in our case the documentation may not be extensive, complete, and even consistent. But that should not deter us from taking whatever we have and apply it for verification and in due course refine this document itself – an invaluable contribution that a verification engineer can leave for a designer. This is not something which is a nice-to-have but is a must. I once heard a VP engineering tell me that we don’t sell documents, we sell chips. Yes, that may be right, if you’re not selling to a market that requires compliance with standards.
When liability enforces reliability
Nowadays with massive requirement of compliance needed for ISO26262, DO254, and DO333, establishing the link between what gets built, what got tested and how needs to be clearly made with the documentation. So, any work that a verification engineer does in this regard, is priceless. It does require meticulous discipline in requirements documenting, tracking and maintaining mapping with what gets validated & verified. Verification in the absence of good tracking is pointless, just as verification with 100% functional coverage and loads of missed bugs is pointless.
Creating good specifications
The challenge is that creating specifications in a vacuum is just not practical. Without trying to build a model it’s sometimes very difficult to describe what one is building in great detail which is what is expected from a good specification. Where’s specifying high-level requirements are easier and must be done whenever possible, RISC V is a classic example where the ISA defines what is architecturally allowed; in general, it’s difficult.
In the case of RISC-V, it is certainly possible to verify an implementation against the ISA without a having great detail of micro-architecture specification, in general, it is not possible for all the other domains.
Good specifications: Easier said than done
So, how do we ensure that a great specification is available for verification and other downstream requirements such as maintaining compliance with standards?
The secret lies in using formal methods – using formal properties such as SVA and PSL to describe precise requirements. And you know what, you can use these to evaluate your specification model for inconsistencies without a design implementation.
When you have an implementation, these become constraints on the input interface and checkers on the output interface of the driving logic. Both designers, as well as verification engineers, can and should work on developing this together. It’s important that there is diversity in specification development and specification validation to explore corner case holes.
When an implementation is ready, the verification engineer can take over complete ownership – verification, finding bugs, debug, establishing proofs of bug absence and ensuring everything is tracked and linked to requirements with coverage and bug trends indicators of when we are done. There is a method we deploy in practice for projects whereby we work with designers and verification resources to develop a specification that is clear and can be executed for verification. The exercise is not hard and must be done systematically in conjunction with deploying formal in an agile manner.
Deploying formal – the agile way
Using an agile flow, shown in Figure 1, designers can start deploying formal methods way before simulation has even started. It is a truism that UVM testbenches take an enormous time to bring up and stimulus is the weakest link with UVM. This is where complementing it with formal makes much better sense. By running the agile flow, designers can start catching bugs such as initialization issues, unreachable code, lint issues, and start collecting coverage, this is done in the AVOID phase. Designer’s do not introduce silly bugs, so verification engineers do not waste time catching these silly bugs. In the DETECT phase, we dive deeper exploring FSM related issues, deadlocks, livelocks, and X-propagation related issues. Reachability and initialization issues continue to be caught while coverage gets collected from the formal tool. The ERASE and the PROVE phases are particularly interesting as this where most of the bug scrubbing happens and proofs of bug absence get built relying heavily on specifications – taking the lawyer approach of systematic analysis as well as the detective approach to scrutinize the crime scene and find any bugs. The TAPEOUT phase is the one where we verify for IP integration that has been previously verified in the early phases looking for connectivity issues, CDC, register checking, clocks & resets and integration and performance bugs.
In this agile approach, bugs become a common goal and the designer and verification engineer both share the same dream – no bugs after sign-off and tape-out!
Figure 1. An Axiomise agile flow called ADEPT-FV
When it becomes a nightmare for a designer
When a systematic method described above is not followed with no clear planning and tracking in place and all is in the hands of a random seed then I bet hunting bugs remain a challenge and there is no definitive path to closure – not even coverage. Functional coverage certainly helps but at the end of the day it only provides a bunch of sample points to say something is and isn’t possible; it does not make any guarantees that bugs are absent or that you’ve checked all possible interesting patterns.
In a nutshell
If you use systematic documentation, planning and execution in an agile manner to close the loop iteratively between what gets specified, gets verified, and tracked back then you have a great process in place. If you now use the beauty of formal methods in specifying properties and then using these to formally verify the implementation, you have a chance to obtain formal proofs of bug absence and also, at the same time have the ability to hunt corner-case bugs and prove once and for all that bugs do not exist.
Where to go next?
Start your journey with formal methods, give us a call and we can help.
If you want to learn formal, go to https://elearn.axiomise.com. If you want a RISC-V formal verification solution, go to https://www.axiomise.com/riscv-formal-app/. If you want us to provide consulting & services, talk to us.
We also regularly podcast on formal verification and technology; you can subscribe to our channel on Youtube at: https://www.youtube.com/channel/UC8wHm-C2Xl0XC3-pxySLmnA