Specification and Verification II

University of Cambridge Computer Laboratory

Principal lecturer: Prof Mike Gordon (mjcg@cl.cam.ac.uk)
Taken by: Part II
Number of lectures: 12
Lecture location: Lecture Theatre 2, William Gates Building
Lecture times: 12:00 on starting Friday, 25 April, 2003

IMPORTANT ANNOUNCEMENT

I will not be lecturing on Monday May 19 and Wednesday May 21.
Instead there will be lectures on Thu May 1 and Tue May 13.
The schedule is thus as follows:
 Lecture 01 Fri Apr 25
 Lecture 02 Mon Apr 28
 Lecture 03 Wed Apr 30
 Lecture 04 Thu May 01
 Lecture 05 Fri May 02
 Lecture 06 Mon May 05
 Lecture 07 Wed May 07
 Lecture 08 Fri May 09
 Lecture 09 Mon May 12
 Lecture 10 Tue May 13
 Lecture 11 Wed May 14
 Lecture 12 Fri May 16

Prerequisites: Specification and Verification I

Syllabus: Hoare Logic and hardware. Theory of words (bitstrings). Describing hardware directly in higher order logic. Representing behaviour with predicates. Combinational and sequential behaviour. Simple CMOS examples. Edge-triggered D-type register. Verification of adder and multiplier circuits. Comparison with HDL verification. Discussion of various transistor models. Temporal abstraction. Transition systems. Modelling with BDDs. Disjunctive partitioning (early quantification). Expressing properties in temporal logics (CTL, LTL, ITL, Sugar/PSL). Model checking. Event, trace and cycle semantics of a simple Verilog-like HDL.

Past exam questions

Course notes [ps | ps.gz | pdf ]
These notes contain general and background material for the course. Some of the material in them may not be covered in the lectures, and some additional detail and examples are only presented in the lectures. The online notes may change, and so differ from the printed version.

The examinable material is what is actually covered in the lectures.

Online slides:
(warning: slides for lectures not yet given might change)

Exercises: the two sets of exercises below cover approximately the first and second halves of the course.

Examples classes: examples classes will be run by Joe Hurd in FW11 at the following times:
 Monday 19 May between 2-4pm 
 Monday 26 May between 2-4pm 
In the second class Joe will also provide revision support for Specification and Verification 1.

Further reading