next up previous contents
Next: Part II (General) of Up: Easter Term 2001: Part Previous: E-Commerce

Specification and Verification II

Lecturer: Professor M.J.C. Gordon (mjcg@cl.cam.ac.uk)

No. of lectures: 12

Prerequisite course: Specification and Verification I


Aims


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.


Lectures

Objectives


Students successfully completing the course will have been introduced to the following topics. The use of Floyd-Hoare logic for verifying HDL programs. Event, trace and cycle 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. Early quantification. Expressing properties in CTL. Model checking.


Recommended books


None (comprehensive notes supplied).


next up previous contents
Next: Part II (General) of Up: Easter Term 2001: Part Previous: E-Commerce
Christine Northeast
Wed Sep 20 15:13:44 BST 2000