Decoding Formal Club Meeting – Completeness of End-to-End Formal (Video)
In this latest Decoding Formal Club video, Oski COO Dave Parry talks about the high stakes on SoC designs, shrinking design cycles and the importance of higher levels of effectiveness and efficiency with verification, and Prashant Aggarwal delivers a presentation on how to ensure the completeness of End-to-End formal, for formal sign-off.
Decoding Formal “Break the Testbench” Challenge* at DAC 2015
Oski Technology DAC 2015 “Break the Testbench” Challenge
This year at DAC, Oski hosted the 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 100% of these bugs were 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, visitors to the Oski DAC 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.
* “Break the Testbench” Challenge supported by Synopsys VC Formal