Other popular techniques that proved to be helpful in solving this puzzle included Case-Splitting, where checkers are split into multiple checkers on the basis of starting square of the King; Symmetry Identification, which allows the number of starting squares of the King for which the goal must be proven to be reduced to only those that are topologically unique. These and others were discussed in more detail at the Decoding Formal event, and in a short video recap of the Chessboard Challenge (link).
One solution even used simulation with dynamic search, and was partially successful with goal B, using a particular seed of the random generator. The simulation solution underscores the weaknesses of simulation vs. formal, especially for this kind of problem, and quantifies the advantage of using formal over simulation. As formal search is exhaustive, it is possible to achieve targets like goal A and hit corner-cases like goal B. Simulation search, on the other hand, is non-exhaustive and so is not suitable for targets like goal A, as it cannot guarantee that it’s impossible to achieve goal A, even after millions of runs. Also, simulation is likely to miss low probability corner cases like goal B.
In general, the solutions tended to rely heavily on tool features, which was surprising. Too much reliance on tool features takes away the creative possibilities in applying formal and makes it hard to port the environment to different tools. Common mistakes included introducing accidental over-constraints, causing vacuous proofs. Vacuous proofs are generally very quick to converge and result in missed bugs. Therefore, keeping a check on “too good to believe” fast proofs, is always recommended.
Overall, the general enthusiasm for the puzzle was impressive; as mentioned above, even the simulation engineers had a go at solving it. Research students used open-source tools like NuSMV and SPIN to produce the solution. As mentioned above, some participants applied bug hunting techniques by disabling checkers at lower depths, some narrowed down the formal search by identifying symmetry in the start position of the King.
In many ways this challenge is analogous to real world combinatorial problems with schedulers, virtual mapping arrays and free lists, which is perhaps why it attracted interest from participants across the industry. Engineers from large semiconductor companies, IP vendors, PhD students and tool vendors offered different approaches in a number of different languages including SystemVerilog, SMV, Python.
While general levels of interest were strong, and several participants submitted more than one solution, the approach, techniques and mindset required is strongly relevant to the verification of structures in real designs, and offered formal users everywhere an opportunity to sharpen their strategies for the real world application of formal verification.
Link to video: Video recap: 2016 Oski Formal Puzzler – “Chessboard Challenge”