You’ve seen robotic Rubik’s cube solvers before—even in EDA360 Insider. (For example, see “Friday Video: Multicore, ARM-powered CubeStormer II solved Rubik’s Cube puzzle in world-beating 4.762 seconds”). Well, Cadence once again had its robotic Rubik’s Cube solver powered by Incisive Formal Verifier running at this week’s DVCon and it was a popular demonstration judging by the crowd.
This time, I got a bit more information about the Formal application program that’s powering the brain of the solver. There’s a Verilog description that models the cube’s state as a series of flip-flops. The Mindstorms robot examines the cube and then sends a text file representing the current state of the cube to the PC running Incisive Formal verifier. The text file initializes the state of the Rubik’s Cube Verilog representation and the Incisive Formal Verifier then goes to work using just one assertion that essentially says “Show me how all of the faces of this cube can match.”
The ensuing activity of the Verifier generates the stimulus needed to command the Mindstorms robotic Rubik’s Cube manipulator to rotate the cube until all of the squares on all of the faces do match. In a sense, the Formal verification assertion has become an app.
Here’s the video from DVCon showing the Formal robotic Rubik’s cube solver in action:
Note: To see the earlier EDA360 Insider blog on this topic written in September of last year, see “Friday Video: Rubik’s Cube puzzle solved with Lego Mindstorms robot and… Cadence Incisive Formal Verifier???”
