Jasper Announces Sequential Equivalence Checking

Jasper Announces Sequential Equivalence Checking
by Paul McLellan on 03-31-2014 at 8:00 am

 Jasper finally announced their sequential equivalence checking app this morning. I say finally because they haven’t really tried to keep it a secret. They talked about it at the end of last year the Jasper User Group meeting and it has even had a page on their website. But formally the product was announced today.

The new JasperGold SEC App enables designers to exhaustively verify the sequential functional equivalence of RTL implementations, ensuring that they function identically. And 10x faster than competing tools.

SOC designers often make changes to RTL that may not be purely functional. Low power optimization, using structures such as clock gating, power gating and power domain partitioning is a common motivation for such changes. Other changes might be motivated by the need to optimize performance or insert ECOs into the design. Faced with two versions of the RTL design, the designer needs to verify that the new RTL is sequentially equivalent to the previous RTL even though the details behavior of the internal registers may be different. Comparing the two versions of the RTL in simulation can take weeks of regression runs. In addition, because simulation is non-exhaustive by nature the results are far from certain and so formal techniques are much better. The SEC App can accept large sub-system blocks as well as complete SOCs and compare the two versions of the RTL orders of magnitude faster than simulation.

The SEC App leverages a combination of algorithmic techniques, new optimized engines, and a customized GUI—all specially targeted for equivalence checking challenges. For example, one customer reported that with only one machine, Jasper’s SEC app was able to simultaneously verify timing fixes, chicken bits, clock gating validation, and power optimizations in only 45 minutes. This performance completely blew away their prior simulation-based regression flow that took five days to run on a whole rack of computers.

Two of the lead customers for the SEC App are STMicroelectronics and nVidia.

In ST’s GPU designs, they have systematically replaced the incoming memory blocks of IP modules with a different memory architecture, specifically optimized for 28nm FD-SOI Low-Power Platform. The Jasper SEC App allowed them to very smoothly verify that this substitution did not alter the behavior of the design, giving them strong confidence in the resulting optimized GPU micro-architecture. They can now run exhaustive checks in hours vs the weeks it used to take to run a non-exhaustive simulation.

At DVCon a month ago, NVIDIA’s Syed Suhaib presented a paper on clock gating verification with the JasperGold SEC App. You can watch the a brief interview with him here.

And an overview video of the SEC App is here.

More articles by Paul McLellan…