Advertisement

Models and logic of MOS circuits

  • Glynn Winskel
Conference paper
Part of the NATO ASI Series book series (volume 36)

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.

Keywords

Proof System Static Configuration Flow Relation Elimination Rule Proof Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [A]
    Abramsky, S., An intuitionistic logic of computable functions. Copy of slides 1984.Google Scholar
  2. [B1]
    Bryant, R.E., A switch-level model of MOS circuits. In VLSI ’81, Ed. J. Gray, Academic Press 1981.Google Scholar
  3. [B]
    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.CrossRefGoogle Scholar
  4. [C]
    Cardelli, L., An algebraic approach to hardware description and verification. Ph.D. thesis, Comp.Sc.Dept., University of Edinburgh (1982).Google Scholar
  5. [CGM]
    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).Google Scholar
  6. [D]
    Dijkstra, E.W., A discipline of programming. Prentice-Hall (1976).MATHGoogle Scholar
  7. [F]
    Fourman, M.P., Verification using higher-order specifications and transformations. Department of Electrical Engineering, Brunei University (1986).Google Scholar
  8. [FS]
    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.Google Scholar
  9. [Gor1]
    Gordon, M.J.C., LCF-LSM. Report no. 41 of the Computer Laboratory, University of Cambridge (1983).Google Scholar
  10. [Gor2]
    Gordon, M.J.C., How to specify and verify hardware using higher order logic. Lecture notes, Computer Laboratory, University of Cambridge (1984).Google Scholar
  11. [Gor3]
    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.Google Scholar
  12. [GH]
    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.Google Scholar
  13. [Gra]
    Grayson, R., Heyting-valued semantics. Proc. logic colloquium ’82, North-Holland (1984).Google Scholar
  14. [Ha]
    Harel, D., First-order dynamic logic. Springer Verlag Lecture Notes in Comp.Sc., vol. 68 (1979).MATHCrossRefGoogle Scholar
  15. [HD]
    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)Google Scholar
  16. [Hay]
    Hayes, J., Aunified switching theory with applications to VLSI design. Proc. IEEE 70 (10) pp. 1140–1155 Oct. 1982.Google Scholar
  17. [KB]
    Bergstra, J.A., and Klop, J.W., A proof rule for restoring logic circuits. Integration 1 pp.161–178 (1983).Google Scholar
  18. [MC]
    Mead, C., and Conway, L., Introduction to VLSI systems. Addison-Wesley (1980).Google Scholar
  19. [MD]
    Mavor, J., and Denyer, P.B., Introduction to MOS design. Addison Wesley 1983.Google Scholar
  20. [Me]
    Melham, T., Abstraction in hardware verification. Progress report and thesis proposal, Computer Laboratory, University of Cambridge (1985).Google Scholar
  21. [Mi]
    Milne, G., CIRCAL, TOPLAS April 1985.Google Scholar
  22. [Mos]
    Moszkowski, B., Executing temporal logic programs. Report no.71 of the Computer Laboratory, Cambridge University 1985.Google Scholar
  23. [OH]
    Olderog, E., and Hoare, C.A.R., Specification-oriented semantics for communicating processes. ICALP 83, Springer Lecture Notes in Comp. Sc. vol. 154 (1983).Google Scholar
  24. [P]
    Plotkin, G.D., Types and partial functions. Lecture notes, Computer Science Dept., University of Edinburgh 1985.Google Scholar
  25. [Pr]
    Prawitz, D., Natural deduction. Almqvist and Wiksell 1985.Google Scholar
  26. [deR]
    de Roever, W.P., The quest for compositionality. In the proceedings of the IFIP working conference, January 1985, North-Holland (1985).Google Scholar
  27. [S]
    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.Google Scholar
  28. [She]
    Sheeran, M., μFP an algebraic VLSI description language. D.Phil, thesis, Oxford 1983.Google Scholar
  29. [St]
    Stirling, C. Modal logics for communicating systems. Report CSR-193–85 of the Computer Science Dept., Univ. of Edinburgh (1985).Google Scholar
  30. [W]
    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).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1987

Authors and Affiliations

  • Glynn Winskel
    • 1
  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations