Video Easter Egg: Incisive Formal Verifier and SVA driving a Rubik's Cube robot

Just in time for Easter, Team Verify's Apurva Kalia, Manu Chopra, and Suman Ray of the Incisive R&D team created a Rubik's Cube solving Lego robot.  However, unlike other such 'bots (recall the now famous ARM-driven Rubik's Cube ‘bot at ARM's TechCon), the brain of this one is actually a single SVA assertion that is solved in an instant by Incisive Formal Verifier (IFV).  Check it out:

If video fails to open, click here.

More details about this project:

* The core program is a single SVA assertion (in a nutshell, "never (solved cube)"), which IFV solves and then produces a counter example which turns out to be the optimal solution to the cube.  A script translates the counter-example signals into a set of actuator commands for the robot to execute.

* Taking a step back: first, the scrambled state of the cube is read - 6 faces, and 54 cubelets in all - and translated into an array on the ‘bot end, which is transferred to a Linux machine via a VNC session.

* On the Linux machine a script takes the sensor data array and models the cube as a Verilog array of 54 consecutive numbers, each of which can have a value of 1-6 (signifying the 6 colors).

* An "always" block models the quarter turn of one face at each posedge clock.  The array is modified appropriately when the face is turned one quarter turn.

* There is practically no limit to the size cubes this algorithm can handle - as long as you have enough Lego Mindstorms, you could solve arbitrarily large cubes.

* The robot design itself was taken from http://www.tiltedtwister.com  Hans Andersson - the owner of that site - is truly an inspiration to Lego-maniacs everywhere!

Happy solving!

Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify