• Home
  • :
  • Community
  • :
  • Blogs
  • :
  • Functional Verification
  • :
  • Video Easter Egg: Incisive Formal Verifier and SVA driving…

Functional Verification Blogs

  • All Blog Categories
  • Breakfast Bytes
  • Cadence Academic Network
  • Cadence Support
  • Computational Fluid Dynamics
  • CFD(数値流体力学)
  • 中文技术专区
  • Custom IC Design
  • カスタムIC/ミックスシグナル
  • 定制IC芯片设计
  • Digital Implementation
  • Functional Verification
  • IC Packaging and SiP Design
  • In-Design Analysis
    • In-Design Analysis
    • Electromagnetic Analysis
    • Thermal Analysis
    • Signal and Power Integrity Analysis
    • RF/Microwave Design and Analysis
  • Life at Cadence
  • Mixed-Signal Design
  • PCB Design
  • PCB設計/ICパッケージ設計
  • PCB、IC封装:设计与仿真分析
  • PCB解析/ICパッケージ解析
  • RF Design
  • RF /マイクロ波設計
  • Signal and Power Integrity (PCB/IC Packaging)
  • Silicon Signoff
  • Solutions
  • Spotlight Taiwan
  • System Design and Verification
  • Tensilica and Design IP
  • The India Circuit
  • Whiteboard Wednesdays
  • Archive
    • Cadence on the Beat
    • Industry Insights
    • Logic Design
    • Low Power
    • The Design Chronicles
TeamVerify
TeamVerify
21 Apr 2011

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

 

Tags:
  • Suman Ray |
  • ABV |
  • Apurva Kalia |
  • Formal Analysis |
  • Easter |
  • formal |
  • Manu Chopra |
  • SVA |
  • Verilog |
  • Lego |
  • assertions |
  • egg |
  • robot |
  • ARM |
  • IEV |
  • Rubik's Cube |
  • Formal verification |
  • IFV |
  • Assertion-based verification |