Innovations in Formality Equivalence Checking: An Interview with Todd Buzan

Q: Hi Todd thanks for talking with us today. In your role as director of R&D for Formality, it is important for you to understand industry trends that are impacting formal verification solutions. What is the biggest challenge facing equivalence checking today?

Todd Buzan:

Customers are rapidly growing chip functionality which is resulting in increasing die sizes.  In addition, with the latest advances in logic synthesis at advanced nodes, designers employ aggressive synthesis optimizations to achieve their power, performance, and area (PPA) goals.

Synopsys’ industry-leading synthesis solutions, Design Compiler NXT and Fusion Compiler, provide a broad spectrum of optimization techniques such as retiming, multi-bit banking, and advanced data-path optimization that designers want to utilize for achieving maximum QoR.

These optimizations, however, are of little value if they cannot be verified through formal equivalence checking. Designers using 3rd party logic equivalence checking tools are being forced to switch off optimizations for those tools to successfully verify their design. This is forcing designers to sacrifice their PPA goals for the sake of verifiability.

Q: How is Formality addressing this challenge?

Todd Buzan:

Formality is the only tool on the market that can independently verify all of the Design Compiler NXT and Fusion Compiler advanced optimizations. We have countless examples of customers switching to Formality and seeing improvements in PPA by enabling aggressive optimizations in Design Compiler NXT or Fusion Compiler.

Formality is decisively bridging the gap between the level of design optimization achieved during implementation and what equivalence checking technology could readily verify.

So, in short, if Design Compiler NXT and Fusion Compiler optimize it, Formality will verify it. It is that simple. That is what we call “Best Verifiable QoR”.

Q: How does this really benefit the customer?

Todd Buzan:

The typical complaint we hear about 3rd party equivalence checking tools is that it has an inefficient setup process which can be iterative and error-prone. In the verification phase, it suffers from long runtimes and inconclusive results. When you add up all the man-hours and machine-hours, it takes longer to run a block successfully through equivalence checking than it takes to go through synthesis! Equivalence checking cannot be the bottleneck in the design flow.

Equivalence Checking must provide confidence to the designers that they can verify their designs without switching off optimizations or sacrificing their PPA goals. The verification process must be set up fast, accurately, and run to completion out-of-the-box to enable designers to meet their aggressive tape-out goals.

That is exactly what Formality delivers.

Q: With the September 2020 release, you are announcing that Formality is delivering “Best Verifiable QoR … Up to 5X faster”. Can you elaborate on that?

Todd Buzan:

Formality has always boasted of an arsenal of cutting-edge solvers that can verify the most complex, highly optimized, high-performance designs. The additional technology investments we have made are in the way we orchestrate these solvers to achieve maximum efficiency.

I am very happy to introduce our new distributed processing technology which harnesses the power of running verification on multiple workers. In this new scheme, Formality takes the existing design, splits it into partitions, and sends each partition to multiple workers running multiple strategies in parallel.

The results we see with this technology have been very exciting. Our customers have seen very clear benefits of up to 5X runtime improvement when they ran experiments on their toughest designs. But what is also very exciting to note is that they are seeing these benefits out-of-the-box. No manual intervention was required to iterate with the various strategies.

Just simply, out-of-the-box completion on what used to be the toughest blocks to verify.

Q: Great! Now that Formality is delivering up to 5X faster runtimes how does that change designers’ approach to synthesis?

Todd Buzan:

Synthesis and equivalence checking run in tandem. What we hear from our customers is that in an average project, a block goes through about 50 synthesis runs. They would like to run more often, but the limiting factor is really the long or inconclusive equivalence checking runs with 3rd party tools.

When Formality delivers verifiability with this kind of irresistible runtime advantage, we see customers switch over with no hesitation. What this enables, according to them, is an opportunity to run more and more synthesis regressions.

Which again simply means, Formality is delivering “Best Verifiable QoR…up to 5X faster”.

Q: Sounds like distributed processing in Formality is bringing an exciting new usage model to equivalence checking. Anything more in the roadmap that we can expect?

Todd Buzan:

Excellent question! We have been working on some cool new machine learning (ML) techniques which when productized, will ride on top of the distributed verification capabilities I talked about earlier. The idea is to develop a learning-based architecture into Formality that can predict the most effective techniques to achieve a verified result more readily.

Stay tuned and soon we will be able to talk in more detail about this ML-based approach in Formality.

Q: Thanks very much for sharing insights into Formality Equivalence Checking exciting new technologies!

Todd Buzan:

You are welcome! We are in an exciting new chapter in Formality and Formality ECO technologies. We have many more to come in the future.