Decoding Formal Club Unlocks Some Mysteries

Last May, I published two blog posts on the presentations made at a “Decoding Formal Club” event hosted by the smart folks from Oski Technology at the Computer History Museum in Mountain View. With everything else going on, I didn’t manage to make it to another of their regular meetings until last week. The first event of 2015 was very interesting, so again I’m returning to the popular topic of formal analysis and playing reporter. The line between media and blogging is rather thin these days anyway.

This edition of Decoding Formal featured three talks, one an end-user case study and the other two  instructional in nature from well-known formal experts. I found all three worthwhile and will do my best to communicate some of the main points made. I also have to mention the final presentation, more a performance than a talk, by the inimitable and irrepressible Clifford Stoll. Lately he’s been manufacturing and selling Klein bottles, which you may remember from a geometry teacher trying to mess with your mind.

The case study, by Ross Weber, described “Formal Usage in ARM Austin CPU Group.” He described how a group of five experts used formal analysis to target more than ten units in a next-generation ARM design. They initially verified the properties (assertions) on the interfaces between all pairs of connected units. Ross made the excellent point that the unit designers needed to be involved, and were required to document all interfaces with either properties or comments that the formal team could convert to properties.

After running automated formal checks as well, the team chose a subset of the units most suitable for comprehensive formal analysis. The high-level properties checked end-to-end unit behavior, ordering rules, coherence, deadlock/livelock, and other important design attributes. It was interesting to me that even this experienced team did not have a goal, at least as this stage of deployment, for formal to replace any particular simulations. Perhaps that will happen as formal takes an even deeper role.

Oski CEO Vigyan Singhal gave a well-organized talk on “Managing Constraints for Formal Sign-Off.” In formal analysis, as in graph-based SoC verification, constraints are essential. They ensure that only legal state space is explored and offer the verification team ways to fine-tune what is being verified and where the focus should be. Vigyan did an excellent job of describing two all-too-common situations when running formal: under-constraining and over-constraining.

Too few constraints means that illegal state space is being considered. This can reduce the likelihood of a proof for a property or generate apparent property failures that that would not occur with more accurate constraints. Too many constraints is even worse, since it can result in “proofs” that are not accurate since not all legal state space was considered. Vigyan offered several ways to detect when these two situations occur and how to resolve them.

The other instructional talk was “Liveness vs. Safety – A Practical Viewpoint” from Jon Michelson of NVIDIA. A liveness property is one that is unbounded in time, for example, that a request must eventually be followed by a grant. These are notoriously difficult for formal analysis to prove. One approach is to convert to a safety property, for example, that a request will be followed by a grant within 100 cycles. This is a compromise that may not reflect the actual intended behavior of the design being verified.

An alternative is to use abstractions to simplify parts of the design in order to make a liveness proof more tractable. Jon walked through some possible abstractions, including tying the refresh signal inactive and reducing some four-bit signal groups to a single bit each. He went through several examples of both liveness and safety properties, showing the actual runtime of each on a commercial formal tool. He stepped through the examples carefully, so that those who weren’t formal experts could learn from his talk.

I though that both Vigyan and Jon did a really good job of what the event promised: “decoding” some of the secrets and unlocking some of the mysteries of formal analysis. I really like the format of these events and plan to attend whenever I can. Beyond that, I’m wondering whether the time might be right for a similar event devoted to portable stimulus and graph-based verification. I can imagine how the right talks could demystify some aspects of graphs the same way that last week’s event did for formal constraints, properties, and abstractions.

Would you be interested in attending a half-day event sponsored by Breker? What topics would you like to see covered? Is there another company who should co-sponsor with us? Please let me know your thoughts with a comment to this post. Thank you in advance!

Tom A.

The truth is out there … sometimes it’s in a blog.

Tags: Accellera, Breker, cache coherency, constraints, EDA, formal, functional verification, graph-based verification, oski, portable stimulus, properties, scenario model, SoC verification, standards, Trek, TrekApp, TrekSoC

This entry was posted on Tuesday, March 10th, 2015 at 10:09 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.