Test generation games from formal specifications

ABSTRACT

In this paper, we present methods for automatic test generation from formal specifications.These are used to create intelligent test benches that are able to cover corner case behaviors in much less time.We have developed a prototype tool for intelligent test generation within the layered test bench architecture proposed in RVM.We present results on verification IPs of standard bus protocols to show the effectiveness of our approach.

REFERENCES

• 1: Jacob A. Abraham , Vivekananda M. Vedula , Daniel G. Saab, Verifying Properties Using Sequential ATPG, Proceedings of the 2002 IEEE International Test Conference, p.194, October 07-10, 2002
• 2: Paul E. Ammann , Paul E. Black , William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.46, December 09-11, 1998
• 3: Edmund M. Clarke , Steven M. German , Yuan Lu , Helmut Veith , Dong Wang, Executable Protocol Specification in ESL, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.197-216, November 01-03, 2000
• 4: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
• 5: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.146-162, September 06-10, 1999, Toulouse, France
• 6: Aarti Gupta , Albert E. Casavant , Pranav Ashar , Akira Mukaiyama , Kazutoshi Wakabayashi , X. G. (Sean) Liu, Property-Specific Testbench Generation for Guided Simulation, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.524, January 07-11, 2002
• 7: IBM CoreConnect, http://www-306.ibm.com/chips/techlib/techlib.nsf/techdocs
• 8: Pnueli,A.,The temporal logic of programs;FOCS '77,46--57.
• 9: A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75293]
• 10: Reference Verification Methodology for Vera,http://www. synopsys.com/products/simulation/pdf/va vol4 iss1 vera.pdf
• 11: Suchismita Roy , Sayantan Das , Prasenjit Basu , Pallab Dasgupta , P. P. Chakrabarti, SAT based solutions for consistency problems in formal property specifications for open systems, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.885-888, November 06-10, 2005, San Jose, CA
• 12: 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]
• 13: System Verilog,http://www.eda.org/sv/SystemVerilog 3.1a.pdf
• 14: Serdar Tasiran , Yuan Yu , Brannon Batson, Using a formal specification and a model checker to monitor and direct simulation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775926]
• 15: VCS,http://www.synopsys.com/products/simulation/

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
realizability, test generation, vacuity