Blog: What is still missing in your FPGA design verification methodology?

What is still missing in your FPGA design verification methodology?
—

In the past, we would have seen that Formal methods and Assertions predominantly featured in the ASIC world but times are changing. Today, with the increase in the complexity of FPGA designs, reflected by simulations taking hours and even days to complete, and the need to catch bugs earlier on, Assertions are becoming more popular in the FPGA world too. If we don’t incorporate Assertions and Formal into our flow; bugs could go undetected during the simulation phase, and we would need to spend longer to attain our coverage goals.

In my previous blog, I talked about how to achieve our Coverage Goals using the Aldec Riviera-PRO simulator for functional simulation. Still, in today’s context, this flow seems to be somewhat incomplete.

Broadly speaking, verifying any design comes with two challenges: Controllability (the stimulus) and Observability (Checker at the Output). If any of these conditions are missing or incomplete, there is a possibility for some of the bugs going undetected into production. However, using Assertions can help us to overcome both these challenges for the following reasons. Firstly, the need for the bugs to be propagated at the output pins for observability gets eliminated. Furthermore, it makes it easier to detect bugs closer to the source, thereby reducing the debugging time as well. An IBM study corroborates this, claiming that by using Assertions, debugging times fell by a staggering 50%. Moreover, the studies done by Wilson Research have shown that by adopting Assertions in the verification flow, it has been possible to reduce the bug escape into production dramatically. This is shown in the diagram below.

You will often hear the term ‘Assertion-Based Verification’ (ABV) used to describe the whole verification process. However, this process deals with more than just assertions as the flow comprises a mixture of sequences, properties and covers. Furthermore, there are two languages available with practical applications of expressing assertions, namely Property Specification Language (PSL) and SystemVerilog Assertion (SVA). Although they are relatively new, they are governed by IEEE Standards.

Having touched on the benefits of using Assertions, we will now look at the advantages of using Formal in our flow. Firstly, unlike simulations (that are dynamic), Formal verification is static; therefore, it does not require tests or test benches to execute the design. Instead, it statically analyses the design for all possible input sequences and all possible state values, checking for any violated assertions. Formal has entered the mainstream in recent years as it allows for exhaustive verifications while simulations have a small chance of hitting every corner-case bug.  Hence, Formal represents another approach in determining precise coverage metrics and is complimentary to simulation. FirstEDA also represents OneSpin and their class-leading Formal solutions. If you would like to know more, just get in touch.

I do plan to introduce you to SVA using Aldec Riviera-PRO simulator in one of my future blogs. Stay tuned!