MYGEN: automata-based on-line test generator for assertion-based verification

ABSTRACT

To assist in dynamic assertion-based verification, we present a method to automatically build a test vector generator from a temporal property. Based on the duality between monitors and generators, we have extended the monitor generator tool MYGEN to produce synthesizable on-line generators. We have tested the resulting generators in simulation and by emulation on an FPGA. The combination of multiple generators provides an efficient way to model the environment of modules within a DUT, facilitating an equivalent of software "unit testing" under real conditions, early in the design flow.

REFERENCES

• 1: http://freshmeat.net/projects/bool-expr-solve/.
• 2: http://www-tima.imag.fr/vds/horus/mygen_props/.
• 3: Marc Boulé , Zeljko Zilic, Automata-based assertion-checker synthesis of PSL properties, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.1, p.1-21, January 2008 [doi>10.1145/1297666.1297670]
• 4: J. Calamé. Specification-based test generation with TGV. Technical Report R0508, Centrum voor Wsikunde en Informatica, May 2005.
• 5: Hans Eveking , Martin Braun , Martin Schickel , Martin Schweikert , Volker Nimbler, Multi-Level Assertion-Based Design, Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, p.85-86, May 30-June 02, 2007 [doi>10.1109/MEMCOD.2007.371244]
• 6: Harry Foster , David Lacey , Adam Krolnik, Assertion-Based Design, Kluwer Academic Publishers, Norwell, MA, 2003
• 7: H. Foster, Y. Wolfshal, E. Marschner, and I. W. Group. IEEE standard for Property Specification Language PSL. pub-IEEE-STD, pub-IEEE-STD:adr, Oct 2005.
• 8: K. Morin-Allory, M. Boulé, D. Borrione, and Z. Zilic. Proving and disproving assertion rewrite rules by automated theorem proving. In IEEE International High Level Design Validation and Test Workshop 2008 HLDVT'08, Nov. 2008.
• 9: Y. Oddos, K. Morin-Allory, and D. Borrione. Assertion-based design with horus. In 6th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'2008, Jun. 2008.
• 10: B. Pal, A. Banerjee, A. Sinha, and P. Dasgupta. Accelerating assertion coverage with adaptative testbenches. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, volume 27, pages 967--972, May 2008.
• 11: Irith Pomeranz , Sudhakar M. Reddy, Circuit lines for guiding the generation of random test sequences for synchronous sequential circuits, Proceedings of the 2008 Asia and South Pacific Design Automation Conference, January 21-24, 2008, Seoul, Korea
• 12: Barry Shackleford , Motoo Tanaka , Richard J. Carter , Greg Snider, High-Performance Cellular Automata Random Number Generators for Embedded Probabilistic Computing Systems, Proceedings of the 2002 NASA/DoD Conference on Evolvable Hardware (EH'02), p.191, July 15-18, 2002
• 13: Kanna Shimizu , David L. Dill, Deriving a simulation input generator and a coverage metric from a formal specification, Proceedings of the 39th annual Design Automation Conference, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514118]
• 14: J. Srouji, S. Mehta, D. Brophy, K. Pieper, S. Sutherland, and I. W. Group. IEEE Standard for SystemVerilog - Unified Hardware Design, Specification, and Verification Language. pub-IEEE-STD, pub-IEEE-STD:adr, Nov 2005.
• 15: Raghuram S. Tupuri , Arun Krishnamachary , Jacob A. Abraham, Test generation for Gigahertz processors using an automatic functional constraint extractor, Proceedings of the 36th annual ACM/IEEE Design Automation Conference, p.647-652, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310018]
• 16: Stephen Wolfram, Random sequence generation by cellular automata, Advances in Applied Mathematics, v.7 n.2, p.123-169, June 1986 [doi>10.1016/0196-8858(86)90028-X]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.2 ARITHMETIC AND LOGIC STRUCTURES
      B.2.3 Reliability, Testing, and Fault-Tolerance**
          Subjects: Test generation**

General Terms:
Verification

Keywords:
generator, psl, test vector generation