Verification of design decisions in ForSyDe

ABSTRACT

The ForSyDe methodology has been developed for system level design. Starting with a formal specification model that captures the functionality of the system at a high abstraction level, it provides formal design transformation methods for a transparent refinement process of the specification model into an implementation model that is optimized for synthesis. A transformation may be semantic preserving or a design decision. The latter modifies the semantics of the system level description and changes the meaning of the model. The main contribution of this paper is the incorporation of model checking to verify that refined system blocks satisfy the design specification. We illustrate the translation of the ForSyDe code to the SMV language and the verification of local design decisions with a case study of a ForSyDe equalizer model.

REFERENCES

• 1: The SMV model checker. http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/.
• 2: Friedrich Ludwig Bauer , Bernhard Möller , Helmut Partsch , Peter Pepper, Formal Program Construction by Transformations-Computer-Aided, Intuition-Guided Programming, IEEE Transactions on Software Engineering, v.15 n.2, p.165-180, February 1989 [doi>10.1109/32.21743]
• 3: Albert Benveniste and Gerard Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79(9):1270--1282, September 1991.
• 4: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
• 5: Per Bjesse , Koen Claessen , Mary Sheeran , Satnam Singh, Lava: hardware design in Haskell, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.174-184, September 26-29, 1998, Baltimore, Maryland, United States
• 6: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
• 7: David Cyrluk , S. Rajan , Natarajan Shankar , Mandayam K. Srivas, Effective Theorem Proving for Hardware Verification, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.203-222, September 26-28, 1994
• 8: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 9: Nicolas Halbwachs , Fabienne Lagnier , Christophe Ratel, Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE, IEEE Transactions on Software Engineering, v.18 n.9, p.785-793, September 1992 [doi>10.1109/32.159839]
• 10: Edward A. Lee and Alberto Sangiovanni-Vincentelli. A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(12):1217--1229, December 1998.
• 11: Zhonghai Lu , Ingo Sander , Axel Jantsch, A case study of hardware and software synthesis in ForSyDe, Proceedings of the 15th international symposium on System Synthesis, October 02-04, 2002, Kyoto, Japan [doi>10.1145/581199.581219]
• 12: Helmut A. Partsch, Specification and transformation of programs: a formal approach to software development, Springer-Verlag New York, Inc., New York, NY, 1990
• 13: Alberto Pettorossi , Maurizio Proietti, Rules and strategies for transforming functional and logic programs, ACM Computing Surveys (CSUR), v.28 n.2, p.360-414, June 1996 [doi>10.1145/234528.234529]
• 14: Ingo Sander , Axel Jantsch, Transformation based communication and clock domain refinement for system design, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.513992]
• 15: Ingo Sander , Axel Jantsch , Zhonghai Lu, Development and Application of Design Transformations in ForSyDe, Proceedings of the conference on Design, Automation and Test in Europe, p.10364, March 03-07, 2003
• 16: Tiberiu Seceleanu. Systematic Design of Synchronous Digital Circuits. PhD thesis, University of Turku, Finland, 2001.
• 17: Simon Thompson, The Haskell: The Craft of Functional Programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Systems specification methodology

General Terms:
Design, Verification

Keywords:
design refinement, system design, verification