TheoSim: combining symbolic simulation and theorem proving for hardware verification

ABSTRACT

TheoSim is a symbolic verifiation tool that fills the gap between the simulation of test cases, and the use of theorem provers, for the validation of initial specifications, and the exploration of the very first design steps of digital integrated systems. The principles of Theosim are presented, followed by its application to the verification of the first design step of a state-of-the-art network on chip architecture.

REFERENCES

• 1: Accellera. Property Specification Language Reference Manual Version 1.1, 2004.
• 2: ARM. AMBA Specification, rev. 2.0.
• 3: D. Borrione, P. Georgelin, and V. Rodrigues. Symbolic simulation and verification of VHDL with ACL2. In P. J. Ashenden, J. P. Mermet, and R. Seepold, editors, System-on-chip Methodologies and Design Languages, pages 59--70. Kluwer Academic Publisher, 2001.
• 4: John A. Darringer, The application of program verification techniques to hardware verification, Proceedings of the 16th Conference on Design automation, p.375-381, June 25-27, 1979, San Diego, CA, United States
• 5: B. L. Evans, S. X. Gu, A. Kalavade, and E. A. Lee. Symbolic Computation in System Simulation and Design. In Proc. of SPIE Int. Sym. on Advanced Signal Processing Algorithms, Architectures, and Implememtations, July 1995.
• 6: R. W. Floyd. Assigning Meanings to Programs. In J. T. Schwartz, editor, Proc. Symposium in applied Mathematics, Mathematical Aspects of Computer Science, pages 19--32. American Mathematical Society, 1967.
• 7: Harry Foster , David Lacey , Adam Krolnik, Assertion-Based Design, Kluwer Academic Publishers, Norwell, MA, 2003
• 8: David A. Greve, Symbolic Simulation of the JEM1 Microprocessor, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.321-333, November 04-06, 1998
• 9: Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, You Assume, We Guarantee: Methodology and Case Studies, Proceedings of the 10th International Conference on Computer Aided Verification, p.440-451, June 28-July 02, 1998
• 10: IEEE. 1076.6-1999 IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis, 1999.
• 11: A. Jantsch. Network on Chip. In Proceedings of the Conference Radio vetenskap och Kommunication, Stockholm, June 2002.
• 12: Faraydon Karim , Anh Nguyen , Sujit Dey, An Interconnect Architecture for Networking Systems on Chips, IEEE Micro, v.22 n.5, p.36-45, September 2002 [doi>10.1109/MM.2002.1044298 ]
• 13: Faraydon Karim , Anh Nguyen , Sujit Dey , Ramesh Rao, On-chip communication architecture for OC-768 network processors, Proceedings of the 38th conference on Design automation, p.678-683, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379047]
• 14: Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
• 15: J. S. Moore. Introduction to the OBDD Algorithm for the ATP community. Technical report, Computational Logic Inc., 1992.
• 16: J. Strother Moore, Symbolic Simulation: An ACL2 Approach, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.334-350, November 04-06, 1998
• 17: G. A. Sammane, D. Toma, J. Schmaltz, P. Ostier, and D. Borrione. Constrained Symbolic Simulation using Mathematica and ACL2. In Proc. Correct Hardware Design anf Verification Methods (CHARME'03), LNCS 2860. Springer, October 2003.
• 18: J. Schmaltz and D. Borrione. A Functional Approach to the Formal Specification of Networks on Chip. In Proc. of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), Austin, Texas, USA, November 14-17 2004. Springer. To appear.
• 19: N. Shankar, S. Owre, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Prover Guide Computer Science Laboratory. Technical report, SRI International, Menlo Park, CA, USA, 1999.
• 20: Matthew Wilding , David Greve , David Hardin, Efficient Simulation of Formal Processor Models, Formal Methods in System Design, v.18 n.3, p.233-248, May 2001 [doi>10.1023/A:1011217102270 ]
• 21: Stephen Wolfram, The Mathematica book (4th edition), Cambridge University Press, New York, NY, 1999
• 22: Jin Yang , Carl-Johan H. Seger, Generalized Symbolic Trajectory Evaluation - Abstraction in Action, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.70-87, November 06-08, 2002

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Simulation

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
hardware verification, symbolic simulation, theorem proving