The Semantics of Verilog Using Transition System Combinators
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.
KeywordsModel Check Transition System Transition Relation Sequential Composition Parallel Composition
Unable to display preview. Download preview PDF.
- 1.P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In TACAS00, 2000.Google Scholar
- 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.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.E. M. Clarke. Automatic verification of finite-state concurrent systems. Lecture Notes in Computer Science, 815, 1994.Google Scholar
- 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.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.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.K. McMillan. Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers, 1993.Google Scholar
- 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.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.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.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