In December 2015, Oski challenged formal users to solve a chessboard problem. This was an opportunity to show how nifty formal techniques might be used to solve a fun puzzle. Design verification engineers from a variety of semiconductor companies and research labs participated in the contest. The techniques submitted by participants presented a number of worthy solutions, with varying degrees of success. In all cases, formal techniques were needed fight formal complexity. In this session we describe the puzzle, and some of the techniques, all of which are relevant to real-world ASIC designs. Techniques included case-splitting, symmetry reduction, assume-guarantee and disabling lower proof depths. We will also describe the winning solution.
