Advertisement

A foundation for formal reuse of hardware

  • Ana C. V. de Melo
  • Howard Barringer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

This paper presents a basis for the formal reuse of hardware components as a strategy to reduce the task of verifying new hardware elements. Assuming the existence of a library of formally verified hardware components, we propose to make effective reuse of these existing elements when creating new ones. The strategy used is to formally create an interface element with which an existing hardware component is composed in order to implement a new desired component. In doing so, the verification task of the whole system is reduced to verifying the interface element.

Keywords

Reusability High-Level Synthesis Formal Methods Process Algebras Bisimulation Interface Equation 

References

  1. 1.
    André Arnold. Finite Transition Systems. International Series in Computer Science. Prentice-Hall, 1994.Google Scholar
  2. 2.
    H. Barringer, G. Gough, B. Monahan, and A. Williams. An algebraic framework for action and process. D2.3c, Formal Verification Support for ELLA, IED project 4/1/1357, University of Manchester, May 1993.Google Scholar
  3. 3.
    H. Barringer, G. Gough, B. Monahan, and A. Williams. A process algebra foundation for reasoning about core ELLA. Technical Report 94-12-1, University of Manchester, Dec 1994.Google Scholar
  4. 4.
    T. J. Biggerstaff and A, J. Perlis. Software Reusability — Applications and Experience, volume 2. Addison-Wesley Publishing Company, first edition, 1989.Google Scholar
  5. 5.
    T. J. Biggerstaff and A. J. Perlis. Software Reusability — Concepts and Models, volume 1. Addison-Wesley Publishing Company, first edition, 1989.Google Scholar
  6. 6.
    H. Busch, H. Nusser, and T. Rössel. Formal methods for synthesis. In P. Michael, U. Lauther, and P. Duzy, editors, The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1993.Google Scholar
  7. 7.
    Ana C. V. de Melo. Formal Reuse of Hardware Design. PhD thesis, University of Manchester, March 1995.Google Scholar
  8. 8.
    Srinivas Devadas. Optimizing interacting finite state machines using sequential don't cares. IEEE Transactions on Computer-Aided Design, December 1991.Google Scholar
  9. 9.
    P. Freeman. A perspective on reusability. In Peter Freeman, editor, Tutorial: Software Reusability. IEEE — The Computer Society Press, 1987.Google Scholar
  10. 10.
    Peter Freeman. Tutorial: Software Reusability. IEEE — The Computer Society Press, 1987.Google Scholar
  11. 11.
    M. C. Gaudel and T. Moineau. A theory of software reusability. In ESOP'88, volume 300 of LNCS. Springer Verlag, 1988.Google Scholar
  12. 12.
    Arthur Gill. Introduction to the Theory of Finite-State Machines. McGraw-Hill Book Company, first edition, 1962.Google Scholar
  13. 13.
    W. Glunz, A. Pyttel, and G. Venzl. System-level synthesis. In P. Michael, U. Lauther, and P. Duzy, editors, The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1993.Google Scholar
  14. 14.
    Joseph A. Goguen. Principles of parameterized programming. In T. J. Biggerstaff and A. J. Perlis, editors, Software Reusability — Concepts and Models, volume 1. Addison-Wesley Publishing Company, 1989.Google Scholar
  15. 15.
    M. J. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986.Google Scholar
  16. 16.
    J. W. Hooper and R. O. Chester. Software Reuse — Guidelines and Methods. Software Science and Engineering. Plenum Press, 1991.Google Scholar
  17. 17.
    T. C. Jones. Reusability in programming: A survey of the state of the art. In Peter Freeman, editor, Tutorial: Software Reusability. IEEE — The Computer Society Press, 1987.Google Scholar
  18. 18.
    Shmuel Katz, Charles A. Richer, and Khe-Sing The. PARIS: A system for reusing partially interpreted schemas. In T. J. Biggerstaff and A. J. Perlis, editors, Software Reusability — Concepts and Models, volume 1. Addison-Wesley Publishing Company, 1989.Google Scholar
  19. 19.
    M. D. McIlroy. Mass-produced software components. In J. M. Buxton, P. Naur, and B. Randell, editors, Software Eng. Concepts and Techniques — 1968 NATO Conf. Software Eng. Petrocelli/Charter, 1976.Google Scholar
  20. 20.
    P. Michael, U. Lauther, and P. Duzy. The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1993.Google Scholar
  21. 21.
    George Milne. Formal Specification and Verification of Digital Systems. McGraw-Hill, first edition, 1994.Google Scholar
  22. 22.
    Robin Milner. Communication and Concurrency. Prentice-Hall, first edition, 1989.Google Scholar
  23. 23.
    J D Morison and A S Clarke. ELLA2000: A Language for Electronic System Design. McGraw-Hill, 1993.Google Scholar
  24. 24.
    N. S. Nagaraj. OPSYN — OASYS based pseudosynthesis tool. In VLSI Design 1992 — The fifth International Conference on VLSI Design. IEEE — The Computer Society Press, 1992.Google Scholar
  25. 25.
    Joachim Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68:175–202, 1989.Google Scholar
  26. 26.
    Lucia Pomello. Some equivalence notions for concurrent systems. an overview. In Advances in Petri Nets 1985, volume 222 of LNCS. Springer-Verlag, 1985.Google Scholar
  27. 27.
    Franklin P. Prosser and David E. Winkel. The art of Digital Design. Pentice Hall International Editions, second edition, 1987.Google Scholar
  28. 28.
    Noah S. Prywes and Evan D. Lock. Use of the model equational language and program generator by management professionals. In T. J. Biggerstaff and A. J. Perlis, editors, Software Reusability — Applications and Experience, volume 2. Addison-Wesley Publishing Company, 1989.Google Scholar
  29. 29.
    Huajan Qin and Philip Lewis. Factorization of finite state machines under observational equivalence. In J. C. M. Baeten and J. F. Groote, editors, CONCUR'91, volume 527 of LNCS. Springer-Verlag, 1991.Google Scholar
  30. 30.
    W. SchÄfer, R. Prieto-Díaz, and M. Matsumoto. Software Reusability. Ellis Horwood, 1994.Google Scholar
  31. 31.
    M. W. Shields. Implicit system specification and the interface equation. The Computer Journal, 32(5), 1989.Google Scholar
  32. 32.
    Stephen H. Unger. Asynchronous Sequential Switching Circuits. Wiley-Interscience, first edition, 1969.Google Scholar
  33. 33.
    R. J. van Glabbeek. The Linear Time — Branching Time Spectrum. In CON-CUR'90, volume 458 of LNCS. Springer-Verlag, 1990.Google Scholar
  34. 34.
    R. J. van Glabbeek. The Linear Time — Branching Time Spectrum II. In CON-CUR'93, volume 715 of LNCS. Springer-Verlag, 1993.Google Scholar
  35. 35.
    Dennis M. Volpano and Richard B. Kieburtz. The templates approach to software reuse. In T. J. Biggerstaff and A. J. Perlis, editors, Software Reusability — Concepts and Models, volume 1. Addison-Wesley Publishing Company, 1989.Google Scholar
  36. 36.
    M. Wirsing, R. Hennicker, and R. Stahl. Menu — an example for the systematic reuse of specifications. In 2nd European Software Engineering Conference, volume 387 of LNCS. Springer Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ana C. V. de Melo
    • 1
  • Howard Barringer
    • 1
  1. 1.Department of Computer ScienceUniversity of ManchesterManchesterUK

Personalised recommendations