Jasper: the Gold Standard for Formal Verification

It was the Jasper User Group JUG this week. I first went to JUG several years ago when Jasper Design Automation was still an independent company and JUG was held in Cupertino. It was clear to me then that Jasper Gold was the best formal verification technology available. If you are a small company and you are successfully competing against the big EDA companies with their package deals and broad sales reach, then you must have better technology.

Formal verification started life as a promising technology with very limited applications where it could be used effectively. Firstly, it is not much of an exaggeration to say that it took a PhD to run it. And secondly, the performance on anything beyond the smallest of designs was inadequate.

But a lot of things changed. The usability gradually improved, and the performance improved almost exponentially. At the JUG 2012, Bob Bentley of Intel gave a bit of history during his keynote:

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, they started proving properties of the Pentium processor FPU. Then in 1997, a bug was discovered in the FIST instruction (that converts floating-point numbers to integers) in the formally verified correct Pentium Pro FPU. It was a protocol mismatch between two blocks not accounted for in the informal arguments. Another escape. So they went back to square one and, during 1997-98, they verified the entire FPU against high-level specs so that mismatches like the FIST bug could no longer escape. During 1997-99, the Pentium 4 processor was verified and there were no escapes.

Also, in 1999, the forerunner of Jasper called Tempus Fugit was founded. They gradually developed, matured, and commercialized the technology. It has improved immeasurably more since I've been attending JUG. Even back then, Jasper marketed formal verification the way that Kodak marketed film: take more pictures, get more formal. The challenge was not so much that competitors were in the marketplace, but that too few people used formal techniques.

Of course in the middle of last year, Cadence acquired Jasper. When a company is acquired they face a big challenge. On the one hand they have a running business selling product, which already took 100% of the effort available. On the other hand, there is a requirement to integrate the technology, which takes the other 100%. But, of course, there is only 100%, plus some limited incremental resources if you are lucky.

Today Cadence has 80 engineers working on formal verification, 20 with PhDs. They are in five design centers: San Jose, Brazil, Israel, Sweden and India. There are nine global field centers with over 120 experts to assist customers.

Cadence had a large verification portfolio already, of course, with simulation, emulation, prototyping and more. Plus an pre-existing formal solution, catchily named the Cadence Incisive Formal Verifier. This all needed to be integrated and, especially, there needed to be a migration path for Incisive users. A lot of verification can be improved with the additional of formal technology. For example, there is no point in verifying with simulation that has already been proved with formal verification, and formal verification can be used to generate useful assertions to verify with simulation parts of the design that cannot be verified formally.

A lot of that integration has been done, although much remains. One focus is democratization of formal and automatic techniques. Partly this is evangelization and education. This doesn’t just mean by Cadence. A lot of the evangelization comes from formal experts in customers proselytizing other design groups and adapting formal techniques to the pre-existing design processes in companies like ARM, NVIDIA, Broadcom, Qualcomm, and more.

But democratization can be helped by new technology, too. In a presentation on Wednesday morning, Asa Ben-Tzur and Chris Komar presented a new JasperGold Expert System. This consists of two parts, a central database that tracks user experience at a fine-grained level and an expert system available to individual users to guide them through the learning process from getting started to becoming an expert to providing additional automation:

• Decrease initial tool/methodology ramp up (e.g., what clocks are in the DUT?)
• Remove the human bottleneck/enable users to do more on their own (e.g., what does an unreachable related cover mean?)
• Educate about formal methodology/techniques (e.g., I have an undetermined property, now what?)
• Educate when new features are released (e.g., new recommendation suggests latest engines)
• Automate day to day tasks (e.g., are there any complexity inducing structures in the COI of this undetermined property?)

It is currently in use with Cadence IP developers and multiple customers.

So, in summary, formal continues to grow on the back of mainstream verification flows, with the formal component growing rapidly. It has the highest ROI of any verification technology and is complementary to simulation and emulation.

If you didn’t attend JUG 2015, then you missed the largest formal verification event in the industry.