Goal posts Aren’t Only for Football – Use Them in Formal Analysis Too!
With both DVCon and the annual Super Bowl championship football game coming up, one can’t help but think of … formal verification!
Seriously: goal posts and scoring drives aren’t just for football – conceptually similar things can be a winning strategy for using formal analysis to penetrate the state space of a large DUT, and drive toward the areas you are seeking to reach. To paraphrase, run a series of formal “goal posting” plays. Here is how it works:
* After so many formally analyzed clock cycles – 10’s, 100’s, or 1000’s depending on the DUT – even the most scalable formal verification engines take longer and longer to compute the next steps of the analysis. The football analogy is when a team can only get so far down the field, and has to concede that it’s better to kick a field goal for 3 points rather than run a risky 4th down play that would waste valuable time, leave them in worse field position, and yield no points at all. Conversely, if you kick enough field goals, each of those 3 pointers begin to add up …
* Translating from football jargon back into formal verification terms: find a cover point which is at a depth of analysis that formal can hit (10’s to low dozens of clock cycles), then use that as a new jumping off point from which to explore deeper into the design. Repeat until you reach the deeply positioned target of interest – Touchdown!
* Referring to the figure above, the intermediate goals (typically specified with COVER statements) are selected to enable successive formal runs to explore deeper into the design to ultimately hit the desired target. With this technique a user can more quickly leap frog from point-to-point and explore deeper into the design than a single formal run could.
This is an effective, time-tested bug hunting technique (especially when you are working to reproduce post-silicon bugs). Indeed, a great real-world case study of this methodology is captured in the 2015 DVCon USA paper, “11.3, Every Cloud – Post-Silicon Bug Spurs Formal Verification Adoption”. In this paper the authors describe how they employed this technique to find the root cause of a corner-case bug in a DDR3 design – a bug that had escaped all previous verification methods.
If this year’s game is like many prior Super Bowls, the outcome will be obvious by half time. Hence, you might as well turn off the TV and download this paper so you’ll be ready to apply this methodology on Monday.
Go Formal, GO!!!
Joe Hupcey III
on behalf of the Questa Formal and CDC team
Comments