Get email delivery of the Cadence blog featured here
Need to make a case for using formal in your organization? ARM’s Austin team now has two years under its belt using formal verification. Vikram Khosa, a staff design engineer on the team, has a few tips and tricks to share from the experience so far.
Formal is critical to ARM because the methodology provides exhaustive analysis that helps find corner-case bugs and, ultimately, leads to better quality designs, said Khosa. By applying formal during RTL coding, a verification team can catch bugs early on with low debug cost and a shorter project cycle, he noted. Part of a pitch to management, he said, is to set expectations by communicating what formal coverage is—an approximation, like any simulation metric, albeit a strong and comprehensive one.
ARM’s Austin team has built a full-time formal team and plans a full-scale formal deployment for a next-generation CPU. Their methodology involves:
ARM's Vikram Khosa discussed formal verification at this year's Design Automation Conference.
Obviously, having a good set of metrics will be a critical point of justification for formal. According to Khosa, an ideal metric would answer how much of a design has been verified and how much of it has not. To indicate signoff, an ideal metric would measure whether assertions completely specify correct design behavior and whether constraints specify at least the maximal legal environment in which the design is expected to correctly operate.
Other important metrics that feed into the formal coverage number, to help measure progress and guide further development, include:
Now, how does formal coverage signal signoff readiness? According to Khosa, these are some of the key questions to answer: Is the list of planned checkers complete? Are there any unintentional over-constraints? Have the implemented checkers reached sufficient proof depth? If there are coverage holes, these holes would point to things like missing checks, unreachable areas due to over-constraints, or areas of the design that are insufficient for exploration for existing checks.
At ARM Austin, formal coverage is now being used comprehensively on a next-generation CPU project. Said Khosa, “It is very key to tracking our progress and also for reporting a set of numbers to management.” As for reporting to management, Khosa and his team focus their weekly reports on three key metrics:
From his experience so far, Khosa also offered some ideas on ways to improve or extend formal coverage:
“Formal coverage is a strong metric—it’s fairly comprehensive and it’s a single number, so it’s easy to track and report,” said Khosa. “However, it’s not perfect. But it is a good approximation of progress you’ve made, what’s left to do, and how close you are to being done.”
Khosa presented this discussion at the Cadence Theater at this summer’s Design Automation Conference in San Francisco. You can view his slides, plus presentations from about 50 other customers, online. Khosa’s talk, called “One Metric to Rule Them All? Tracking Progress on Formal Testbenches,” is Session #47 at the 5:00pm slot on Wednesday, June 10.
- Imagination Dispels 10 Myths About Formal Verification
- Broadcom Design and Verification Engineer: "My First 100 Days in Formal Land"