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,
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!
On Twitter: http://twitter.com/teamverify, @teamverify