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.

Machine Learning-Enabled Smart Formal Verification

Today at CDNLive EMEA, Cadence announced the third-generation of the JasperGold platform, now with machine learning-enabled smart formal verification:

• Smart Proof Technology, with machine-learning for solver inference and multi-advisor orchestration
• Ongoing optimization
• Advanced design scalability, with 2X design capacity increase and 50% memory footprint reduction
• Signoff-accurate formal coverage with new intuitive analysis GUI

STMicroelectronics was an early user. Mirella Negro Marcigaglia is their digital design verification manager:

We measured 2X faster proofs out-of-the-box, 5X faster regressions, and non-converged properties reduced by half.

Smart Proof Technology

Smart Proof Technology uses machine learning for solver inference and multi-advisor orchestration. Machine learning is used to select and parameterize solvers to enable faster first-time proofs. Additionally, machine learning is used to optimize successive runs for regression testing, either on premises or in the cloud.

For solver inference, we use supervised learning on over 500 customer designs, then the best-fit core engine is selected and configured to create a custom solver. This leads to up to 4X, with an average of 2X, better out-of-the-box proofs.

For multi-advisor orchestration, multiple proof advisors use reinforcement learning to improve proof efficiency. This uses training data for better out-of-the-box proofs, and adjusts training data using proof profiling for up to 6X, with 5X average, better subsequent proofs and regressions.

Ongoing Optimization by the Numbers

Core engine performance: Benchmark suite is nine fully converging designs. Increase of 9.5X in properties per second.

Core engine proof success: Benchmark suite is seven hard designs with a significant number of undetermined properties. 37% reduction in the number of undetermined properties.

Advanced Design Scalability by the Numbers

Benchmark suite is six big designs from four different customers. The minimum compilation speed is 100M gates per hour. Peak memory is less that 1.3KB per gate. There is a 70% peak memory reduction on big designs, 50% peak memory reduction across all designs.

Signoff-Quality Formal Coverage

There is a new coverage analysis GUI, with intuitive metrics views and navigations. Coverage collection runs independently from proof runs.

There is signoff-accurate proof-core coverage with a single view of the COI and proof core, and a new high-precision proof-core mode. New formal coverage metrics combine stimuli and checker coverage that provides a single metric for coverage signoff.

Save the Date

This year's JasperGold User Group will be November 6 and 7.  Join the world's largest annual gathering of formal verification experts. Details to come nearer the date.

Sign up for Sunday Brunch, the weekly Breakfast Bytes email