Maximize the power of formal
verification to enable innovative SoC
designs and Formal Sign-offTM!
“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:
The king can start at any square except the center. The goal is to determine:
(*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:
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:
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.