Verification Challenge
As chip design complexity continues to grow astronomically with hardware accelerators running riot with the traditional hardware comprising CPUs, GPUs, networking and video and vision hardware, concurrency, control and coherency will dominate the landscape of verification complexity for safe and secure system design. Even Quintillion (1018) or Sexdecillion (1051) simulation cycles will not be adequate for ensuring bug absence. Bug escape continues to cause pain and some of these will end up causing damage to life.
It becomes blatantly obvious when you look at the best industrial survey in verification conducted every two years by Harry Foster and Wilson Research. With only 68% of the ASIC/IC designs getting built the first time-around and the same number running late, the story of FPGA based designs is even worse – with only 17% hitting the first time-around mark. I’m not a pessimist, and every time I look at the trends of such reports it doesn’t make me feel that we are accelerating the deployment of the best verification methods known to mankind.
The Promise of Formal
Formal methods are a mathematical way of analysing requirements, providing clear specifications and makes use of computational logic under-the-hood to confirm or deny the presence of bugs in a model. This model can be a hardware design expressed as Verilog or VHDL, or any of the other languages such as Chisel, BlueSpec SV or even gate-level netlist. The only way of obtaining 100% guarantees that a given model doesn’t have functional defects or violates security or safety requirements is to verify it with the rigour of formal methods assisted with a great methodology.
A great methodology doesn’t exist in vacuum and is built as a collection of best practices on top of the technologies and describes ‘how’ these technologies can be used.
The how is therefore an important question to answer.
Challenge with formal methods: Lack of good training
One reason why formal methods adoption has been limited is because of the lack of know-how. While we may take a step back and understand the myriad reasons for this to be the case the foremost reason of why formal is not everyone’s cup of tea is because of lack of good comprehensive know-how. Formal methods have an exciting history with numerous landmark contributions from eminent computer scientists but for engineers it continues to be enigmatic. It is still perceived as an abstruse subject – the only exception is the use of apps by engineers thanks to the EDA companies who provided automated solutions to help solve bespoke problems. Formal market is now estimated to be 40% of the simulation. The automation provided easy-to-use tools that can provide an easy starting point on one end by the use of static lint analysis and on the other extreme end, solving problems like connectivity checking, register checking, X-checking, CDC and so on.
Between the two extremes, sits the rest of the interesting landscape of verification problems solvable through model checking also known as property checking as well as equivalence checking. Methodology is the key to success to everything and is no different for property checking. But a good methodology has to be on problem solving and should not tie you to a particular tool.
While I’m a huge fan of property checking and production-grade equivalence checking technologies, they do not solve all the verification problems. For example, if I’m interested in making sure that a compiler works correctly, or an inter-connect protocol model doesn’t have deadlocks, I may have to look beyond the run-of-the-mill property checking solutions. This is where theorem proving comes in.
Theorem provers do not suffer from capacity issues like dynamic simulation, or property checking tools and if you know to use them well, they can be used to verify theoretically infinite sized systems including operating systems and compilers as well as huge hardware designs.
There are several questions.
- Where do you go to learn about all these formal technologies?
- Why should you learn formal?
- What is formal?
- How does one find an accelerated path of learning formal with support without getting locked in a vendor tool?
Formal Verification 101
Welcome to Formal Verification 101 – the world’s first on-demand, self-paced, video course that provides a comprehensive introduction to all essential aspects of formal methods leading to a certification at the end.
This course comes with an online lounge accessible to the enrolled students where they can discuss any questions and engage with experts.
Let me first give you a personal perspective on why I decided to do this?
A Personal Perspective
Designed and delivered by yours truly, I took time to understand what has worked for me and what didn’t. When I started learning formal over two decades ago, we did not have video courses in computational logic. While I took many courses in my master’s course, as an Electrical & Electronics engineer it was a steep learning curve. A large part of it was that we were not given a lot of practical perspectives. I was learning something in theory but didn’t know why and where it was useful.
I was lucky to work on my Doctorate with Tom Melham at University of Oxford and really lucky to have had a few hours with Mike Gordon from University of Cambridge who taught me how to use the HOL 4 theorem prover. If you’re not aware, both Tom Melham and Mike Gordon were one of the first few computer scientists using higher-order logic and formal for hardware verification. However, not everyone, can get the opportunities I got at Oxford and Cambridge.
I have been working in the industry on projects and have been training engineers in the industry in practical use of formal and have trained nearly 200 engineers including designers and verification folks in semiconductor industry. Working on cutting-edge designs, with shrinking time schedules gives me a strange sort of excitement and joy but teaching and sharing what worked and what didn’t equally give me a thrill. So, as it happens, I love sharing knowledge and enjoy teaching.
Two decades later
When I founded Axiomise, three years ago, there was still no video courses covering all the key formal technologies from an industrial perspective. In fact, there wasn’t a structured course covering all three formal technologies from an industrial perspective. There have been a few tutorials in theorem proving, or scanty material on property checking off and on, but no comprehensive introduction to all the key formal technologies in one place with a practical perspective delivered as a standalone course with online support.
Meanwhile, we built a range of instructor-led courses spanning from 1-day to 4-days that are designed to offer in-person tutorials in a structured manner covering theory, labs, and quizzes. The goal is to provide production-grade training to engineers in the industry. In its third year, this course is in demand and we continue to provide this training through face-to-face via Zoom. We issue certificates of completion. The main advantage of these courses is that I deliver them in-person. Students gain insights on real-world problems and get a chance to ask questions live during the training and get their hands dirty on hard problems where we learn together how to solve them.
Bridging the gap in industry
What we discovered was a gap in the industry and our own portfolio. Whereas our instructor-led courses are great for a newbie or a practising professional, these courses are not self-paced, and there is a commitment to multiple-days consecutively which can be a challenge for some people. Formal Verification 101 course is designed to bridge this gap. You can take this comprehensive introductory course at your own pace, in your own time and learn the fundamentals of formal methods covering all the key formal technologies such as theorem proving, property checking and equivalence checking. We take an interactive approach to learning in this course by providing you with hands-on demos that you can redo yourself by downloading the source code, and gain experience of seeing formal methods in action. Once you’re comfortable with this course and pass the final exam and would like to explore more advanced concepts, you can take the multi-day instructor-led courses.
Expert Opinions
When I completed the course design, I invited several peers from industry and academia to take this course, review it and offer feedback.
I had to be conscious in choosing my first audience, so I wanted a spread the experience level, as much as geographic spread. We gave this course to Iain Singleton a formal verification engineer, Rajat Swarup – Manager at AWS, Supratik Chakraborty, Professor at IIT Bombay and Harry Foster, chair of the IEEE 1850 Property Specification Language Working Group.
They provided a candid and open feedback available to read on https://elearn.axiomise.com
Harry Foster humbled me with this comment.
“I’ve always said that achieving the ultimate goal of advanced formal signoff depends on about 20% tool and 80% skill. Yet, there has been a dearth of training material available that is essential for building expert-level formal skills. But not anymore! Dr Ashish Darbari has created the most comprehensive video course on the subject of applied formal methods that I have ever seen. This course should be required by any engineer with a desire to master the art, science, and skills of formal methods.”
With videos, text, downloadable source code, interactive demos, quizzes and a final exam leading to a certificate we have got everything covered for you. I’ve myself, sat down and recorded all the content, created the captions for all the videos so people with challenges can also enjoy the course.
It has been 20+ years of living in trenches, years of planning and several months of production that has gone in this work. I hope you will give this course a chance and join me in my love for formal.
Let us collectively design and build a safer and secure digital world. Sign up for the unique course in formal methods at https://elearn.axiomise.com.
Also read:
Life in a Formal Verification Lane
Accelerating Exhaustive and Complete Verification of RISC-V Processors
CEO Interview: Dr. Ashish Darbari of Axiomise
Share this post via:
TSMC Unveils the World’s Most Advanced Logic Technology at IEDM