Achieving Formal Sign-off: Key Learnings for Trainees and Experts

Formal sign-off is possible with today’s technology and methodology. But to get to formal sign-off takes an understanding of what is possible with formal verification, and an immersion in ongoing practice with formal methods and techniques. Moreover, early experiences with formal can determine later success with formal verification and sign-off. Even with a deep knowledge of a formal verification tool and extensive training from the tool vendor, exponential formal proof complexity often gets in the way of exhaustive coverage. Often what is needed is training in formal verification methodology and formal test planning that includes an exhaustive list of end-to-end checkers, as well as the mastering of formal techniques that help overcome complexity.

In 2015, Oski conducted a seven-week training for a small group of design and verification engineers representing a wide range of experience, under the direction of the company’s formal verification program leader. This company was an existing customer of Oski for formal verification services and, having seen the value of formal first-hand, wished to increase the role of formal in their verification efforts, and to deploy it across a wider range of projects. To accomplish this, the FV program leader was charged with growing the level of formal expertise in the company and the knowledge of the techniques needed to adopt a formal sign-off methodology.

The trainees were already aware of the basics of formal verification and had some experience with the formal tool that was used in the training. The goal of the training was for trainees to learn how to do formal sign-off. The program was based on a series of short lectures, Q&A sessions and a comprehensive set of hands-on labs working with a real design, and started with a review of the fundamentals of formal verification and how to use a formal tool. The example testbench was quite complete, and even included over-constraints that were intentionally introduced to teach proper debug using a step-by-step approach, especially useful to detect cases where only a few legal scenarios are disallowed by the constraints.

There were key learnings for both trainees and Oski instructors. Engineers new to formal often assume that all checkers should achieve an Unbounded Pass, and when the tool reports a Bounded Pass, they run checkers for longer duration, expecting the Unbounded Pass. This is largely because the concept of Required Proof Depth is not intuitive. However, once the students learned this concept, and understood the steps to calculate and validate the Required Proof Depth of the DUT, bounded proofs suddenly became useful.

These engineers, while new to formal verification, were especially creative in coming up with different implementations of checkers and constraints, exposing a range of efficiency in their testbenches. They were also quick to grasp Abstraction Models™ and use them in innovative ways to enable the formal tools to “shortcut” the search space and reach previously unreachable parts of the design. Lastly, it is sometimes easier for people new to design verification in general to learn to use formal techniques more effectively, and engineers who were experts in simulation but new to formal found it harder to let go of controlling input sequences, thereby reducing the benefit of formal.

This Advanced Formal Techniques training presented an opportunity to partner with our customer to optimize their formal efforts, and provided tangible benefits to the company. The success of this program and others like it underscore the larger benefit of this type of training; when formal is deployed in a predictable, measurable and meaningful way, it can be an integral part of the overall verification sign-off process. This particular training was for seven weeks, but key concepts and techniques in one or two areas can be taught in a shorter time frame, such as Oski’s upcoming one-day training on Thursday June 9, at the 2016 Design Automation Conference (DAC) in Austin. More information on how to register, below.

—–

Oski Technology is hosting the Decoding Formal Achieving Formal Sign-off Training Day (link)  Thursday, June 9, from 10 a.m. until 5 p.m. at the Hilton Hotel, Austin. DAC, at the nearby Austin Convention Center, will be held June 5-9. Oski’s event is open to a limited number of attendees.Topics for the 2016 Decoding Formal Achieving Formal Sign-off Training Day include Writing End-to-End Formal Checkers, Dealing with Formal Complexity, Using Formal Coverage, and Putting Theory into Action.  No DAC badge is required for this meeting. The registration fee is $199, including lunch. Coffee and networking is at 10:00 am, and training begins at 10:30 am. The agenda and session abstracts. Space is limited, so please pre-register here, to guarantee a place. Oski will be a DAC exhibitor again this year with a demonstration of Oski Abstraction Models, and how to apply these and other techniques during formal analysis to reach deeper search depth and achieve faster proof, for formal sign-off.

Tags: #53DAC, advanced formal training, formal analysis, formal sign-off, formal verification methodology, HarGovind Singh, Oski Abstraction Models, Oski Technology, Pippa Slayton

Category: Blog

This entry was posted on Monday, May 2nd, 2016 at 4:21 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.