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

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

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

Comments(0)Filed under: Formal Analysis, ARM, SVA, ABV, Verilog, IEV, formal, IFV, assertions, formal verification, assertion-based verification, Lego, Manu Chopra, Suman Ray, Apurva Kalia, Easter, robot, Rubik's Cube, egg

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

 

Comments(0)

Leave a Comment


Name
E-mail (will not be published)
Comment
 I have read and agree to the Terms of use and Community Guidelines.
Community Guidelines
The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.