Decoding Formal Events at DAC 2015
Oski Technology “Break the Testbench” Challenge* DAC 2015
This year at DAC, Oski hosted the highly successful “Break the Testbench” Challenge*, proving that Oski’s End-to-End formal testbench is complete, and can be used for formal sign-off. 73 functional bugs were inserted, and every bug was caught, proving the concept that the End-to-End testbench is complete, and that formal verification can be used for formal sign-off.
Over three days at DAC, visitors to the Oski booth were invited to try to break the End-to-End formal testbench by inserting functional bugs into a multicast design. We used the special formal verification techniques, such as the Symbolic Variables and the Wolper Coloring technique, to implement five End-to-End checkers to verify the correctness of the arbitration scheme and ensure consistency and forward progress of data through the design. For comparison, we embedded 144 internal assertions. However, only 22 of the 73 bugs were caught by these internal assertions, suggesting that assertion based verification cannot catch all design bugs, and should not be used for formal sign-off.
See Oski’s DAC 2015 “Break the Testbench” video here: https://oskitech-2.wistia.com/medias/4o19z1zi6t
* “Break the Testbench” Challenge supported by Synopsys VC Formal