Formal Flows From a Simulation Point-of-View
At the end of Your First Step Into Formal Property Checking, I said the effort I put into understanding formal property checking “Makes me wish I had a time machine to see PropCheck sooner”. I wondered how formal property checking earlier in my career would have improved my productivity.
Now I want to hop into the time machine for a different reason. If I were leading a product team, how would I deploy formal? Not just formal property checking, but all formal? What flows do I choose from? Who runs the tools and what value would they expect in return?
After a bit of navel gazing and a few discussions with colleagues, I decided on a list of useful flows. Consider them formal food-for-thought from a simulation point-of-view.
Qualification
The qualification flow traps unintended design issues before they make it into the code base. It includes AutoCheck and X-Check to detect things like latches, FSM lock-ups, dead code and hanging logic; also CDC and RDC to validate clock and reset crossings. Physical design is the primary beneficiary of qualification though it also establishes a functional baseline to verification.
Design engineers drive the qualification flow starting with the first code check-in; ideally running before every check-in. The advantage of employing a strict qualification flow early is avoiding a forced, and more painful, qualification down the road.
(It’s worth mentioning now that early is a common theme to all the flows I envision – reduce the cost of debug by trapping bugs as early as possible with the minimum effort required!)
Functional Compliance
The functional compliance flow adds an element of specification-level functional quality to RTL qualification. This involves the addition of PropCheck to do black-box formal property checking on external interfaces. Formal property checking delivers an improved quality baseline into block-level and top-level verification.
Functional compliance should be a shared responsibility between design and verification engineers where both teams add and prove black-box assertions. 3rd party Verification IP is also an option, particularly for industry standard interfaces. The Questa Formal Library (QFL), for example, includes formal Verification IP for AMBA. Again, I suggest functional compliance checks placed early (i.e. as interfaces are implemented) because bugs on external interfaces tend to be show-stoppers for verification teams.
Quality
The quality flow showcases PropCheck in a proactive effort to eliminate functional RTL bugs at the source through the addition of white-box properties. In a nutshell, white box formal property checking brings substantial improvement in functional quality of RTL through dramatic bug reduction.
Design engineers should own formal property checking because (a) properties tend to be implementation dependent; and (b) design engineers best understand the implementation. The scope and focus is variable. On one hand is a targeted approach of verifying just critical portions of a design. On the other is an approach of exhaustive functional correctness. Either way, the goal here is to trap bugs before they permeate through the rest of the team.
Personally, I see formal property checking as the first big step toward bulletproof RTL that keeps you off the debug hot-seat at crunch time. There is one more step though. If you’re really fed up with RTL bugs, consider…
Property-Driven Development
Property-driven development (PDD) is a method of formal property checking whereby properties are captured before RTL implementation. It’s based on test-driven development (TDD), a closed-loop, methodical, rigorous approach to coding software. The goal is bug-free RTL.
Design engineers own PDD. As for the new quality advantages from PDD, see my previous comment about bullet-proof RTL and multiply it by 10! Bug-free RTL is possible with the right tool and technique!
Verification Pre-bug
Not debug, but pre-bug. Pre-bug is effort spent by a verification team to protect itself from RTL bugs prior to simulation. This is basically AutoCheck and X-Check in a pre-simulation qualification flow.
Pre-bug is only necessary in situations where the design team hasn’t instituted a rigorous formal qualification flow of its own. If this is your case, the verification team can build and take advantage of a pre-bug flow. Ideally, that flow then migrates to the design team to become a proper design qualification.
Integration
Focusing on issues that are critical at the chip level, the integration flow includes Connectivity Check, X-Check and AutoCheck. Connectivity Check and X-Check are crucial for confirming connectivity between subsystems while AutoCheck flags obvious functional incompatibilities between subsystems; specifically, issues related to flow control and possible lock-ups. CDC and RDC are back to validate chip level clock and reset crossings. RegisterCheck is another option for validating chip-level register accessibility.
The integration flow is particularly important because integration bugs can be an absolute nightmare. Their broad scope makes them difficult to root cause so they commonly inflict debug cycles across a large swath of a development team. The integration flow provides the means for quickly identifying connectivity and compatibility issues to avoid this type of team-wide debug.
The integration flow is another shared responsibility. Ideally, the design team triggers the extra checking in qualification. Verification engineers may also run the integration flow as part of regular regressions.
Coverage Closure
I see constrained-random test suites continuing as the key driver toward coverage closure. But CoverCheck is a valuable addition for reachability analysis before coverage holes are targeted with new tests.
The “Last Stop” Flow
We finish with what I’m assuming is the typical, entry level flow for many development teams. Because formal apps are easy to run, they are a viable, last stop bug hunting option to employ before tape-out. A team can run them all, save for possibly PropCheck, as the last hurdle.
The last stop flow is something you should (a) only use once; and (b) only use once!
I realize it’s easiest to frame the value of formal tools in terms of critical bugs found. And that a pre-tape-out showstopper obviously qualifies as a critical bug. But formal provides enough credible options that waiting for that type of feedback shouldn’t be necessary anymore. Not to mention that the “last stop” does nothing – zero! – to improve your productivity along the way. So run it once if this is where you’re at in your development cycle. But follow-up by integrating specific flows to begin the next cycle to really take advantage of the tooling.
All Said…
Given my sheltered existence within simulation over the last 20 years, I’ve known nothing about formal for a long time. But with minimal effort, I now have a decent idea of how I’d use formal with a product team. Especially with the formal apps, there is a lot of value for very little effort.
My advice to other engineers that have lived exclusively in the simulation paradigm: take a look at formal! Regardless of your responsibilities and where you are in your project cycle, there will be several good options. Find what’s right for you and talk to others about what might be right for them. And remember, earlier is better with formal verification. Run the tools now and keep running them.
No need to keep missing out.
-neil
