Specification and Verification II

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

No. of lectures: 12

Prerequisite course: Specification and Verification I  

Introduction to formal methods for hardware.

Use of HDLs (e.g. Verilog) versus mathematical logic. Specifying structure and behaviour. Parameterised designs.

Logical models of transistors.

Simple switch models. Threshold switching models. Unidirectional sequential models. Problems with existing methods.

Sequential behaviour.

Temporal abstraction. Temporal logic applied to memory protocols.

Introduction to proof mechanisation.

Model checking versus interactive proof. State of the art and future prospects.

Recommended book:

Melham, T.F. (1993). Higher Order Logic and Hardware Verification: Cambridge Tracts in Theoretical Computer Science 31. Cambridge University Press.