How I learned Formal Verification

Bing Xue is a dedicated Formal Verification Engineer at Axiomise, with a strong academic and professional foundation in hardware verification. He completed his PhD at the University of Southampton, where he conducted cutting-edge research on Formal Verification, RISC-V, and the impact of Single Event Upsets. Bing is proficient in RISC-V, System Verilog, and Formal Verification tools such as Cadence Jaspergold, and is skilled in Python and Linux, bringing a versatile and analytical approach to his work.

How I learned FV

I had no idea what Formal Verification (FV) was when I started my PhD,.  I spent six months exploring related papers, books, websites and open-source projects, as well as watching videos to learn about FV and System Verilog Assertion (SVA).  However, I faced several challenges during that time.

Some resources, despite being labelled as FV-focused, primarily discussed simulations. Others were too abstract, providing no practical details while some were too theoretical, presenting modelling and proving algorithms without real-world applications. After six months of study, I had a basic overview of FV but still didn’t know how to apply it to my project.

It took me another three months of hands-on practice with simple RISC-V designs to make progress. During that time, I made many mistakes and had to invest significant effort to understand and fix them. Searching for quality FV learning resources was time-consuming, and extracting the accurate information was even more challenging. I always thought that if I had access to well-structured FV courses, including theories, demonstrations, and practical labs with real world-designs, I could have completed my project faster and with better results.

Why Axiomise FV courses

I finished Axiomise FV courses last month. I believe they are the best courses for freshers and verification engineers. I wish I had discovered them earlier as they would have made a significant difference in my research journey.

FV is more than model checking

Most of the resourses I found provided only a general overview, covering the definition and history of FV.   These resources mainly focused on model checking, but FV is not just model checking!

The Axiomise FV courses cover not only model checking but also theorem proving and equivalence checking.  During my project, I mainly used model checking to evaluate fault tolerance and hardware reliability.  After completing the course, I was inspired to use equivalence checking to achieve improvement in my work.

Theory

I learned FV theories from books and papers.  These theories include transforming designs and specifications into mathematical models and formulas and proving formal properties with various (such as BDD- and SAT-based) algorithms.  However, are these theories truly essential for all verification engineers?

Given that formal tool can handle much of the modelling and proving, it is clear that verification engineers should focus more on why, when and how to use FV.  This is exactly what Axiomise FV courses emphasize.   These courses help verification engineers save their valuable time by focusing on the most critical and applicable concepts, rather than overwhelming them with unnecessary details.

Formal Techniques

A ‘smart’ formal testbench, composed of high-quality formal properties, significantly contributes to better performance by reducing run time and overcoming state explosion threshold.  But how can we develop formal properties with high qualities?

The Axiomise FV courses answer this question clearly: by applying formal (problem reduction) techniques to develop ‘smart’ formal testbenches.  These techniques, such as abstraction, invariants, assume-guarantee, decomposition, case splitting, scenario splitting, black-boxing, cut-pointing and mutation, are explained in detail within the course; accompanied by codes and examples for a deeper understanding.

What sets the course apart is the inclusion of step-by-step demos and labs that help learners master these problem reduction techniques.  All the other resources I found fail to explain formal techniques in such an easy-to-understand manner.  In my previous project, I didn’t apply all these techniques, which led to some inclusive results when verifying multipliers and dividers.  Now, I know effectively how to apply these methods to improve my project.

Demos and Labs

When learning to develop formal testbenches, I often wished for more high-quality demos and labs. Unfortunately, the resources I found typically offered either overly simplistic examples, like a basic request-and-acknowledge handshake protocol, or non-generalized designs, such as a specific meaningless hardware module.

I really enjoy the demos and labs in the FV courses. I could see their careful selection of designs used for demonstrations. For instance, the courses present FIFO, a fundamental structure in electronics and computing, as demonstration. Two brilliant abstraction-based methods are presented to exhaustively verify a FIFO: Two-Transaction and Smart Tracker.  Another valuable example is using invariants for scalable proof and bug hunting.

All serial designs, such as processors and memory sub systems, which are challenging to verify, can be represented and verified as FIFOs.  The FV courses also provide multiple demos and labs, such as variable packet design and micro-cache to demonstrate this concept.

From the FV courses, I strongly believe verification engineers can acquire all knowledge and skills required to formally verify complex designs.

The Complete FV flow: ADEPT

Most resourses agree that FV can be used for exhaustive verification, but the question is: how?  What is the overall process of FV?  How can one verify the correctness of a formal testbench? When is it appropriate to sign off?  These were questions I struggled with early on, as I couldn’t find any detailed standards or guidance. It took me considerable time to investigate and eventually realized that coverage was the key to answer these questions.

Axiomise addressed these challenges by developing ADEPT, the first industrial FV flow which clearly states the flow of FV sign-off.  The FV courses also introduce formal coverage.  Coverage in FV is more comprehensive than that in simulations.  These insights are invaluable for conducting efficient and confident FV workflows.

Benefits

Axiomise’s vision is to make formal normal and the FV courses effectively address three major misunderstandings about FV:

1. FV is not a mystery. With the training from Axiomise, all engineers (whether they are design engineers or verification engineers) can (and should) use FV in all stages.
2. FV is not a magic wand. A high-quality formal testbench is essential for effective bug hunting and exhaustive proof.  The FV courses provide all the necessary knowledge and skills to develop and evaluate such formal testbenches.
3. Learning FV is not hard. Following the FV courses, even beginners can smoothly transition into formal verification engineers.

Summary

In summary, the Axiomise FV courses are an invaluable resource for anyone looking to master formal verification. I sincerely recommend the FV courses to all design and verification engineers.

Also Read:

The Convergence of Functional with Safety, Security and PPA Verification

An Enduring Growth Challenge for Formal Verification

RISC-V Summit Buzz – Axiomise Accelerates RISC-V Designs with Next Generation formalISA®

Share this post via:

• 
• 
• 
•