Oski Holiday Challenge: Fun Formal Puzzler Entries Due by Jan. 31!
“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 2016 Oski Formal Puzzler 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 except the center. 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:
- 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.
- Allow the reset state to be any of the 24 squares except the center.
- Add constraint(s) to enforce that there are no more than three moves in any of the eight directions during the entire route.
- Implement two checkers that fire if the final conditions (a) or (b) are achieved, respectively.
- 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 Monday, Feb. 29 at the Parcel 104 restaurant at the Santa Clara Marriott, where we will also discuss why certain techniques work better than others. (Registration is required. Pre-register, here). 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 Formal Puzzler Chessboard Challenge! Send your Chessboard Challenge solution to the email below. Three winners and the first 5 entries will receive special prizes, so don’t delay! We’ll post #formalpuzzler on twitter @oskitech.
Email your 2016 Oski Formal Puzzler Chessboard Challenge solution to firstname.lastname@example.org. We’ll post updates: #formalpuzzler on twitter @oskitech.