Achieving Formal Sign-off
Sponsored by Synopsys
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
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.
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.
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.