HW/SW co-verification of embedded systems using bounded model checking

ABSTRACT

Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes more and more important. In this paper we present an integrated approach for formal verification of hardware and software. The approach is demonstrated on a RISC CPU. The verification is based on bounded model checking. Besides correctness proofs of the underlying hardware the hardware/software interface and programs using this interface can be formally verified.

REFERENCES

• 1: Accellera Property Specification Language Reference Manual, version 1.1. http://www.pslsugar.org, 2005.
• 2: B. Becker, R. Drechsler, and P. Molitor. Technische Informatik --- Eine Einführung. Pearson Education Deutschland, 2005.
• 3: 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
• 4: Per Bjesse , Koen Claessen, SAT-Based Verification without State Space Traversal, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.372-389, November 01-03, 2000
• 5: Nikolaos Kostaras , H. T. Vergos, SyCE: An Integrated Environment for System Design in SystemC, Proceedings of the 16th IEEE International Workshop on Rapid System Prototyping (RSP'05), p.258-260, June 08-10, 2005 [doi>10.1109/RSP.2005.46]
• 6: D. Groβe and R. Drechsler. CheckSyC: An efficient property checker for RTL SystemC designs. In IEEE International Symposium on Circuits and Systems, pages 4167--4170, 2005.
• 7: D. Groβe, U. Kühne, C. Genz, F. Schmiedle, B. Becker, R. Drechsler, and P. Molitor. Modellierung eines Mikroprozessors in SystemC. In ITG/GI/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", 2005.
• 8: Thorsten Grotker, System Design with SystemC, Kluwer Academic Publishers, Norwell, MA, 2002
• 9: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 10: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 11: Synopsys Inc., CoWare Inc., and Frontier Design Inc., http://www.systemc.org. Functional Specification for SystemC 2.0.
• 12: Klaus Winkelmann , Hans-Joachim Trylus , Dominik Stoffel , Görschwin Fey, Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor, Proceedings of the conference on Design, automation and test in Europe, p.10162, February 16-20, 2004

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Verification

Keywords:
PSL, SystemC, bounded model checking, embedded systems, formal verification, hardware/software co-verification