This Diwali take a pledge to root out all the darkness (bugs) from your design and shine the light of exhaustive proofs of bug absence – know that your design works first time and every time.

The question is how?

At Axiomise we are enabling and empowering DV teams around the world on how to do this through our unique training, proof kits and consulting & services. We talked about finding bugs in RISC V this year by applying our industry’s first vendor-neutral ISA formal proof kit. Come and talk to us, to see how we can help you.

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.

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.

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.

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.

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.

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.

In this 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!

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.

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 much more quickly and systematically allowing you to have a much better, happy Diwali, on the Diwali day and later on as well.

On this note, I better get back and join the festivities at home and leave you with best wishes for a Happy Diwali.