Promoting Formal Education: Oski Shares Experiences at FMCAD 2013

Although Oski Technology is first and foremost a formal verification service company, making effective use of formal tools and promoting education around the power of formal technology has always been at the core of our business. Since Oski was founded in 2005, we have engaged in many activities to help increase the adoption of formal in the industry:

1. Our formal verification service offering includes training for customers on End-to-End formal verification and Oski Formal Sign-off Methodology so they can leverage formal effectively and across all design projects.

2. We produced the “Decoding Formal” series of video tutorials on formal verification covering a broad array of topics and interests, and made the series available on the Oski website.

3. We recently launched the Decoding Formal Club, a forum to foster knowledge-sharing and networking among formal enthusiasts so as to build critical mass of formal experts in the industry.

4. The Oski 72-hour Live Verification Challenge hosted at DAC 2012 was an impressive demonstration of the power of End-to-End formal verification over a very short period.

5. Finally, Oski is the sponsor of the Deep Bounds Award at the annual Hardware Model Checking Competition (HWMCC) affiliated with FMCAD (Formal Methods in Computer Aided Design). This award recognizes outstanding technological achievement for solving the most useful End-to-End formal verification problems.

Oski Deep Bounds Award winner Niklas Sörensson and Vigyan Singhal, Oski Technology

FMCAD 2013

FMCAD 2013 Panel Discussion: “Teaching Formal Methods: Needs, Challenges, Experiences and Opportunities”

FMCAD 2013 held in Portland, OR was well attended this year, and Oski was invited to participate in a panel discussion with participants from industry and academia. The goal of the panel discussion – “Teaching Formal Methods: Needs, Challenges, Experiences and Opportunities” – was to share experiences and insights about the most effective ways to teach formal methods and improve formal education so as to enhance the adoption of formal in the industry.

During the FMCAD panel discussion Oski shared the following perspectives and insights. Some that apply to educating engineers on how to leverage formal can also be applied to building successful formal teams and developing formal expertise.

1. Better one full-time user of formal than several part-time users – When companies begin to deploy formal verification for the first time, they sometimes start with a few people doing part-time formal verification work. In our experience, one full-time dedicated formal engineer delivers much more than two or three part-time formal engineers. Compared to simulation, formal is an orthogonal technology, and the user really needs to be immersed in it to gain the necessary expertise.

2. Success is about more than bugs – Most companies deploy formal in “bug-hunting” mode and measure the success of formal by tracking the bugs it finds. In contrast, Oski is teaching customers to deploy formal for sign-off, i.e. for the blocks verified with formal, no simulation testbench needs to be developed; formal verification guarantees complete functional correctness of the design through end-to-end checkers. The Formal Sign-off approach truly leverages the power of formal in the verification flow. While bug hunting is valuable, it doesn’t help to develop a “sign-off-worthy” formal methodology. Once customers see success in using the Formal Sign-off Methodology, they tend to want to deploy formal on more projects. We have to aim high to be successful and Formal Sign-off Methodology should be a must-have in the verification flow, so formal engineers are held responsible for design quality and also receive well-deserved credit for it.

3. Relate formal to simulation plans – If formal verification is mostly used as a bug-hunting solution, the synergy it has with simulation is rarely leveraged. The downside is the application of formal becomes an isolated event and it doesn’t lead to the most successful usage of formal. In fact, formal and simulation are complementary; both are needed and they also support one another in application. A complete verification methodology needs to leverage both technologies to where is most appropriate for each, and to each its fullest potential.

4. Learn how to overcome the complexity barrier – We all know formal verification is hard and people often run into the complexity barrier with state space explosion problem. While formal technology is improving every year, fighting exponential run-times is usually futile. When formal tools fail to give conclusive results within a few hours, running the tools overnight (or over the weekend) usually does not help. When they run into such inconclusive results, formal users are discouraged and often give up, hindering formal adoption. In reality, much can be done to overcome the complexity barrier. Users need to quantify the benefits of bounded proofs, and apply the appropriate techniques when proof bounds are not good enough.

5. Focus on solving the right problem – We all prefer easy-to-use or automated solutions. However to make the best use of formal technology, manual work is necessary. We need to change the problem by decomposing the proofs and building Abstraction Models. With such techniques, proofs can often run millions of times faster, and formal can be used for sign-off. In our experience with hiring our own team members, having past verification experience (with formal or not) is not critical. What is critical is a willingness to use analytical skills to find creative solutions. We hire people who are good problem-solvers rather than people who prefer tools that are completely automated.

In summary, Oski’s formula for educating engineers on how to leverage formal, building successful formal teams and developing formal expertise: Hire problem-solvers to be dedicated, full-time users of formal who can relate formal to simulation plans, explore bounded proofs, and use formal to its fullest potential by deploying formal for sign-off.

Category: Blog

This entry was posted on Monday, November 25th, 2013 at 6:28 am. 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.