Next: Business Studies
Up: Easter Term 2000: Part
Previous: Distributed Systems
Lecturer: Prof. 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
- 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]
- Introduction to proof mechanisation.
Model checking versus interactive proof. State of the art and
future prospects. [4 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: Business Studies
Up: Easter Term 2000: Part
Previous: Distributed Systems
Christine Northeast
Mon Sep 20 10:28:43 BST 1999