A deeeeep dive into Formal Verification 🤿
If you're a practicing verification engineer or an aspiring verification engineer, the best gift you can give to yourself would be the skill of Formal Verification. In ever expanding complexity of systems and increasing demand of Silicon industry, Formal Verification is the shovel that could help you ride this gold rush.
In the following post we will cover the MOST frequently asked questions about Formal Verification:
1. What is Formal Verification, how it solves, how it is different from Dynamic verification
2. Randomness in Formal Verification and automated stimulus generation
3. What is COI(Cone of Influence)?
4. How to write a property in Formal? How it verifies? How it works?
6. Non convergence of Formal properties? How to converge them – Abstraction techniques?
1. What is Formal Verification, how it solves, how it is different from Dynamic verification
To understand Formal Verification we first need to understand what exactly is verification and why are we doing it? After understanding the need for verification we will talk about the ways to optimize it.
Verification engineers are detectives for Silicon. They are responsible for observing, analyzing and catching the bugs in the RTL design. See the verification engineer as the defense wall between Silicon translation of RTL design and the RTL design code being drafted.
The Verification engineering team tries to break down the RTL design into pieces and analyze them – independently and then in sync. This takes time! Design Verification takes almost 80% of the overall time spent on chip development and verification engineers lose hair, sleep, peace, patience and a pinch of weekends on tight deadlines to deliver the quality of verification.
Each miss from Verification team can cost a potential revenue loss of Millions. The bugs can result in rolling back all the produced Silicon from the market – example : Samsung rolled back it’s Galaxy Note 7 – Turns out it was happening due to battery short circuit happening which was missed during the verification of the design .
RTL designing and verification is a tricky task because you can’t give an update or version upgrade like Software industry and you can’t translate your design to silicon for each update in design. Hence, you need to simulate and thoroughly analyze the design before actually sending the design to foundry. As you can sense it correctly, this is a very expensive process both in terms of Time and Money. Thus, there is a perennial need to be accurate and fast at all times.
Conventional way of verification involves having a DUT(Design under Testing) version of your RTL design and then writing test patterns to test the sanctity of the design. These test patterns are directed in nature, assume them as throwing darts on the wall – either you hit the target or you miss it, mostly miss it if taking the shot for the first time. This approach fails to cover all the possible scenarios and hence, most often than not we skip the verification of some crucial corner cases.
To save us from the misery – Formal verification comes for the rescue. Here we use a mathematical model of the design to verify the design thoroughly. It covers all the possible values a design variable can take and hence generating all the possible scenarios and stimulus for the design. Instead of throwing darts on the wall now, let’s imagine painting the whole wall. Since you’re covering the whole wall, you’re covering every possible corner cases as well.
In Formal Verification ,we are not required to generate stimulus or expected outputs like Directed Testcases (also known as Dynamic verification). The Formal Verification tool automatically uses it’s magic to generate the stimulus and implicitly covers all the cases. The only requirement of Formal tool is to give it the RTL design and a formal description of the specifications in form of PROPERTIES for covering all the input and output combinations exhaustively. Basically Formal Verification works on the principle of “failing to fail” to prove the design’s correctness. It generates all the possible stimulus and tries to fail your check. When it fails to fail – it states your design is correct else it stop immediately once a failure is found.
Let’s understand this through an example: You need to verify a DUT. You have two options:
1. You can generate possible input and output combinations on your own and write very specific test patterns to validate that the input you provided generates the expected output. This is known as Directed Testing of the design of Directed Verification. We use SV, UVM test-benches to write specific testcases to check the DUT
2. The other option is – a tool generates all the possible inputs possible for your design and you only describe the behavior or relationship of input with the output. This description of behavior is done using SVA(system Verilog Assertions).
2. Randomness in Formal Verification and automated stimulus generation
VLSI industry broadly uses 3 types of verifications -
1. Static Verification – Formal Verification
2. Dynamic Verification – Simulation Based Verification
3. Emulation & FPGA prototyping – Hardware Based Verification
Dynamic Verification: This simulation-based verification technology demands testbenches in HVL like SystemVerilog to verify the IP/Sub-System level RTL designs. Constrained-random, Assertions, Code and Functional Coverage are the most popular techniques/methodologies which are based on dynamic verification technology.
Emulation and FPGA prototyping: This hardware-based verification technology demands the user to synthesize and map the design & TB components on the configurable chip [FPGAs]. Emulation and FPGA prototyping are primarily used to verify complex chips & SoCs, running simulation at higher speeds, 5-10X greater than simulation.
Simulation-based techniques are unable to keep up with today’s growing complexity of the Chips and SoCs. This is particularly true when simulating large SoCs that include both software and embedded processor core models.
The emulation and FPGA prototyping have become key platforms for SoC integration verification where both hardware and software are integrated into a system for the first time. In addition to SoC verification, emulation and FPGA prototyping are also used today as a platform for software development.
Static Verification: This static verification technology demands user defined/ automated formal properties [assertions] to verify the module/IP level RTL designs. Examples of automatic formal application tools include: SoC integration connectivity checking, deadlock detection, X semantic safety checks, coverage reachability analysis, and many other properties that can be automatically extracted and then formally proven.
Let me give you 4 variables and ask you to draw all the possible combinations with these variables given that each element can only take binary values – 0 or 1. Since each element has 2 choices – 0 or 1, in total we will have 2*2*2*2 i.e 2^4 = 16 combinations. Now imagine you’re verifying the design for correctness. Using dynamic verification you will have to write 16 testcases to cover each possibility. Formal tool on the other hand will toggle each variable with all possible values and will keep on moving forward until it has covered all the possible cases. This means in dynamic verification you need to generate your own stimulus and also need to define what value to expect whereas this stimulus generation step is automated by Formal tool in case of Formal Verification.
3. What is COI(Cone of Influence)?
Let me tell you a story – a murder mystery!
Assume you are a detective and trying to solve a case where the victim was found dead on the bed. Can you tell me who killed the man or what was the murder weapon ? Strange request, right? I know!
Let me start giving you hints for the case now. The man laid in a pronated position and the bed sheets were crumbled as if pulled. A pillow was found crushed and thrown besides the bed in a corner with saliva traces on it. One last clue, dead body had all the signs of Asphyxiation (death by suffocation).
Does it ring any bells now ? If you’re with me on this case – I believe the victim was crushed with a pillow and he died due to suffocation.
A weird way to explain a technical concept but trust me you will be able to remember it better now.
Treat the murder mystery as a Verification problem. Detective as a Verification engineer. My first question about whodunit as the design spec being presented without any known aspect or features to find the bug. As soon as I started revealing the clues you started eliminating the irrelevant details and started focusing on the points which had some reverence to the mystery.
This whole process is known as CONE OF INFLUENCE in the respect of FORMAL VERIFICATION. You only focus on the parts which has some influence on the problem you are trying to solve and reject all the other possible values of variables which doesn’t. In the above example, it would have been futile to check what was being played on Television or what was cooked in the pan but it would have definitely costed you time and efforts. Hence, in formal verification you try to define this CONE OF INFLUENCE so that your mathematical model does not expand beyond requirements and result in state-space explosion.
Thus, Formal verification tool will try to toggle all the variable present in your design with all the possible values one by one to generate all the possible combinations that your design can take and then analyze all the possible combinations to check for correctness. This means introduction of each new element in the design increases the complexity exponentially for the Formal tool to analyze resulting in Higher computational power or Very high time requirements. Hence, we tend to draw an observation of parameters which actually impacts the design and are genuinely required for verification. We constraint all the other irrelevant parts of the design and this results in having a state-space cone which has relevant influence, better known as CONE OF INFLUENCE.
4. How to write a property in Formal? How it verifies? How it works:
We use SVA to write formal properties. Link to SVA Handwritten notes - HANDWRITTEN NOTES
Please check out the above notes which covers this topic in depth.
5. What are formal engines? :
Just like the engines of a car or any other vehicle. Formal engine is the actual heart and soul of the Formal Tool. It is the driving force. It determines how exhaustively the tool is verifying. It contains the algorithm which mathematically proves the correctness of your design.
This is an advanced topic and you should first watch this video to develop the understanding about how formal engines are coded:
*https://www.youtube.com/watch?v=9e7F1XhjhKw&list=PLZ5_EQH6uyVucnu20SS2BFQdVp_m_bznu&index=2&ab_channel=RobertBaruch : This covers what goes inside a formal engine and how the formal engines are coded. How are they able to generate the stimulus and verify that the design is correct.
* https://verificationacademy.com/seminars/what-is-formal-and-how-it-works-under-the-hood/instant-formal-expert-session : This gives you an insight about what goes inside a Formal Verification tool and how Formal engines work. What are formal property checking engines and how do they work? This requires you to make a SIEMENS account using your business (Official) email-id.
6. Non-Convergence of Formal checks? How to use Abstraction Techniques?
Owing to the nature of Formal verification, we tend to cover all the possible cases. This means as the variable in the design grows which means as the complexity of the design grows, it becomes exponentially difficult to cover all the states. Hence, the formal tool which adopts the pessimistic approach to verify design - trying to fail the checks unless all the states are covered - fails to cover all the possible states because it becomes very difficult to contain all the information generated so far. This is known as state-space explosion where the formal check or formal property fails to converge. The formal property is declared to be in INCONCLUSIVE State which means - it took so much time/memory or both that no conclusion can be drawn. Thus, to overcome the state space explosion or to optimize the performance of our Formal Setups we use some technique to reduce the computation power and time. These techniques are known as Abstraction Techniques. There are various Abstraction techniques like black-boxing portion of design, Applying cut-points in the design, Cone of Influence reduction, etc. This is very vast topic and needs a separate discussion to do justice with the subject. Please follow my blog to catch all the updates!
Resources And Recommended Readings:
1. https://www.systemverilog.io/ : (HIGHLY RECOMMENDED) Best blog to start formal verification and DDR concepts
2. https://verificationacademy.com/seminars/what-is-formal-and-how-it-works-under-the-hood : Gives introduction to Formal engines and how Formal tools work under the hood
3. https://besttechviews.com/formal-verification-tools-reviews-metrics/ : Formal Tools comparison and overview
4. https://www.youtube.com/watch?v=LfqNlRfpVWo&ab_channel=nptelhrd : NPTEL course on FORMAL VERIFICATION using Formality Tool
https://www.youtube.com/watch?v=VUr5jiQvUMY&ab_channel=EmbeddedSystemsDesign : NPTEL Course on Theory of Formal Verification
5. https://www.techdesignforums.com/practice/technique/doc-formal-my-10-golden-rules/ : 10 Golden Rules to apply Formal Verification
I have covered the complete strategy to crack VLSI jobs along with thorough notes in the this blog. I will be regularly sharing best resources for preparation as well as upskilling. Please share this post in your network – hopefully this could help someone achieve their dream.
BLOG: PLACEMENT PREP RESOURCES
Follow me for more insightful content! 💯
LinkedIn
Telegram
Comments
Post a Comment