Abstract
Various models of hardware have been proposed though virtually all of them do not model circuits adequately enough to support and provide a formal basis for many of the informal arguments used by designers of MOS circuits. Such arguments use rather crude discrete notions of strength—designers cannot be too finicky about precise resistances and capacitances when building a chip—as well as subtle derived notions of information flow between points in the circuit. One model, that of R. E. Bryant, tackles such issues in reasonable generality and has been used as the basis of several hardware simulators. However Bryant’s model is not compositional. These lectures introduce Bryant’s ideas and present a compositional model for the behaviour of MOS circuits when the input is steady, show how this leads to a logic, and indicate the difficulties in providing a full and accurate treatment for circuits with changing inputs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., An intuitionistic logic of computable functions. Copy of slides 1984.
Bryant, R.E., A switch-level model of MOS circuits. In VLSI ’81, Ed. J. Gray, Academic Press 1981.
Bryant, R.E., A switch-level model and simulator for MOS digital systems. IEEE Transactions on Computers C-33 (2) pp. 160–177, February 1984.
Cardelli, L., An algebraic approach to hardware description and verification. Ph.D. thesis, Comp.Sc.Dept., University of Edinburgh (1982).
Camilleri, A., Gordon, M., and Melham, T., Hardware verification using higher order logic. To appear in the proceedings of the IFIP International working conference, Grenoble, France, September 1986. Also available as a report 91 of the Computer Laboratory, University of Cambridge (1986).
Dijkstra, E.W., A discipline of programming. Prentice-Hall (1976).
Fourman, M.P., Verification using higher-order specifications and transformations. Department of Electrical Engineering, Brunei University (1986).
Fourman, M.P., and Scott, D.S., Sheaves and logic. In proc. of Durham conference on Applications of Sheaves 1977, Lecture notes in Math., Springer-Verlag 1979.
Gordon, M.J.C., LCF-LSM. Report no. 41 of the Computer Laboratory, University of Cambridge (1983).
Gordon, M.J.C., How to specify and verify hardware using higher order logic. Lecture notes, Computer Laboratory, University of Cambridge (1984).
Gordon, M.J.C., Why higher order logic is a good formalism for specifying and verifying hardware. Report no.77 of the Computer Laboratory, Cambridge University 1985.
Gordon, M.J.C., and Herbert, J., A formal methodology and its approach to a network interface chip. Report no.84 of the Computer Laboratory, Cambridge University 1985.
Grayson, R., Heyting-valued semantics. Proc. logic colloquium ’82, North-Holland (1984).
Harel, D., First-order dynamic logic. Springer Verlag Lecture Notes in Comp.Sc., vol. 68 (1979).
Hanna, F.K., and Daeche, N., Specification and verification using higher-order logic. Proc. IFIP WG 10.2, 7th. international conference on computer hardware description languages and their applications, Tokyo, Japan 1985, Koomen & Moto-oka (eds.), North-Holland (1985)
Hayes, J., Aunified switching theory with applications to VLSI design. Proc. IEEE 70 (10) pp. 1140–1155 Oct. 1982.
Bergstra, J.A., and Klop, J.W., A proof rule for restoring logic circuits. Integration 1 pp.161–178 (1983).
Mead, C., and Conway, L., Introduction to VLSI systems. Addison-Wesley (1980).
Mavor, J., and Denyer, P.B., Introduction to MOS design. Addison Wesley 1983.
Melham, T., Abstraction in hardware verification. Progress report and thesis proposal, Computer Laboratory, University of Cambridge (1985).
Milne, G., CIRCAL, TOPLAS April 1985.
Moszkowski, B., Executing temporal logic programs. Report no.71 of the Computer Laboratory, Cambridge University 1985.
Olderog, E., and Hoare, C.A.R., Specification-oriented semantics for communicating processes. ICALP 83, Springer Lecture Notes in Comp. Sc. vol. 154 (1983).
Plotkin, G.D., Types and partial functions. Lecture notes, Computer Science Dept., University of Edinburgh 1985.
Prawitz, D., Natural deduction. Almqvist and Wiksell 1985.
de Roever, W.P., The quest for compositionality. In the proceedings of the IFIP working conference, January 1985, North-Holland (1985).
Scott, D.S., Identity and existence in intuitionistic logic. In proc. of Durham conference on Applications of Sheaves 1977, Lecture notes in Math., Springer-Verlag 1979.
Sheeran, M., μFP an algebraic VLSI description language. D.Phil, thesis, Oxford 1983.
Stirling, C. Modal logics for communicating systems. Report CSR-193–85 of the Computer Science Dept., Univ. of Edinburgh (1985).
Winskel, G., A complete proof system for SCCS with modal assertions. In the proceedings of Foundations of Software Technology, Springer lecture notes in Comp.Sc. (1985).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Winskel, G. (1987). Models and logic of MOS circuits. In: Broy, M. (eds) Logic of Programming and Calculi of Discrete Design. NATO ASI Series, vol 36. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-87374-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-87374-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-87376-8
Online ISBN: 978-3-642-87374-4
eBook Packages: Springer Book Archive