Preparing for Another Challenge at DAC: Break the Testbench!

You may remember the Oski Technology Live Verification Challenge in 2012, where during the 72 hours of DAC, Oski verification engineer Chirag Agarwal formally verified a well-simulated design from NVIDIA, sight unseen, live and on camera, and found 4 corner case bugs. The challenge results exceeded everyone’s expectations, and inspired other companies to do more with formal in their verification flow. See the Live Oski Verification Challenge, and a blog recap and six-minute video, here.

This event reflected the extremely high level of confidence we place in formal, to find corner case bugs under tight schedule constraints. End-to-End Formal is a new concept. Can it in fact catch all design bugs, and so be useful for sign-off? This year we are hosting the Oski “Break the Testbench” live challenge at DAC to prove formal can be used for sign-off, and we are inviting you to try it for yourself, and win a prize.

Here’s how the 2015 DAC challenge works. Visit the Oski “Break the Testbench” kiosk at DAC, booth #1215, and try to insert functional RTL bugs that break our End-to-End formal testbench for an 8×8 multicast design. The client can send requests to many targets (multicast), and an arbiter is used to decide which client’s request gets forwarded to the target, based on certain priority and arbitration scheme. Kick off the formal run, and see how Formal Sign-off works as your intentional bugs are caught live, with our End-to-End formal testbench. Our scoreboard will display the challenge results as they come in!

The design has 312 flops and about 1000 lines of RTL code, and is intentionally small to allow for faster tool runtime on the showroom floor, and quicker turnaround on the challenge results. We are using VC Formal. The formal testbench contains 5 End-to-End Checkers, 11 constraints, a total of 500 lines of testbench code, written in SV and SVA.

Before you take the challenge, our engineers will show you how to use symbolic variables to write End-to-End Checkers, and how to apply the Wolper Coloring technique to catch drop, reorder or duplicate data. This technique is especially useful in formally verifying data-transport designs.

Participating in this year’s Oski “Break the Testbench” challenge at DAC is a fun way to learn about and apply End-to-End formal, plus you’ll have an opportunity to win a paid registration for the one-day Decoding Formal Training “Achieving Formal Sign-off” on Thursday June 11, valued at $199. Oski is also hosting daily Decoding Formal lunch lectures at noon, and customer lectures at 3 PM at Oski booth #1215; pre-register for lunch lectures here, as space is limited. Please visit our 2015 “Break the Testbench” kiosk at DAC, and enjoy the fun of breaking the formal testbench!

Thanks to Synopsys for co-sponsoring the 2015 Oski “Break the Testbench” challenge at DAC. We hope to see you there.

Update: Video coverage of the Oski 2015 “Break the Testbench” Challenge (link) 

Tags: "Decoding Formal" Club, #52DAC, 2012 Oski Challenge, 2015 "Break the Testbench" Challenge, formal sign-off, Oski "Break the Testbench" Challenge 2015 DAC, Oski Live Verification Challenge, Oski Technology

Category: Blog

This entry was posted on Monday, May 18th, 2015 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.