Asterix In The Land Of Sudoku: The Fast, The Elegant, And The Popular Formal Solvers
By Sergio Marchese, Semiconductor Engineering
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.
[…]
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.
