Asterix In The Land Of Sudoku: The Fast, The Elegant, And The Popular Formal Solvers

It has become a time-honored tradition for OneSpin to pose a holiday puzzle challenge to engineers everywhere. Last year, we asked you to solve the famous Einstein riddle using assertions and a formal tool: It was a great success. For the 2017–18 holiday season, we asked you to solve the hardest Sudoku in the world and prove that the solution is unique. We are delighted that even more enthusiastic engineers have shared their expertise and submitted a multitude of neat and fast solutions.

To check out the OneSpin Holiday Puzzle, click here.

We planned to award three prizes this year:

• The Magic Carpet for the solution with the shortest runtime
• The Golden Sickle for the most elegant solution
• The Laurel Wreath for the most popular solution, based on your votes

In case you are not a fan of Asterix, the wildly popular comic series from France, these names are inspired by three episodes of the famous adventures of the indomitable Gauls. In our slightly distorted interpretation, Asterix and his friends use a formal potion that gives them superhuman strength to resist the occupation of a bunch of sneaky bugs.

Solving puzzles is fun and, as you might guess, making sure that you enjoy the contest is our top priority. It also sharpens our logical thinking skills, and being able to review a range of high-quality solutions to the same problem is a rare, incredibly valuable learning opportunity, particularly when one has had a go at the puzzle beforehand.

Writing a Sudoku solver using RTL code and assertions is not a hugely challenging task for seasoned engineers, but it still requires a significant amount of thinking and decision-making. I had a go at it myself and am sure I am not the only one who double-checked that the solution was correct. I went through a few iterations in an attempt to come up with more reusable and readable code.

A screen shot of OneSpin 360 DV-Verify shows the solution to the Sudoku challenge.

Besides specific targets you may have, coding style is influenced by established best practices and personal preferences. The first thing to choose is the language. Most submissions came from Europe and North America and more than 80% used SystemVerilog for both RTL code and assertions. We also received submissions using VHDL, and a few using PSL or ITL for assertions. ITL stands for Interval Language and is OneSpin’s proprietary assertion language.

Another choice that has a significant impact on coding style is how much of the solution is implemented in auxiliary modelling RTL code, and how much is coded directly into assertions and assumptions. Some engineers prefer to write simple properties and shift complexity into modelling RTL.

Our 2017–18 Holiday Puzzle asked engineers to prove that the given Sudoku had only one solution. It is worth noting that, while a simulator with a constraint solver can be used to find a valid solution, only a formal tool can prove quickly and easily that the solution is unique. Formal tools are exhaustive in nature, their key differentiator over simulators.

Having to prove the solution’s uniqueness also afforded us the chance to observe different coding choices. Some of you opted for a combinational approach, based on instantiating the core solver twice and proving that both instances had to produce the same solutions. Others went for a sequential approach, based on proving that a single solver would always produce the same solution over time.

Some participants took on the runtime challenge and gave this goal the highest priority. Coding choices have a huge impact on runtime: Some solutions need more than 10 seconds of CPU time while others, including the Magic Carpet, take less than 0.1 seconds.

Here are the winners:

• Phil Barker from Infineon wins the Laurel Wreath prize for the most voted solution
• Lars Viklund from Axis wins the Golden Sickle prize for the most elegant solution
• Holger Busch from Infineon wins the Magic Carpet prize for the solution with the shortest runtime

We also decided to add an extra prize:

• Anthony Wood from Imagination wins the Team Player prize for the best submission message:

Hi, delighted that you’ve done another puzzle this year. It was fun and educational last year. My solution takes 3.5s to prove uniqueness, so I doubt it will be the fastest and it’s not particularly readable, so I’m sure it’ll not be up for a prize, but I really wanted to support this by taking part. Cheers, Anthony

All four winners will receive an Amazon Echo Plus and could use it to implement a voice-controlled Sudoku solver.

For next year, we have new ideas, not only for the puzzle but also for the format of the challenge. If you have feedback or proposals to share, please email us at [email protected]. We want to hear from you.

A big thank you to all the participants. Stay tuned later this year for the next OneSpin Holiday Puzzle!