Advertisement

A hardware semantics based on temporal intervals

  • Joseph Halpern
  • Zohar Manna
  • Ben Moszkowski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

We present an interval-based temporal logic that permits the rigorous specification of a variety of hardware components and facilitates proving properties such as correctness of implementation. Conceptual levels of circuit operation ranging from detailed quantitative timing and signal propagation up to functional behavior are integrated in a unified way.

After giving some motivation for reasoning about hardware, we present the propositional and first-order syntax and semantics of the temporal logic. In addition we illustrate techniques for describing signal transitions as well as for formally specifying and comparing a number of delay models. Throughout the discussion, the formalism provides a means for examining such concepts as device equivalence and internal states.

Keywords

Temporal Logic Linear Temporal Logic Digital Circuit Predicate Symbol Propositional Variable 
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. 1.
    M. R. Barbacci. “Instruction Set Processor Specifications (ISPS): The notation and its applications.” IEEE Trans. Comp. C-30, 1 (Jan. 1981), 24–40.Google Scholar
  2. 2.
    A. Bernstein and P. Harter. “Proving real-time properties of programs with temporal logic.” Proc. 8-th Symp. on Operating Systems Principles, Pacific Grove, California, Dec., 1981, pp. 1–11.Google Scholar
  3. 3.
    R. Betancourt and E. J. McCluskey. Analysis of sequential circuits using clocked flip-flops. Tech. Rept. 82, Digital Systems Laboratory, Stanford Univ., Aug., 1975.Google Scholar
  4. 4.
    G. V. Bochmann. “Hardware specification with temporal logic: An example.” IEEE Trans. Comp. C-31, 3 (March 1982), 223–231.Google Scholar
  5. 5.
    M. A. Breuer and A. D. Friedman. Diagnosis and Reliable Design of Digital Systems. Computer Science Press, Inc., Woodland Hills, California, 1976.Google Scholar
  6. 6.
    A. Chandra, J. Halpern, A. Meyer, and R. Parikh. Equations between regular terms and an application to process logic. Proc. 13-th ACM Symp. on Theory of Computing, Milwaukee, Wisconsin, May, 1981, pp. 384–390.Google Scholar
  7. 7.
    H. Eveking. The application of Conlan assertions to the correct description of hardware, Proc. 5-th Int'l Conf. on Computer Hardware Description Languages, Kaiserslautern, West Germany, Sept., 1981, pp. 37–50.Google Scholar
  8. 8.
    M. Gordon. Register transfer systems and their behavior. Proc. 5-th Int'l Conf. on Computer Hardware Description Languages, Kaiserslautern, West Germany, Sept., 1981, pp. 23–38.Google Scholar
  9. 9.
    B. T. Hailpern and S. Owicki. Verifying network protocols using temporal logic. Tech. Rept. 192, Computer Systems Laboratory, Stanford Univ., June, 1980.Google Scholar
  10. 10.
    D. Harel. First-Order Dynamic Logic. Springer-Verlag, Berlin, 1979. No. 68 of Lecture Notes in Comp. Sci. Google Scholar
  11. 11.
    D. Harel, D. Kozen, and R. Parikh. Process logic: Expressiveness, decidability, completeness. 21-th Symp. on Foundations of Comp. Sci., Syracuse, New York, Oct., 1980, pp. 129–142.Google Scholar
  12. 12.
    G. E. Hughes and M. J. Cresswell. An Introduction to Modal Logic. Methuen and Co., Ltd., London, 1968.Google Scholar
  13. 13.
    L. Lamport. Specifying concurrent program modules. Opus 60, Comp. Sci. Lab., SRI International, June, 1981.Google Scholar
  14. 14.
    S. Leinwand and T. Lamdan. Algebraic analysis of nondeterministic behavior. Proc. 17-th Design Automation Conf., Minneapolis, June, 1980, pp. 483–493.Google Scholar
  15. 15.
    T. M. McWilliams. Verification of timing constraints on large digital systems. Proc. 17-th Design Automation Conf., Minneapolis, June, 1980, pp. 139–147.Google Scholar
  16. 16.
    Y. Malachi and S. S. Owicki. Temporal specifications of self-timed systems. In H.T. Kung, B. Sproul, and G. Steele, editors, VLSI Systems and Computations, pp. 203–212, Computer Science Press, Inc., Rockville, Maryland, 1981.Google Scholar
  17. 17.
    Z. Manna and B. Moszkowski. Temporal logic as a programming language, forthcoming.Google Scholar
  18. 18.
    Z. Manna and A. Pnueli. Verification of concurrent programs: the temporal framework. In R. S. Boyer and J. S. Moore, editors, The Correctness Problem in Computer Science, pp. 215–273, Academic Press, New York, 1981.Google Scholar
  19. 19.
    P. Meinen. Formal semantic description of register transfer language elements and mechanized simulator construction. Proc. 4-th Int'l Symp. on Computer Hardware Description Languages, Palo Alto, California, Oct., 1979, pp. 69–74.Google Scholar
  20. 20.
    B. Moszkowski. A temporal logic for multi-level reasoning about hardware. Proc. 6-th Int'l Symp. on Computer Hardware Description Languages, Pittsburgh, Pennsylvania, May, 1983.Google Scholar
  21. 21.
    B. Moszkowski. Reasoning about Digital Circuits. Ph.D. Thesis, Dept. of Comp. Sci., Stanford Univ., forthcoming.Google Scholar
  22. 22.
    A. C. Parker and J. J. Wallace. “SLIDE: An I/O hardware description language.” IEEE Trans. Comp. C-30, 6 (June 1981), 423–439.Google Scholar
  23. 23.
    D. A. Patterson. “Strum: Structured microprogram development system for correct firmware.” IEEE Trans. Comp. C-25, 10 (Oct. 1976), 974–985.Google Scholar
  24. 24.
    V. R. Pratt. Semantical considerations on Floyd-Hoare logic. 17-th IEEE Symp. on Foundations of Comp. Sci., Houston, Texas, Oct., 1976, pp. 109–121.Google Scholar
  25. 25.
    N. Rescher and A. Urquart. Temporal Logic. Springer-Verlag, New York, 1971.Google Scholar
  26. 26.
    R. L. Schwartz and P. M. Melliar-Smith. Temporal logic specification of distributed systems. Proc. 2-nd Int'l Conf. on Distributed Computing Systems, Paris, France, April, 1981, pp. 446–454.Google Scholar
  27. 27.
    R. L. Schwartz, P. M. Melliar-Smith, and F. H. Vogt. An interval logic for higher-level temporal reasoning: language definition and examples. Tech. Rept. CSL-138, Comp. Sci. Lab., SRI International, Feb., 1983.Google Scholar
  28. 28.
    A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Proc. 14-th ACM Symp. on Theory of Comp., San Francisco, California, May, 1982, pp. 159–168.Google Scholar
  29. 29.
    S. Y. H. Su, C. Huang, and P. Y. K. Fu. A new multi-level hardware design language (LALSD II) and translator. Proc. 5-th Int'l Conf. on Computer Hardware Description Languages, Kaiserslautern, West Germany, Sept., 1981, pp. 155–169.Google Scholar
  30. 30.
    A. D. Talantsev, “On the analysis and synthesis of certain electrical circuits by means of special logical operators.” Automation and Remote Control 20, 1959, pp. 874–883.Google Scholar
  31. 31.
    T. Wagner. Hardware Verification. Ph.D. Thesis, Dept. of Comp. Sci., Stanford Univ., 1977.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Joseph Halpern
    • 1
  • Zohar Manna
    • 2
    • 3
  • Ben Moszkowski
    • 2
  1. 1.IBM Research CenterSan JoseUSA
  2. 2.Department of Computer ScienceStanford UniversityStanfordUSA
  3. 3.Applied Mathematics DepartmentWeissmann Institute of ScienceRehovotIsrael

Personalised recommendations