Dr. Jin Zhang
Jin Zhang has over 15 years of experience working in EDA, driving the effort of bringing new products and services to market. At Oski Technology, she is responsible for Oski’s overall marketing strategy as well as business development in Asia Pacific. Prior to that, she was the General Manager at … More »
Preparing for Another Challenge at DAC: Break the Testbench!
May 18th, 2015 by Dr. Jin Zhang
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.
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.
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