I have been associated with formal verification for so long that I have always wondered why it remains a niche verification paradigm despite its tremendous success in numerous forms throughout the industry. We have seen the deployment of industrial grade theorem provers, commercial formal tools, and even scalable equivalence checking, yet formal still is not used every day by every design and verification engineer.

The reasons for this are complex and varied, but we can distill them down to the following:

1. Lack of good training

Formal training programmes usually focus too much on languages, and peripheral aspects of verification whilecompletely overlooking the methodology side. This has inevitably slowed adoption.

2. Lack of a good methodology

‘Methodology’ can mean different things to different people. If you ask a formal expert who has used the technology for end-to-end verification of a complex design block, he or she will say his or her methodology is what a methodology should be. But ask the same question of an engineer who has mostly used formal apps mostly or a lot of combinational equivalence checking (e.g., RTL-to-gate), and he or she will say that that is what a formal methodology is all about. The truth is that methodology should cover the entire spectrum of the use model ranging from shallow lightweight app-based formal to end-to-end deep formal, and the need for such breadth is insufficiently considered.

3. Lack of good processes

Of course, it is easy for us to blame poor processes for not being helpful either. But the truth is that indeed quite often the processes tend to sway in the direction of who said what rather than catalysing an approach based on metrics-based empirical analysis.

4. Lack of continuity on projects

I applied formal on Block A and got great results. You will hear this quite often from formal champions. But what plan did they have to repeat that experience on all the blocks leading up to Block Z. There is often no continuity in the application of formal even within the same project, never mind across the wider organizations within which design and verification taker place.

All of the above factors have contributed to a haphazard deployment of formal technology, and that has in turn lead to mixed results, mixed PR, and, worst of all, no further application of formal to mainstream functional verification. For functional verification in particular, formal should be used repeatedly to prevent corner case bugs from making it to the silicon. We cannot afford another Meltdown or Spectre.

Having spent a good 18 years since completing my masters in computational logic, learning about and deploying formal with success in both industry and in academia, I have concluded that we need to do better. I want to play my part towards making a positive difference. The only way for me to do that has been to create my enterprise that can realisethe vision that I have.

On 1 February 2018, Axiomise was born.  Its vision is to enable the use of formal in all verification throughout the diverse industrial segments that use semiconductors. We aim to accomplish this vision by working directly with end-customers, the hundreds of design and verification engineers, and empowering them with the best combination of training, consultancy and project support in formal.

Our training and consulting services are backed by years of experience working at the coal face, devising and deploying cutting-edge methodologies on industrial-sized projects. We now aim to transfer this know-how to everyone who wishes to use formal to carry out better verification.

When I talked about life moving fast some nine months ago in my first DocFormal article, I didn’t realize it was going to be this fast – and that I was going to make a locus change this soon. But hey that’s life, and here I am ready to start my career as CEO of Axiomise.

Let’s really get started with formal.

This article was first published on the Tech Design Forum. It is reproduced here in its original form for informational and archival purposes, with appropriate acknowledgment to the original publisher.