Decoding Formal 
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 » Unbroken, 73 Bugs Captured!June 19th, 2015 by Dr. Jin Zhang
The story of Louis Zamperini, as told by Laura Hillenbrand in “Unbroken: A World War II Story of Survival, Resilience, and Redemption”, is a great testimony of the strength of human spirit. Going through unimaginable catastrophes, including drifting 47 days on the open sea with leaping sharks, thirst, starvation, and machine gun attack from a bomber plane, as well as enduring 3 years under severe and brutal conditions as a POW in Japan, Zamperini emerged unbroken with grace, humanity and love. This is such an inspiring story that when I thought about writing about Oski DAC 2015 “Break the Testbench” Challenge results, the word “unbroken” came to mind. While this is no comparison in its scale to the story of Zamperini, the word “unbroken” succinctly summarizes the challenge result.
Over the three days in Oski DAC booth, we invited visitors to insert bugs into a multicast crossbar design, to see if the bug could be detected by our custom-built End-to-End formal testbench that included five End-to-End checkers. The challenge generated a great deal of interest. While some visitors simply and quickly introduced random bugs, there were many others who carefully examined the design, thoughtfully inserted bugs and debugged the counterexamples provided by the formal run, to make sure the reported failure was indeed due to the bug they inserted. Many people took to the challenge to try to break our formal testbench, including Raik Brinkmann, OneSpin CEO, formal R&D folks from Cadence, Mentor and Synopsys, as well as many formal experts from leading companies such as ARM, Broadcom, Cisco, Huawei, Imagination, NVIDIA, Qualcomm and Texas Instruments. A total of 73 functional bugs were inserted, ranging from modifications of the RTL code related to the arbitration scheme, connectivity, grant generating, mask generation logic, incorrect operators and modified parameters. Some examples of the changes are shown in the table below.
It was no surprise to us that all functional bugs introduced were indeed caught by the End-to-End formal testbench, proving the concept that the End-to-End formal testbench is complete and can be used for formal sign-off. For comparison, we also embedded 144 internal assertions in the RTL code to see how many of these bugs can be caught by internal assertions. As shown in the figure below, 22 bugs were caught by these assertions. While we highly recommend designers embedding RTL assertions to catch design bugs, it is clear from this experiment that Assertion-Based-Verification (ABV) cannot catch all design bugs and therefore should not be used for sign-off.
With the challenge results, we can declare our End-to-End formal testbench is indeed unbroken, having captured 100% of the bugs, a total of 73 bugs in all. Along with the formal testbench we built, we also introduced users to techniques such as symbolic variables and the use of Wolper coloring technique to check for data consistency. If you didn’t attend DAC but want to learn more about the End-to-End testbench and how to build one, and even try out the “unbroken” version of the formal testbench for our multicast crossbar design, please visit our website at www.oskitechnology.com and fill out our “Contact us” form. It was a fun DAC. Our formal testbench emerged intact after 73 bug insertion attempts. Thanks to Synopsys for allowing us to use VC Formal. If you want a verification flow where you can guarantee no bug is left behind, consider End-to-End formal. Tags: "Decoding Formal" Club, #ARM, formal sign-off, Oski Technology, Vigyan Singhal Category: Blog |
|
|
|||||
|
|
|||||
|
|||||
