I have been associated with formal verification for so long yet I still wonder 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. But formal is not used every day by every design verification engineer.
The reasons for this are complex and varied, but we can break them down into the following:
- Lack of good training
Formal training programmes usually focus too much on languages and peripheral aspects of verification. They completely overlooking the methodology side. This has inevitably slowed adoption.
- 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 that his or her methodology is what a methodology should be. But ask the same question of an engineer who has mostly used formal apps or a lot of combinational equivalence checking (e.g., RTL-to-gate), and he or she will say 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. The need for greater breadth is insufficiently considered.
- Lack of good processes
It is easy to blame poor processes for not being helpful either. The truth is that current processes often tend to favor ‘who said what; rather than catalyze an approach based on metrics-based empirical analysis.
- Lack of continuity
“I applied formal on Block A and got great results.” You hear this frequently from formal’s 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 across a single project, never mind across the wider organizations within which design and verification taker place.
All these factors have contributed to a haphazard deployment of formal verification. Such a deployment has led to mixed results, mixed PR, and, worst of all, the stuttering application of formal for mainstream functional verification.
For functional verification, formal should be used repeatedly to prevent corner case bugs reaching final 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 academia, I have concluded that we must do better. I want to play my part toward making that happen. The only way for me to do that has been to create my enterprise that can realise the vision I have.
On 1 February 2018, Axiomise was born. Its aims to enable the use of formal in all verification throughout the diverse industrial segments that use semiconductors. We will accomplish this by working directly with end-customers, namely the hundreds of design and verification engineers out there. We will empower 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 will transfer this know-how to everyone who wishes to use formal to carry out better verification.
In my first Doc Formal post nine months ago, I talked about life moving fast. I didn’t realize it could be this fast – and that I was going to make a locus change this soon. But hey, that’s life. Here I am, ready to start my career as CEO of Axiomise.
Let me invite you to check out www.axiomise.com for more information. Let’s really get started with formal.