Connectivity Checking Is A Perfect Fit For Formal Verification
By Tom Anderson, Semiconductor Engineering
Formal verification has traditionally been regarded as an advanced technique for experts to thoroughly verify individual blocks of logic, or perhaps small clusters of blocks. However, if you talk to anyone involved in the field these days, you’ll find that the majority of formal users are running applications (“apps”) targeted for specific verification problems. Further, many of these apps, notably connectivity checking, are being run at the full-chip level on very large designs. We’d like to use this month’s post to explore the links between these two extremes, looking at what has changed and what is likely to happen going forward.
Let’s acknowledge that the traditional view of formal verification is rooted in reality. Formal techniques exhaustively analyze all possible behavior for the design being verified. This stands in sharp contrast to simulation, which exercises only a tiny fraction of possible behavior by running specific tests. If no test triggers a design bug, the bug will not be found. If the bug is triggered but no change in results is observed, the bug will not be found. Given a sufficiently robust set of properties to describe intended behavior, formal tools can not only find all bugs but also prove that there are no more bugs to be found.
Analyzing all possible behavior is a mathematically complex problem. The number of possible states for even a small design is far more than the number of atoms in the universe. Formal algorithms don’t consider these states one by one, unlike simulation. However, the larger the design the more analysis is needed. Sequential depth is also a factor in complexity. There are regular breakthroughs in the power and performance of formal algorithms, so users now run on large blocks and clusters unimaginable just a few years ago.