Dr. Jin Zhang
Jin Zhang has over 15 years of experience working in EDA, driving the effort of bringing new products and services to market. At Oski Technology, she is responsible for Oski’s overall marketing strategy as well as business development in Asia Pacific. Prior to that, she was the General Manager at … More »
Oski Holiday Challenge – a Fun Formal Puzzler
December 9th, 2015 by Dr. Jin Zhang
“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:
The king can start at any square. 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, 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 email@example.com. We’ll post updates: #formalpuzzler on twitter @oskitech.