DAC Decoding Formal Training Day
Achieving Formal Sign-off
Sponsored by Synopsys
Austin, TX | Hilton Hotel 
Thursday, June 9, 10:00 AM – 5:00 PM 

Join Oski for an all-day training session “Achieving Formal Sign-off” at DAC on Thursday June 9, 2016. Register here.  More about other Oski activities, talks and presentations at DAC, is here.

Formal sign-off is possible today, and takes knowledge of formal methods and techniques, and immersion in ongoing practice. This Decoding Formal training day is hosted by Oski Technology, takes place at the Hilton Hotel, #53DAC HQ, and will discuss key components of formal sign-off methodology, with the goal of Formal Sign-off.  Detailed session descriptions are below. Fee $199. No DAC badge is required.  Purchase tickets here.

Agenda: “Achieving Formal Sign-off” Decoding Formal DAC Training
10:00 AM   Coffee and Networking
10:30 AM   Writing End-to-End Formal Checkers
           Lunch and Networking
           Dealing with Formal Complexity
           Using Formal Coverage
           Coffee Break
           Putting Theory into Action
5:00 PM    Wrap Up

Event:  “Achieving Formal Sign-off” Decoding Formal DAC Training day
Date: Thursday June 9
Time: 10:00 am to 5:00 pm
Venue: Hilton Hotel, Austin, TX 
Fee: $199. Lunch included.

Thanks to Synopsys for sponsoring the Decoding Formal DAC Training Day.

Session 1: Writing End-to-End Formal Checkers

Formal verification can replace unit-level RTL simulation for designs that are the most difficult to verify otherwise due to complex corner-cases.  Such a replacement requires the design of a set of end-to-end checkers, which needs to be both complete – every possible RTL bug should be caught by at least one checker – and efficient – each checker should be proven to a sufficient depth in a reasonable amount of time.  This lecture covers the art of designing the end-to-end checkers and associated reference models that comprise a formal testbench, interpreting the results of those checkers, and utilizing various techniques to optimize them so they reach greater proof depths.  The discussion of end-to-end checkers leads into the next two topics: overcoming formal complexity which can prevent the checkers from reaching required proof depth, and measuring the completeness of the set of checkers via formal coverage.

Session 2: Dealing with Formal Complexity 
Managing proof complexity is central to being successful with formal.  Because exhaustive proofs are computationally hard, especially for end-to-end checkers, users must learn to get the most out of bounded proofs.  This lecture begins by explaining what gives rise to formal complexity issues; then goes on to describe effective strategies for reducing and resolving those issues, including the use of over-constraints and under-constraints, creation of Abstraction Models(TM), and various other techniques such as Wolper coloring and floating pulses.  It shows how users can always implement some strategy to achieve convergence to a sufficient depth for almost all designer-sized units.  It closes with a brief description of how one can use a combination of architectural and RTL formal verification to formally verify large, complex sub-systems of an SoC.
Session 3: Using Formal Coverage 
Coverage has been used effectively for decades in simulation to measure the progress and completeness of simulation work.  Measuring these is even more important for successful adoption of formal since there is a large variance in the scope of checkers written by different users coupled with the often intractable complexity of formal proofs.  Formal coverage, a very recent advance in tools, is effective at quantifying the adequacy of the set of checkers, the constraints and the achieved proof depths.  This lecture introduces the concept of formal sign-off, and describes how formal coverage can help achieve it.  It discusses the different types of formal coverage, their respective strengths and weaknesses, how to interpret and use their results, and how those results can be used in a formal sign-off process.
Session 4: Putting Theory into Action
This session drives home key learnings from the three earlier lectures by showing their application to a real-world example problem.  It begins by describing a sample target design for end-to-end formal verification, then walks through creation of checkers and constraints for the design, reduction of complexity in its formal testbench and the formal results that are consequently achieved, and use of formal coverage measurement in combination with those results to determine that the formal verification is “complete”.  The information is presented as a combination of static slides and live demonstration.
Link to register for the “Achieving Formal Sign-off” all day training.