Friday Video: Incisive Formal Verifier solves Rubik’s Cube redux at DVCon 2012

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???

About sleibson2

EDA360 Evangelist and Marketing Director at Cadence Design Systems (blog at https://eda360insider.wordpress.com/)
This entry was posted in EDA360, Verification and tagged , , , , , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s