Doc Formal answers 11 key questions

Ashish Darbari is CEO of formal verification consultancy and training provider Axiomise.

During DVCon USA I was able to meet with numerous colleagues from industry and academia. I presented a new research paper and helped to present a Synopsys-sponsored tutorial. Whether presenting or not, events like these can and should be like multi-day Q&A sessions. What I’ve tried to capture here are some of the most important questions I faced during the conference, together with how we at Axiomise set about answering them.

1. What is the biggest design that can be verified with formal?

I get asked this a lot. So, here is an indication of how big we can go with formal. We recently worked on a design as big as 338 million flops with 1.1 billion gates. And we found bugs in seconds.

2. That can’t be true. Either the design was very simple, or you must have done some cut-points and boxing?

No, we didn’t do any of these things. We compiled the whole design at once and deployed Axiomise proof accelerators. We got these checkers to fail or prove whatever the case may be. The key to scalability is methodology.

3. So, can we verify any one billion-gate design?

No, not necessarily. It depends on what you’re trying to verify. Verifying designs with tens of millions of flops is normal for us though.

4. So, what was this design?

I can’t say too much, but it was deeply sequential. It was the kind of design you might see in sectors like AI and machine learning, networking, and pipelined processors.

5. So how can we improve the way our team uses formal techniques? For years, we’ve believed formal was only suited to app-based work such as connectivity, register checking and so on.

Formal is great for functional, safety and security verification. At Axiomise we don’t view these as completely different problem targets. We see them as verification problems that must be addressed through a common flow using a combination of property checking and equivalence checking, and leveraging a range of techniques based in abstraction and problem reduction.

These techniques are important but it is useful to know that there is a blueprint for a flow that can be used in much the same way as the standard operating procedures seen in other engineering disciplines. This blueprint can be deployed in a sequential and parallel manner. We talked about it recently in an article describing our ADEPT FV flow.

A packed house at DVCon with plenty of questions about formal verification.

6. When we have previously used formal verification, we have turned to specialist services companies. They were great at what they did, but once they were finished and gone, we didn’t hold on to formal techniques that we could repeat ourselves. How do we get past that?

That’s something I’ve heard before. The Axiomise business model is built around enabling customers in their backyards, teaching them skills that will remain with them forever. And if you want more help toward understanding how far you can exploit those skills, Axiomise will guide you along with way.

We don’t want to replace your engineers with ours. That won’t help your teams use formal techniques more widely and more effectively in the longer term. If you just do that then formal will remain something located in the hands of a few experts in a given organization.

We want to fully democratize formal so that it can be used by everyone. We want to get us beyond the constraints on adoption set by automated app-driven techniques, to a point where we can collectively build safer, more secure systems that are guaranteed to work as expected because they are based on a deeper and much broader understanding of formal.

Services have a place. They help you solve problems when you’re short of time and need to bring in highly experienced experts. But the downside is that the expertise remains with those experts.

7. What tools would you recommend?

All the major commercial tools are as good as each other. What you do with them makes the difference. In 2019, the methodology is going to be the game changer, rather than specific tools.

8. We saw that you are now giving a talk on ‘Smart formal for scalable verification’. What are its main themes?

One aspect of the talk is that it takes a very hard problem that’s representative of a range of other problem signatures and looks at how to solve it. Another perspective it takes looks at various similar types of challenge from the point-of-view of computing resources, development effort, run times and so on – effectively, it’s describing what considerations you need to address to deploy formal from a cost point of view.

We show how a variable packet 16-flop design verification technique can be used to verify a 24K flop packet-based design on a tablet computer with 6GB memory and two CPU cores. When not limited to a laptop, the same strategy can be used to verify designs with 141K flops. Strategies such as these can be used to scale up to designs with one billion gates.

A big takeaway underlines, again, that verification is about risk management. It is not always about solving one problem but about scalability in general, making sure managers understand what it takes to solve a wide range of problems, and taking a cost-benefit view of verification.

9. How do you help a company improve and extend its use of formal techniques?

Axiomise can help in many ways.

First, we can come in and show you how to solve verification problems yourself through training. Our training is unique in the industry as we teach you what works in practice – some of our modules are directly usable in your project work, and you’ll also learn how to solve not one particular problem in a lab but how to take the lessons from that problem to other problems.

After the training, we offer a program to help your team to transition training to project work so that you speed up your day-to-day adoption of formal. Many of our trainees don’t need this, but others find it extremely valuable.

And finally, if you do need services, we offer that option.

We want to train people who will use formal to solve complex problems. We don’t just to want to teach people who need a certificate to cite on a CV – although, sure, there is one. But that isn’t – and shouldn’t be – the end goal.

10. How do you take formal beyond the theoretical?

We teach you what works in practice. We can do that because we have been practising formal verification for more than two decades. We don’t want to teach you text-book theories that may or may not work; we teach strategies that can be applied in practice – and we show you how to do that.

Having myself completed a doctorate in formal verification with emphasis on problem-reduction techniques and having used formal in the industry to achieve problem reduction for the last decade at numerous customers, I’ve learned much about what does and what doesn’t work. Armed with that knowledge, we can help others get up the learning curve that much faster – this is pretty much the goal. We don’t know it all, but what we know can make a difference for you.

11. How many people have you trained before?

Over a hundred, some of whom now work at top organizations; a lot of these are designers, and some are verification engineers and managers. Although we do teach a lot of new people, what surprised me most was the interest we had from practising formal experts who wanted to deepen their knowledge. To learn more about them, please check out www.axiomise.com/testimonial