Open side-bar Menu
 Decoding Formal
Dr. Jin Zhang
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.

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: , , , , , , ,

Category: Blog

Leave a Reply

Your email address will not be published. Required fields are marked *



TrueCircuits: IoTPLL

Internet Business Systems © 2019 Internet Business Systems, Inc.
25 North 14th Steet, Suite 710, San Jose, CA 95112
+1 (408) 882-6554 — Contact Us, or visit our other sites:
TechJobsCafe - Technical Jobs and Resumes EDACafe - Electronic Design Automation GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy PolicyAdvertise