Advertisement

The Semantics of Verilog Using Transition System Combinators

  • Gordon J. Pace
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

Since the advent of model checking it is becoming more common for languages to be given a semantics in terms of transition systems. Such semantics allow to model check properties of programs but are usually difficult to formally reason about, and thus do not provide a sufficiently abstract description of the semantics of a language. We present a set of transition system combinators that allow abstract and compositional means of expressing language semantics. These combinators are then used to express the semantics of a subset of the Verilog hardware description language. This approach allows reasoning about the language using both model checking and standard theorem proving techniques.

Keywords

Model Check Transition System Transition Relation Sequential Composition Parallel Composition 
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.
    P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In TACAS00, 2000.Google Scholar
  2. 2.
    S. Campos, E. Clarke, and M. Minea. The Verus tool: A quantitative approach to the formal verification of real-time systems. Lecture Notes in Computer Science, 1254, 1997.Google Scholar
  3. 3.
    S. Cheng, R. Brayton, R. York, K. Yelick, and A. Saldanha. Compiling Verilog into timed finite state machines. In 1995 IEEE International Verilog Conference (Washington 1995), pages 32–39. IEEE Press, 1995.Google Scholar
  4. 4.
    E. M. Clarke. Automatic verification of finite-state concurrent systems. Lecture Notes in Computer Science, 815, 1994.Google Scholar
  5. 5.
    R. Cleaveland, G. Lüttgen, and V. Natarajan. Priority in process algebra. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra. Elsevier, 2000. To appear.Google Scholar
  6. 6.
    John Fiskio-Lasseter and Amr Sabry. Putting operational techniques to the test: A syntactic theory for behavioural Verilog. In The Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS'99), 1999.Google Scholar
  7. 7.
    Mike Gordon, Thomas Kropf, and Dirk Hoffman. Semantics of the intemediate language IL. Technical Report D2.1c, PROSPER, 1999. available from http://www.cl.cam.ac.uk in /users/mjcg/IL/IL15.ps.
  8. 8.
    K. McMillan. Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers, 1993.Google Scholar
  9. 9.
    Gordon J. Pace and Jifeng He. Formal reasoning with Verilog HDL. In Proceedings of the Workshop on Formal Techniques in Hardware and Hardware-like Systems, Marstrand, Sweden, June 1998.Google Scholar
  10. 10.
    H. Sasaki. A Formal Semantics for Verilog-VHDL Simulation Interoperability by Abstract State Machine. In Proceedings of DATE’99 (Design, Automation and Test in Europe), ICM Munich, Germany, March 1999.Google Scholar
  11. 11.
    IEEE Computer Society. IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. IEEE Computer Society Press, Piscataway, USA, 1996.Google Scholar
  12. 12.
    P. F. Williams, A. Biere, E.M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In CAV00, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Gordon J. Pace
    • 1
  1. 1.Chalmers University of TechnologySweden

Personalised recommendations