OneSpin Puzzler:
The Top 10 Solutions

Our 2017–18 Holiday Puzzle

The holidays are here again! Last year, we set a challenge to engineers everywhere: solve the famous Einstein’s Riddle using a formal tool. The response was tremendous, and we had many requests for another such contest this year. We’re happy to oblige!

Sasa Stamenkovic, one of our awesome senior field application engineers, devised a fun and challenging puzzle for you: How about a little Sudoku?


The Sudoku Challenge

Ah, Sudoku. Never did a puzzle offer such a variety of difficulty levels. These variable little brain teasers can make you feel like you’re out for a gentle stroll in the park, or they can give you the impression that you’re scaling a mountain with a refrigerator on your back—and everything in between.

In 2012, Finnish mathematician Arto Inkala came up with what was then regarded as the hardest Sudoku in the world (pictured at right). Apparently, on a difficulty scale from one to five stars, this Sudoku would score eleven stars. Sudoku’s Everest!

Faced with such a hard slog to complete this seemingly insurmountable puzzle, it’s only natural to look for ways to find a foothold and get a leg up (ha ha ha). Formal tools to the rescue! With a little programming, they can virtually teleport you to the summit.

What do you say? Are you up to the task?

Your mission—should you choose to accept it—is as follows:

Set up the problem. You can use VHLD/Verilog/SystemVerilog to write RTL code and SVA/PSL/ITL for assertions.

You can use any formal tool to find the solution, but make sure the tool script only uses the basic commands to compile and run the checks, so that your code is fit to run on other formal tools and even simulators.

Additionally, without using the information on the solution you have found, write an assertion to prove that the solution is unique. A simulator won’t be any good for that—ha!

We have three prizes to give away:

The Golden Sickle

OneSpin’s jury will select the most reusable, compact, readable and elegant solution.

The Magic Carpet

We will run the solution on OneSpin and select the fastest one.

The Laurel Wreath

The best solutions will be put against popular judgement, with the most voted one taking this prize.

Each winner will receive an Amazon Echo Plus. You've automated your Sudoku solving, why not automate your home as well?

Deadline has been passed on Sunday, January 7th, 2018

Winners will be announced by the end of February after a thorough review. Best of luck!