Oski Holiday Challenge – a Fun Formal Puzzler

“Jingle Bells”, “Silent Night”, “We Wish You a Merry Christmas”… It has been several weeks since my youngest daughter started practicing for her upcoming violin concert. I grew up in China and missed out on the fun of Christmas festivities and holiday music. Now that we live in the United States and have had the full holiday experience, I learned that Santa Claus comes to town – two months early!

With the holiday season upon us and reflecting on the past year, 2015 has been a very busy and rewarding time for Oski. The hard work put in by each of our colleagues is paying off – with the growing adoption of formal technology and formal sign-off methodology at many companies across the globe. Formal Verification is finally coming to town!

We would like to thank colleagues, customers, partners, friends, families, and everyone in the industry for their support in helping us succeed in our mission – maximizing the power of formal technology to enable innovative SoC designs and formal sign-off. More than in any time in the history of Oski and the semiconductor industry, formal has gained its rightful place in the design and verification flow. 2016 will be an even better year and we will continue our efforts in contributing to that history.

We at Oski like a good challenge, so what better gift to leave with you for the holidays, than a fun formal puzzler* – the Oski Holiday Chessboard Challenge!

Here it is –

On a 5 × 5 chessboard, a king moves according to the following rules:

• It can move one square at a time, horizontally, vertically, or diagonally (these are the usual moves of the king in chess).
• It can move in each of the eight allowable directions at most three times in its entire route.

The king can start at any square. The goal is to determine:

• Whether the king can visit every square.
• Whether the king can visit every square except the center.

(*This puzzle is from Berkeley Math Circle Monthly Contest 8, 2011, and was proposed by Evan O’Dorney.)

You can try to solve the problem with paper and pencil. But for those of you familiar with running formal verification tools, we challenge you to solve it with your favorite formal verification (model checking) tool:

1. Write a Verilog module to implement the moves for the chessboard – in every clock cycle the king makes one move and the state of the chessboard changes. The specific move is dictated by an input to the module.
2. Allow the reset state to be any of the 24 squares except the center.
3. Add constraint(s) to enforce that there are no more than three moves in any of the eight directions during the entire route.
4. Implement two checkers that fire if the final conditions (a) or (b) are achieved, respectively.
5. Run the model checker to see if you can get a proof, failure or a bounded proof for the checkers!

For further credit and to make the problem easier for the formal tools, try using reductions based on symmetry, or creating simpler checkers and using assume-guarantee, or any of your favorite formal verification techniques, including abstractions. For example:

• You could over-constrain the reset state to be one of the 6 squares in top-left quadrant of the chessboard, exploiting the fact that the board and the moves are symmetric, and that means the correctness of the checkers will not be violated by making this reduction.
• You could add a checker that at any state, the number of unvisited squares must not exceed the number of moves left (a simplification of a more complex pruning idea due to Joe Trapasso of NVIDIA). This smaller checker might be easier to prove, and can be assumed to make the proof for (a) or (b) easier.

Send us your paper-and-pencil solutions, or your Verilog programs, for the above. Use any techniques to simplify the problem. We will run your program in formal tools and see whose Verilog testbench runs the fastest. The winner will be announced at our next Decoding Formal Club meeting, where we will also discuss why certain techniques work better than others. In addition, we will discuss how this chessboard problem related to structures often seen in hardware Verilog designs, like controllers managing linked lists, arrays, FIFOs, sets, tags, etc.

Please join us in taking our fun holiday challenge! Send your challenge solution to the email below. Three winners and the first 5 entries will receive special prizes, so don’t delay!

Email your Oski Holiday Chessboard Challenge solution to formalpuzzle@oskitech.com. We’ll post updates: #formalpuzzler on twitter @oskitech.

Happy Holidays!!

Tags: "Decoding Formal" Club, #formalpuzzler, chessboard challenge, formal puzzler, model checking, Oski Holiday Challenge, Oski Holiday Chessboard Challenge, Oski Technology, verilog

Category: Blog

This entry was posted on Wednesday, December 9th, 2015 at 6:28 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.