Keep The Wooden Horse Out Of Your Chip


The OneSpin's Holiday Puzzle tradition has reached its fourth year: hear, hear! In December 2016, OneSpin challenged engineers to solve the Einstein riddle using assertions and a formal verification tool. In December 2017, the challenge was to model the hardest Sudoku in the world using assertions and find a solution with a formal tool. The OneSpin 2018-19 Holiday Puzzle asked engineers to desi... » read more

This Year’s Holiday Puzzle: Find The Trojan Horse


The term “Trojan horse” is widely used, but it’s likely that not everyone knows the story behind this metaphor. It refers to an ancient legend about a giant wooden horse that contained a most unpleasant surprise for its recipients. In general usage, the term refers to anything dangerous that lurks within a seemingly innocent disguise. The electronics hardware design community is increasin... » read more

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 enthusi... » read more

Using Formal To Solve The World’s Hardest Sudoku


It’s no secret that the OneSpin team loves contests. Last year around this time, we set a challenge to engineers everywhere: solve the famous Einstein’s Riddle using a formal tool. After an enthusiastic response, we decided to make the holiday puzzle an annual event, with a different subject area each year. Our engineering team was challenged to come up with a new topic, and my idea, whi... » read more