Solving Einstein’s Riddle Using Formal Verification

Attention all Sherlockians in the semiconductor industry! OneSpin Solutions challenges you to take on Einstein’s Riddle Intelligence Test below and spend the holidays puzzling it out, using the brand of formal verification software of your choosing.

Three remote-controlled flying drones will be awarded to the three fastest solutions to the riddle that execute correctly on OneSpin’s DV-Verify formal verification software. OneSpin will publish the results and promote them at DVCon in March.

Einstein’s Riddle

Einstein purportedly devised the riddle in the late 1800s and suggested that only 2% of the world’s population could solve it. While there’s no evidence to the claim he is the author, it earned the logic puzzle the nickname “Einstein’s Riddle.” Of course, Einstein didn’t have access to formal verification or the brainpower in our industry. Regardless, logic and deduction such as Sherlock Holmes would employ and formal verification is all you need to get to the solution. It’s elementary, my dear puzzler.

Here is the riddle: Five houses on one street are in five different colors. In each house lives a person with a different nationality. These five owners drink a certain type of beverage, smoke a certain brand of cigar and keep a certain pet. No owners have the same pet, paid the same amount for their pet, smoke the same brand of tobacco or drink the same beverage.

The question is: Who owns the fish?

Some additional clues to help solve the riddle:

• The Brit lives in the red house
• The Swede keeps dogs as pets
• The Dane drinks tea
• The green house is on the left of the white house
• The owner of the green house drinks coffee
• The person who smokes Pall Mall raises birds
• The owner of the yellow house smokes Dunhill cigarettes
• The man living in the center house drinks milk
• The Norwegian lives in the first house
• The man who smokes blends lives next to the one who keeps cats
• The man who keeps horses lives next to the man who smokes Dunhill cigarettes
• The owner who smokes BlueMaster drinks beer
• The German smokes Prince cigarettes
• The Norwegian lives next to the blue house
• The man who smokes blend has a neighbor who drinks water

As a puzzler, you should come up with a set of properties to run in your favorite formal verification tool or write out the solution that should work. The riddle can be solved using formal verification with a simple Verilog or VHDL model and some properties.

OneSpin will run the solution in DV-Verify and will award drones to the three puzzlers with the fastest solutions. All submissions must be received by Monday, January 16. Submissions should be emailed to: [email protected].

Don’t be a fictional detective like Sherlock Holmes or sit on the sidelines as Dr. Watson did. Instead, put on your deerstalker cap and try your hand at solving the riddle. Meerschaum pipe optional.