Distance-guided hybrid verification with GUIDO

ABSTRACT

Constrained random simulation is a widespread technique used to perform functional verification on complex digital designs, because it can generate simulation vectors at a very high rate. However, the generation of high-coverage tests remains a major challenge even in light of this high performance. In this paper we present Guido, a hybrid verification software that uses formal verification techniques to guide the simulation towards a verification goal. Guido is novel in that 1) it guides the simulation by means of a distance function derived from the circuit structure, and 2) it has a trace sequence controller that monitors and controls the direction of the simulation by striking a balance between random chance and controlled hill-climbing. We present experimental results indicating that Guido can tackle complex designs, including a picoJava microprocessor, and reach a verification goal in far fewer simulation cycles than random simulation.

REFERENCES

• 1: Mark D. Aagaard , Robert B. Jones , Carl-Johan H. Seger, Combining theorem proving and trajectory evaluation in an industrial environment, Proceedings of the 35th annual conference on Design automation, p.538-541, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277189]
• 2: Sigal Asaf , Eitan Marcus , Avi Ziv, Defining coverage views to improve functional coverage analysis, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996579]
• 3: Janick Bergeron, Writing Testbenches: Functional Verification of HDL Models, Second Edition, Kluwer Academic Publishers, Norwell, MA, 2003
• 4: Jules P. Bergmann , Mark A. Horowitz, Improving coverage analysis and test generation for large designs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.580-583, November 07-11, 1999, San Jose, California, United States
• 5: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 6: Per Bjesse , James Kukula, Using Counter Example Guided Abstraction Refinement to Find Complex Bugs, Proceedings of the conference on Design, automation and test in Europe, p.10156, February 16-20, 2004
• 7: J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
• 8: Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
• 9: Malay K. Ganai , Adnan Aziz , Andreas Kuehlmann, Enhancing simulation with BDDs and ATPG, Proceedings of the 36th ACM/IEEE conference on Design automation, p.385-390, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309965]
• 10: Faisal Haque , Jonathan Michelson, Art of Verification with VERA, Verification Central, 2001
• 11: Scott Hazelhurst , Osnat Weissberg , Gila Kamhi , Limor Fix, A hybrid verification approach: getting deep into the design, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.513948]
• 12: Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 13: Richard C. Ho , Mark A. Horowitz, Validation coverage analysis for complex digital designs, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.146-151, November 10-14, 1996, San Jose, California, United States
• 14: A. Hu. Formal hardware verification with BDDs: An introduction. In IEEE Pacific Rim Conference on Communications, Computers and Signal Processing (PACRIM), pages 677--682, 1997.
• 15: Andreas Kuehlmann , Kenneth L. McMillan , Robert K. Brayton, Probabilistic state space search, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.574-579, November 07-11, 1999, San Jose, California, United States
• 16: Kanna Shimizu , David L. Dill, Deriving a simulation input generator and a coverage metric from a formal specification, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514118]
• 17: Sun Microsystems. PicoJava technology. http://www.sun.com/microelectronics/communitysource/picojava.
• 18: Texas 97 benchmark suite. http://www-cad.eecs.berkeley.edu/Respep/Research/vis/texas-97.
• 19: Praveen Yalagandula , Vigyan Singhal , Adnan Aziz, Automatic lighthouse generation for directed state space search, Proceedings of the conference on Design, automation and test in Europe, p.237-242, March 27-30, 2000, Paris, France [doi>10.1145/343647.343771]
• 20: C. Han Yang , David L. Dill, Validation with guided search of the state space, Proceedings of the 35th annual conference on Design automation, p.599-604, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277201]
• 21: Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Modeling design constraints and biasing in simulation using BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.584-590, November 07-11, 1999, San Jose, California, United States