2016 Oski Formal Puzzler - Chessboard Challenge Video

In December 2015, Oski challenged formal users to build the fastest testbench to solve our Oski Formal Puzzler - the Chessboard Challenge! This puzzle is from the Berkeley Math Circle Monthly Contest 8, 2011, and was proposed and designed by 3-time Putnam Fellow, Evan O’Dorney. The winning entry was submitted by Jesse Bingham from Intel, and announced during a presentation at the recent meeting of the Decoding Formal Club, held in Santa Clara, CA on February 29, 2016. Our goal was to share formal techniques through a formal puzzle, and promote the adoption of formal verification across the semiconductor industry. In many ways the challenge is analogous to real world combinatorial problems with schedulers, virtual mapping arrays and free lists, while the approach, techniques and mindset required to solve this type of problem is strongly relevant to the verification of structures in real designs. More about Oski Technology at www.oskitechnology.com