Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Computer Science Tripos Syllabus - Specification and Verification II
Computer Laboratory > Computer Science Tripos Syllabus - Specification and Verification II

Specification and Verification II next up previous contents
Next: Part II (General) of Up: Easter Term 2005: Part Previous: E-Commerce   Contents

Specification and Verification II

Lecturer: Professor M.J.C. Gordon

No. of lectures: 12

Prerequisite course: Specification and Verification I


The aim of the course is to introduce modern work on formal hardware verification. Both manual deductive methods and automatic techniques (including model checking) will be discussed. Hardware description languages will be described and used to illustrate similarities and differences with software verification.


  • Introduction to formal methods for hardware. Use of HDLs (e.g. Verilog) versus mathematical logic. Specifying structure and behaviour. Parameterised designs. [4 lectures]

  • Logical models of transistors. Simple switch models. Threshold switching models. Unidirectional sequential models. Problems with existing methods. [2 lectures]

  • Sequential behaviour. Temporal abstraction. Temporal logic. [2 lectures]

  • Property specification and checking. Introduction to temporal logic and model checking algorithms. [4 lectures]


Students successfully completing the course will have been introduced to the following topics. The use and limitations of Floyd-Hoare logic for verifying HDL programs. Event and trace semantics of a simple Verilog-like HDL. The theory of words (bitstrings). Formal verification of adder and multiplier examples. The description of hardware directly in higher order logic. Modelling combinational and sequential behaviour. Representing behaviour with predicates. The strengths and weaknesses of various transistor models. Formal treatment of simple CMOS examples and edge-triggered D-type registers. Temporal abstraction. Transition systems. Modelling with BDDs. Expressing properties in temporal logic. Model checking.

Recommended books

None (comprehensive notes supplied).

next up previous contents
Next: Part II (General) of Up: Easter Term 2005: Part Previous: E-Commerce   Contents
Christine Northeast
Wed Sep 8 11:57:14 BST 2004