The Future is Formal

Holly Stump, Vice President of Marketing, Jasper Design Automation

What predicts the wave of the future? In many cases, our customers show us the way. In other cases, new technology enables a new vision. And sometimes, industry trend analysis points to future necessities. When all three combine as they do for verification, it’s a Perfect Storm. Recently, participants in our 7th annual Jasper Users Group meeting enjoyed a number of compelling presentations describing new and innovative ways formal verification is impacting leading-edge SoC designs. In one notable case, formal was used to verify a very large and complex graphics processor, finding bugs that were missed in simulation and with other debugging tools. Verification results are obtained much faster thanks both to the inherent advantages of formal, and to scalable technology (high capacity, powerful engines, and distributed processing) of verification tools such as JasperGold. Trading low-cost computing time for precious engineering and calendar time is one key factor in targeted ROI.

Another speaker described the predictions in the latest ITRS roadmap for verification, which analyzed future trends in verification, and the increasing necessity for formal verification as design complexity rises. This speaker, who designs products for one of the leaders in visual computing, reported that their real-world results with Jasper prove that formal’s ability to find bugs and outperform simulation are helping them achieve results with 3.5x more efficiency, running three years ahead of the roadmap! Even more revealing, design productivity (measured by how many engineer years are needed to verify a certain number of transistors) exploded with formal and ran a full seven years ahead of the ITRS projection. How is this possible? Formal is infinitely more scalable than other verification technologies, and distributing tasks across server farms with highly intelligent management software provides sufficient proof power to meet the largest and most complex design challenges today, and in the future.

Jasper is currently pushing the formal envelope in a number of ways, facilitating RTL block design, IP reuse and retargeting, architectural specification and exploration, protocol certification with Intelligent Proof Kits that encapsulate critical behaviors for standard interconnect designs such as AMBA, and post-silicon validation, among other applications.

Several publicly available success stories from Jasper users describe in detail how they use formal technologies across the spectrum of SoC development. Please see A Formal Pot-Pourri by Laurent Arditi, ARM; NVIDIA Addresses Critical Verification Challenges with Formal Verification, by Ali Habibi, NVIDIA; and Maximizing the Value of Your Formal Run, by George Plouffe, Oracle.

One of our User Group members said it best, by stating that formal is “no longer just a verification technology.” Today’s designers and verification teams are harnessing these powerful tools early, and continuing to put them to work at every stage of the design cycle.