Formal Ensures Tight Working Relationships

Gabe Moretti of Chip Design used several points from Jin’s blog post below, in his recent article titled, “Design and Verification Need a Closer Relationship.” The article can be found at: http://bit.ly/1fGyXW2

Today, verification engineers have a whole arsenal in their tool kit in order to combat hidden bugs in the design. Different verification techniques render different working relationship with the designers.

Formal verification is a white-box verification technique, which means formal engineers need to have a good understanding about the internals of the design in order to do effective formal verification. Therefore, formal engineers and RTL designers naturally have a much tighter working relationship than other disciplines.

First, a sound verification methodology should allow equal contribution from all effective techniques, which includes leveraging the exhaustiveness of formal to sign-off on design blocks that are harder to verify with simulation. The block partition between formal and simulation should be clean to simplify the effort on both ends. To achieve that, formal engineers should participate in the architectural planning and exploration stage of design development in order to help influence decisions regarding design partition and block interface. A well-partitioned design with a clean interface will make the decision on where to apply formal, as well as the actual formal verification tasks, much easier.

Once design blocks are selected for formal, formal engineers will need some time from designers to understand the design under test. Often, this is done through reading a design spec, but some interaction with designers is needed to clarify certain situations.

In typical formal verification projects, the verification team needs a few hours of designers’ time to get a good understanding of the design. This exercise often turns out to be beneficial for designers as well. It gives them the opportunity to think about the interface between design blocks, improve design spec and, sometimes, fix issues in the design or spec.

When formal verification work starts, the interaction between formal engineers and designers is often done in the form of waveforms of counterexamples –– potential design bugs found by formal. The level of exchange depends on the quality of the formal testbench and the design. The quality of the formal testbench matters because an under-constrained formal setup could generate counterexamples that are not true design bugs. Therefore, it is important that formal engineers properly constrain the design interface and debug first to understand the reported issues before tossing it designers to review.

Designers often appreciate the formal traces because it reveals potential design bugs, even if it may not be a bug. Corner cases also help them learn the behavior of their own designs in these rare situations. Further, formal traces are often short, usually less than 20 cycles, so it is easy for designers to understand what’s going on without spending a lot of time debugging.

An ideal formal project is when the formal testbench and the RTL design mature at the same rate. When the design is done, formal verification also finishes confirming correctness of design behavior without the need to dedicate extra time after design for formal verification. This can be done because once a RTL feature is enabled, formal can test the implemented features to make sure they are implemented correctly. This is unlike simulation because a simulation testbench can only be enabled when the whole RTL code is implemented. This particular benefit of formal allows for parallel development of RTL and the formal testbench, reducing the overall project cycle and project cost.

When I think of the relationship between formal verification and design, I often compare it to two musicians, one on the piano, one on the violin, playing Beethoven Violin Sonatas. It’s a particularly striking analogy for formal engineers and designers who are in charges of the design project. Each has a different role, but the interwork of the two creates a wonderful piece of art –– a well-designed silicon with no bugs!

Tags: #52DAC, best practices formal verification, Break the Testbench Challenge, formal sign-off, Oski Technology

Category: Blog

This entry was posted on Wednesday, September 9th, 2015 at 1:04 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.