10 Ways To Skin A Formal Puzzle

During the holidays, OneSpin issued a challenge to solve the classic Einstein’s Riddle using any formal verification tool. Although this puzzle was meant to be a little holiday fun, its solution required thought and some useful formal techniques applicable in everyday functional verification.

We received a broad range of answers from engineers across the globe in different companies, including some of the largest semiconductor vendors. Many entries were ingenious and well thought out. Clearly, a lot of time was spent thinking about the challenge and solution approaches.

With the permission of the authors, we published the top ten solutions here: http://tinyurl.com/loqktz5. Please check them out and help us by voting for what you think is the best one. The top three will receive a remote-controlled flying drone.

Albert Einstein created the riddle in the late 1800s, goes the unfounded claim. In those days and well before formal verification, 98% of the world population couldn’t find a solution, evidently.

The riddle involves a collection of colored houses, occupants of different nationalities, drinking, smoking habits and pet ownership. The riddle provides sparse information linking these variables, and invites the reader to eventually discover “Who owns the fish!” The full riddle may be viewed on the same page as the solutions above.

While I won’t critique the solutions here and bias voting, it’s apparent that plenty of creativity went into the entries with perspectives and ideas that could be applied to a broad range of problems beyond this puzzle.

Formal’s abilities are on full display as well. Each entry included a set of properties that ran in a commercial formal verification tool, and not necessarily OneSpin’s DV-Verify. In fact, a few of the top ten entries were run on competitive formal tools.

Entries came from creative engineers with a variety of backgrounds, experiences on different design types and formal verification knowledge. As such, it’s a great learning vehicle to see how others would tackle this brain-teasing problem using verification.

We’ll take a closer look at the solutions after the contest closes Saturday, April 8, and explain how formal techniques trounced age-old Einstein’s riddle. However, if you look through the solutions, you will see an array of different angles taken to target this one problem – truly, ten ways to skin the puzzle!

Please check out these solutions, draw your own opinion and cast your vote!