Abstract
Logical organization refers to a system's decomposition into functional units, processes, and so on; it is sometimes called the ‘structural’ aspect of system description. In an approach to digital synthesis based on functional algebra, logical organization is developed using a class of transformations called system factorizations. These transformations isolate subsystems and encapsulate them as applicative combinators. Factorizations have a variety of uses, ranging from the refinement of actual architecture to the synthesis of certain kinds of verification conditions. This paper outlines the foundations for this algebra and presents several examples.
This research was supported, in part, by NSF grants MIP8707067 and DCR8521497.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Raymond Boute, “Systems Semantics: Principles, Applications, and Implementations,” ACM Transactions on Programming Languages and Systems10(1):188–155 (1988).
C. David Boyer and Steven D. Johnson, “A Derived Garbage Collector,” in J. Darringer and F. Ramming (eds.) Computer Hardware Description Languages and their Applications (Proceedings of the Ninth IFIP WG 10.2 Symposium, CHDL-89), Elsevier, Amsterdam, in preparation.
Paolo Camuarati and Paolo Prinetto, “Formal Verification of Hardware Correctness: Introduction and Survey of Current Research,” Computer21(7):8–19 (1988).
A.L. Davis, “What Do Computer Architects Design Anyway?” (Preliminary papers of the 1988 Banff hardware Verification Workshop).
Daniel D. Gajski, Silicon Compilation, Addison-Wesley, Reading, 1987.
Ganesh C. Gopalakrishnan, Richard M. Fujimoto, and Kevin Smith, “Specification Driven Design of Custom Architectures in HOP, (Preliminary papers of the 1988 Banff Hardware Verification Workshop).
J.A. Goguen, J.W. Thatcher, and E.G. Wagner, “An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types,” in R. Yeh (ed.) Current Trends in Programming Methodology Vol. IV, Prentice Hall, 1978, 80–145.
H.A. Harman and J.V. Tucker, “Clocks Retimings, and the Formal Specification of a UART,” in G. J. Milne (ed.), The Fusion of Hardware Design and Verification, North-Holland, Amsterdam, 1988, 375–396 (Proceedings of the IFIP WG 10.2 Working Conference, Glasgow, 1988).
Fredrick J. Hill and Gerald R. Peterson, Introduction to Switching Theory and Logical Design, (3rd ed.) John Wiley and Sons, New York, 1981.
Steven D. Johnson, “Applicative Programming and Digital Design”, Eleventh Annual ACM Symposium on Principles of Programming Languages (1984) 218–227.
Steven D. Johnson, “Digital Design in a Functional Calculus,” in: G.J. Milne and P.A. Subrahmanyam (eds.), Formal Aspects of VLSI Design, Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1986 (Proceedings of the 1985 Workshop on VLSI, Edinburgh).
Steven D. Johnson, Synthesis of Digital Designs from Recursion Equations, The MIT Press, Cambridge, 1984.
Steven D. Johnson, Bhaskar Bose, and C. David Boyer, “A Tactical Framework for Digital Design,” in VLSI Specification, Verification and Synthesis, (eds.) Graham Birtwistle and P.A. Subramanyam, Kluwer Academic Publishers, 1987, 349–384 (proceedings of the 1987 Calgary Hardware Verification Workshop).
Steven D. Johnson, Bhaskar Bose and Robert W. Wehrmeister, “On the Interplay of Hardware Synthesis and Hardware Verification: Experiments with the FM8501 Microprocessor Description,” submitted.
Jacques Loeckx and Kurt Sieber, The Foundations of Program Verification, John Wiley and Sons, Chichester, 1984.
George J. Milne, “CIRCAL and the Representation of Communication, Concurrency, and Time,” ACM Transactions on Programming Languages and Systems7:270–298 (1985).
Mary Sheeran, “Retiming and Slowdown in Ruby,” in G. J. Milne (ed.), The Fusion of Hardware Design and Verification, North-Holland, Amsterdam, 1988, 289–308 (Proceedings of the IFIP WG 10.2 Working Conference, Glasgow, 1988).
Mary Sheeran, μFP, and Algebraic for VLSI Design, D. Phil. Thesis, Programming Research Group Monograph PRG-39, Oxford University, 1983.
P.A. Subrahmanyam, “Contextual Constraints, Temporal Abstraction and Observational Equivalence in VLSI Design,” in G. J. Milne (ed.), The Fusion of Hardware Design and Verification, North-Holland, Amsterdam, 1988, 159–R184 (Proceedings of the IFIP WG 10.2 Working Conference, Glasgow, 1988).
Franklin P. Prosser and David E. Winkel, The Art of Digital Design (2nd ed.) Prentice-Hall, Englewood Cliffs, 1987.
Glynn Winskel, “A Compositional Model of MOS Circuits,” in VLSI Specification, Verification and Synthesis, (eds.) Graham Birtwistle and P.A. Subramanyam, Kluwer Academic Publishers, 1987, 323–347 (proceedings of the 1987 Calgary Hardware Verification Workshop).
Wayne Wolf, personal communication.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Johnson, S.D. (1990). Manipulating logical organization with system factorizations. In: Leeser, M., Brown, G. (eds) Hardware Specification, Verification and Synthesis: Mathematical Aspects. Lecture Notes in Computer Science, vol 408. Springer, New York, NY. https://doi.org/10.1007/0-387-97226-9_33
Download citation
DOI: https://doi.org/10.1007/0-387-97226-9_33
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-97226-8
Online ISBN: 978-0-387-34801-8
eBook Packages: Springer Book Archive