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.
Chapter PDF
References
André Arnold. Finite Transition Systems. International Series in Computer Science. Prentice-Hall, 1994.
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.
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.
T. J. Biggerstaff and A, J. Perlis. Software Reusability — Applications and Experience, volume 2. Addison-Wesley Publishing Company, first edition, 1989.
T. J. Biggerstaff and A. J. Perlis. Software Reusability — Concepts and Models, volume 1. Addison-Wesley Publishing Company, first edition, 1989.
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.
Ana C. V. de Melo. Formal Reuse of Hardware Design. PhD thesis, University of Manchester, March 1995.
Srinivas Devadas. Optimizing interacting finite state machines using sequential don't cares. IEEE Transactions on Computer-Aided Design, December 1991.
P. Freeman. A perspective on reusability. In Peter Freeman, editor, Tutorial: Software Reusability. IEEE — The Computer Society Press, 1987.
Peter Freeman. Tutorial: Software Reusability. IEEE — The Computer Society Press, 1987.
M. C. Gaudel and T. Moineau. A theory of software reusability. In ESOP'88, volume 300 of LNCS. Springer Verlag, 1988.
Arthur Gill. Introduction to the Theory of Finite-State Machines. McGraw-Hill Book Company, first edition, 1962.
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.
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.
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.
J. W. Hooper and R. O. Chester. Software Reuse — Guidelines and Methods. Software Science and Engineering. Plenum Press, 1991.
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.
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.
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.
P. Michael, U. Lauther, and P. Duzy. The Synthesis Approach to Digital System Design. Kluwer Academic Publishers, 1993.
George Milne. Formal Specification and Verification of Digital Systems. McGraw-Hill, first edition, 1994.
Robin Milner. Communication and Concurrency. Prentice-Hall, first edition, 1989.
J D Morison and A S Clarke. ELLA2000: A Language for Electronic System Design. McGraw-Hill, 1993.
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.
Joachim Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68:175–202, 1989.
Lucia Pomello. Some equivalence notions for concurrent systems. an overview. In Advances in Petri Nets 1985, volume 222 of LNCS. Springer-Verlag, 1985.
Franklin P. Prosser and David E. Winkel. The art of Digital Design. Pentice Hall International Editions, second edition, 1987.
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.
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.
W. SchÄfer, R. Prieto-Díaz, and M. Matsumoto. Software Reusability. Ellis Horwood, 1994.
M. W. Shields. Implicit system specification and the interface equation. The Computer Journal, 32(5), 1989.
Stephen H. Unger. Asynchronous Sequential Switching Circuits. Wiley-Interscience, first edition, 1969.
R. J. van Glabbeek. The Linear Time — Branching Time Spectrum. In CON-CUR'90, volume 458 of LNCS. Springer-Verlag, 1990.
R. J. van Glabbeek. The Linear Time — Branching Time Spectrum II. In CON-CUR'93, volume 715 of LNCS. Springer-Verlag, 1993.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Melo, A.C.V., Barringer, H. (1995). A foundation for formal reuse of hardware. In: Camurati, P.E., Eveking, H. (eds) Correct Hardware Design and Verification Methods. CHARME 1995. Lecture Notes in Computer Science, vol 987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60385-9_8
Download citation
DOI: https://doi.org/10.1007/3-540-60385-9_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60385-6
Online ISBN: 978-3-540-45516-5
eBook Packages: Springer Book Archive