Home > Community > Blogs > Functional Verification > video easter egg incisive formal verifier and sva driving a rubik s cube robot

 Login with a Cadence account. Not a member yet? Create a permanent login account to make interactions with Cadence more conveniennt. Register | Membership benefits
 Get email delivery of the Functional Verification blog (individual posts).

## Email

Recipients email * (separate multiple addresses with commas)

Message *

 Send yourself a copy

## Subscribe

Intro copy of the newsletter section here, some intro copy of the newsletter. Instruction of how to subscribe to this newsletter.

First Name *

Last Name *

Email *

Company / Institution *

 Send Yourself A Copy

# 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:

* 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