Industry Expert Blogs

Formal verification has gone through a number of eras. In the early 1990s, it was an area mostly of academic interest, only able to handle toy problems. Then, in 1994, was the infamous FDIV bug. As Intel's Bob Bentley said at the 2012 Jasper User Group meeting (before Jasper was part of Cadence):

Formal approaches suddenly gained a lot of traction after the 1994 Pentium floating-point divide bug. This caused Intel to take a $475M charge against earnings and management said, "Don't ever let this happen again". In 1996, Intel started proving properties of the Pentium processor FPU.

Then, before the turn of the millennium, Tempus Fugit was founded by Vigyan Singhal and Joe Higgens. It would eventually be renamed Jasper Design Automation. They pioneered commercial formal verification and introduced formal verification apps. This was the first generation of JasperGold apps.

In July 2014, Jasper was acquired by Cadence. The second generation of JasperGold apps were integrated into the Cadence Verification Suite and Incisive Formal technology, with performance increasing up to 15X over the years.

Another trend over the first couple of generations was making it easier for more and more verification engineers to be able to use formal approaches. In the early days, you needed a PhD in formal verification to be able to get anywhere. Then you needed to be a specialized formal verification engineer. Now it has become part of the toolkit of an increasing number of verification engineers, along with simulation. It is also increasingly a part of design signoff, not just a way of finding bugs earlier.