Recap of the 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, Berkeley Math Circle Monthly Contest 8, 2011, proposed and designed by Evan O’Dorney, three-time Putnam Fellow.  Jesse Bingham from Intel submitted the winning entry, as was announced during a presentation at the recent meeting of the Decoding Formal Club in Santa Clara, CA on February 29, 2016. This was an opportunity to promote the adoption of formal verification across the semiconductor industry, and share formal techniques by showing how they might be used to solve a fun formal puzzle.

Participants were presented with one King on a 5 x 5 chessboard with 25 squares, constraints for at most 3 total moves in any single direction, and two goals, A and B. Goal A is to prove that the King, starting from any square except the center square, can visit all 25 squares, while obeying the constraints. Goal B is to prove that the King, starting from any square except the center square, can visit all squares except the center square while obeying the constraints.

Chessboard Challenge formal puzzler

Goal A is easily eliminated as an achievable goal, even without the use of formal tools. Given the constraints, every move has an inverse move, which means the 24th move will always return to the starting square. Since the constraints imply a maximum of 24 moves, each square can only be visited once if all 25 squares are visited. So in 24 moves the King is back at its starting position, having visited that square twice, and cannot have visited all 25 squares. This is proof that goal A is not achievable. Goal B on the other hand, is attainable, but offers a significant challenge for formal users. For goal B, the King must visit all the squares, except the center square. The challenge lies in the proof convergence for the formal tools.

A naïve solution using formal verification exists for both goals, but in each case, it is hard for formal tools to prove. For goal A, for example, a formal verification solution will not converge, even after 12 hours of a formal run. This is a problem that presents itself for both goals A and B. Formal tools can solve it, but with difficulty, and varying degrees of success. The reason is formal complexity. In both cases, the proof encounters an exponential curve in time-to-converge, which is difficult to conquer.

The variety of techniques submitted by participants presented a number of worthy solutions, with varying degrees of success. In all cases, formal techniques were needed to help the tool go faster, and fight formal complexity.

Disabling proof at lower depths

Disabling the proof at lower depths was a popular choice of technique. This is actually a very useful technique commonly used in formal verification in the real world, and it proved to be the most effective technique for goal B.

In this technique, the formal search is started from a deep state, i.e., the checker remains disabled until all 24 moves are exhausted. A speedup of 40x is achieved in getting a witness for the King to visit all the squares except the center.

Assume-Guarantee was the technique used by our winner. Assume-Guarantee is a method whereby some helper checkers are coded to speed up proof convergence. These helper checkers are then converted to assumptions for proving the main checkers. In this case, the moves are symmetric and equal; therefore the King’s aggregate displacement after 24 moves will be zero. One helper checker is that the King must return to its starting square after 24 moves. This helper checker is proved, converted to a constraint; and then it becomes possible to prove the “harder to prove” main checker very quickly.

Assume-Guarantee

Armed with seven other helper checkers, using the Assume-Guarantee, Bingham proved that it’s impossible for the King to visit all the squares, and helped the formal tool to reach its goal 30x faster than a solution without this technique. The use of this technique requires a good understanding of the puzzle, was very powerful and distinguished the winning solution from all the others.

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”

Jesse Bingham from Intel, winner of the Oski 2016 Formal Puzzler Chessboard Challenge, Feb. 29, 2015.

Tags: "Decoding Formal" Club, chessboard challenge, formal analysis, formal sign-off, formal verification, Oski Technology, Pippa Slayton, Vigyan Singhal

Category: Blog

This entry was posted on Thursday, March 24th, 2016 at 10:53 am. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.