Verification is a process that ensures that the given design functions as per specifications. When we use the word ‘functions’, we also imply that the timing, form factor and power requirements that have been ‘specified’ are also met by the design. Verification thus is something that consumes a lot of time and effort and it wouldn’t be surprising to note that verification takes up about 70-80% of efforts in a typical ASIC cycle.
There has been a significant shift in the verification domain as we moved from the legacy procedural test benches to the more sophisticated layered test benches. A lot has been done and researched to build test benches faster and hence speed up verification. The ‘most’ popular mode of verification is and has been ‘functional’ verification. However, to begin the functional verification of a design a ‘significant’ amount of testbench code needs to be written. This can slow down the verification process and sometimes make it error prone too. Hence a need arises to find means and methods to ‘augment’ the verification process. While, there are many ways in which verification can be ‘augmented’ or ‘enhanced’ such as Hardware Acceleration, FPGA based acceleration, in-circuit emulation and Formal Verification. We shall talk here more about Formal Verification, its advantages and what sets it apart from functional verification.
What is Formal Verification?
Formal Verification is a different way of verifying a design. “Verifying the design until it is found to be bug-free”, is also the end goal of formal verification like its functional counterpart. As per its Wikipedia definition, In the context of hardware and software systems, formal verification is an act of proving or disproving the correctness of the intended algorithms underlying a system with respect to a formal specification or property, using formal methods of mathematics. Sounds complicated, isn’t it? Well, the fear of formal verification being ‘beyond reach (read comprehension)’ and difficult’ keeps most verification engineers and designers miles away from it. It may seem overwhelming in the beginning, but it comes with a lot of advantages that make it worth the struggle. In the formal verification method, testbench, coverage, checkers and constraints, all of it can be written using System Verilog Assertions.
The above figure depicts a typical formal verification framework, as we see it is devoid of testbench components such as a driver, a monitor, a scoreboard, etc.
What sets Formal Verification Apart From its ‘Functional’ Counterpart?
‘Functional Verification’ requires building a major chunk or sometimes the entire testbench code for verification to begin. Each and every part of the testbench code has to be written. One writes the test case that defines ‘when’ and ‘what’ stimulus needs to be injected. Generators are written to randomize transactions, while driver code is written to ‘drive’ the DUT signals as per the protocol followed by the DUT. A detailed reference model is also created that mimics the design and checkers and scoreboard are also coded that compare the design output with the ‘reference model’ output. Thus, the entire responsibility of ‘verification’ is shouldered by the verification team and all the tool does, in this case, is to simulate the design at every clock tick. It can be equated to a dinner party wherein the verification engineers are those ‘nameless’ chefs who have slogged all the while to dish out all the delicacies while the one who sets the buffet table which in this case is the ‘simulation tool’ comes across as the ‘hero’. Also, since the verification team needs to code a reasonable amount before it can ‘actually’ begin the design verification process. This approach sometimes can be difficult as verifying certain parts of the design such as complex state machines or arbiters or even multiple access to a single resource or clock domain crossing can be time-consuming as the DV engineer needs to spend a lot of time defining and developing means to verify such complex pieces.
Now let us take a look at how formal verification works and how it can ‘augment’ the verification process. As we spoke earlier, formal verification is also intended to find bugs in every nook and corner of the design. But, the testbench, checkers, constraints and coverage are all written using SVA (System Verilog Assertions). Which means that test bench is a bunch of ‘assertions’, the concept of drivers, monitors, generators or other typical testbench components is absent. The first advantage that arises from this is that the verification team can begin verification much earlier as they can keep adding assertions and verify the design almost in parallel. At the very basic level, the design can be described as an interconnection of logic gates and flip-flops which can be represented by a mathematical equation. Each checker is analyzed mathematically by the tool and it then checks for any sequence of inputs (these include inputs, outputs or internal variables of the design that affects the checker) that would fail the checker. If the tool finds an input sequence that leads to a checker failure, it dumps this error condition into a waveform. The waveform generated as a result of a checker failure in formal verification method is called the ‘Counter Example’. Thus, we can easily conclude that a major share of the verification task is now shouldered by the tool unlike that in the case of functional verification.
This is how formal verification works
- The design inputs or the internal properties of the design are constrained as per the specifications. This is done by the SVA ‘assume’ directive
- Internal outputs of the design or variables are verified by writing checkers. The checkers are written by using SVA Assertions.
- The coverage is collected using the SVA cover directive.
- One can also write (if needed) reference models specific for a checker. Coding a detailed reference model can thus be avoided.
- When the tool receives the design and the checkers it breaks down both into mathematical equations. Hence, the formal tool goes hunting for bugs by hunting for input sequences that would prove the checker wrong and all of this is done ‘mathematically’.
When Should We Use Formal Verification?
It is important to bear in mind that formal verification is a means to ‘augment’ functional verification. It certainly does not imply that it can ‘substitute’ the latter. There are certain logic blocks that need ‘extra’ verification and that is when formal verification saves the day. Industry experts suggest two vital situations in which the verification engineer can especially resort to formal verification. One is when the code to verify is very complex such as complex state machines where it makes sense to write checkers that can plug into the internal variables of the design and verify if the state machine responds appropriately to both sanity as well as stress testing. The second situation in which the DV engineer can seek ‘additional’ assurance is when there is a code within the design that gives a hard time to both the DV and design engineer. This could be a shared resource such as a memory or even clock domain crossing which can prove to be quite unnerving.
Summary
Just as ‘augmented reality’ adds to or enhances the existing reality in gaming, movies and the likes, augmented verification such as formal verification augments or enhances the verification process. While augmented reality serves to add an extra treat to the senses on top of reality, augmented verification serves to provide ‘extra relief and/or assurance’ to the DV engineer. Formal verification like its functional counterpart also works towards finding the tiniest bug(s) in the design, but its modus operandi is different. Functional verification needs a considerable amount of code such as test cases, drivers, monitors, generators, scoreboard, etc to be written before verification begins. Formal verification does not need too much code to be written before the verification process can begin. It has no concept of driver, monitor, generator or even test cases, unlike the conventional test benches. Formal Verification entails writing the testbench as a bunch of checkers and cover points using SystemVerilog Assertions (SVA).
In functional verification, a DV engineer needs to do a lot of coding while the tool simulates the design clock by clock. Thus, in this case, the tool is quite ‘underutilized’ while the DV engineer is ‘overworked’. The formal verification approach works quite the opposite way. The design at a fundamental level can be viewed as a bunch of interconnected logic blocks and flip-flops and this can be represented by mathematical equations. In the formal verification approach, the tool analyses each and every checker or SVA (which includes all the inputs, outputs and internal variables of the design that would influence the checker) and looks for input sequences that would ‘falsify’ the checker. If the checker fails, the tool would dump the error condition into a waveform called the ‘Counter Example’. Thus, unlike functional verification the tool in case of formal verification is ‘utilized smartly’ and the DV engineer isn’t overworked either. This sounds like a ‘win-win’ situation isn’t it?! Formal verification is particularly useful when there are pieces of code that are difficult to penetrate or verify such as complex state machines or clock domain crossing. System Verilog Assertions or SVAs plug into the internal variables of the design and verify the design as well as execute design coverage by means of the ‘cover’ directive. If needed, the DV engineer can write a small piece of code that serves as a reference model ‘specific’ for a checker, thus avoiding the need to write a detailed reference model. Formal verification hence is a very useful mode of verification with a plethora of advantages that are impossible to overlook. It gives additional assurance, confidence and hence relief to the DV team regarding the correctness of the design. In short, if the costs of re-spin haunt you, formal verification works like the witch doctor!