Formal Driven MDV – A New Tool for your Toolbox

Have you considered adding formal to your metric driven verification flow?  Maybe now is the time, as it has never been easier within Incisive Enterprise Manager to combine results coming from formal assertions with results coming from simulation, and visualize both at the same time.  You see the results of simulation, the results of formal, side by side, truly enabling you to utilize the right tools for the job. 

More importantly, how about the time you could save? Assertions are the worker bees of testing – they are the ones that actually perform the checks to ensure things are going as planned. Assertions are easy to write and very fast to execute, in either a formal tool (static testing) or a simulation tool (dynamic testing), so depending on what you need to verify, it can be an excellent choice.  Why not use the best tool for the job?  

Verify it once and move to the next thing.  There is also lots of flexibility with regard to how to implement the assertions -- they can be embedded within the design itself, or they can be separate test files applied to your design.  Assertions can be used to drive coverage where coverage represents the metrics associated to functional testing.   Now, imagine saving 20% or more of your simulation cycles by utilizing assertions and formal to verify a portion of your design.  On a large project that takes 6 months that could represent over a month of savings! 

Formal verification is a well-known white-box approach where mathematical techniques are used to prove an assertion or a property of the design.  The property to be proven may be related to the chip's overall functional specification, or it may represent the internal design behavior. Detailed knowledge of the behavior of design structures is often required to specify useful properties that are worth testing in the first place, also known as proofs.  

Thus, one can prove the correctness of a design without actually doing simulations. Another application of formal verification is to prove that the architectural specifications of a design are sound before starting with the RTL implementation.  But, how about an easy way to get started that will save time and enhance your verification environment.  One of easiest applications of assertions and formal technology is connectivity checking.  Some examples of connectivity checking is pad ring checks, checking that all the pins are properly connected in the SoC for the on-chip bus, or checking between the analog and digital parts of the design.  All of these are critical functions that need to be verified prior to tapeout, and all are easily implemented with formal technology.  There is a really good paper on located here on Cadence.com for the pad ring checking example if you are looking for more information.

So next time your planning your verification project, consider adding formal to your MDV flow – you'll save time and improve productivity.

John Brennan