by Paul B. Egan, Rockwell Automation
Using formal analysis to validate chip level connectivity is one of "The Top Five Formal Verification Applications" (Verification Horizons Oct 2012), and has been proven as the most efficient way to verify interconnects in complex Systems on Chips (SoCs) [3, 4, 5]. So, could formal analysis also be applied at the module level, even small modules? To test our theory, formal connectivity verification was first run on a relatively small block that contained eight instances each of seven different modules (56 instances total). We discovered that, not only does it work well on small blocks, formal analysis found two bugs that would have been very difficult to find in simulation.