Computer Laboratory – Course material 2008–09: Specification and Verification II

Next: System-on-Chip Design Up: Lent Term 2009: Part Previous: Specification and Verification I Contents

Specification and Verification II

Lecturer: Professor M.J.C. Gordon

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 including manual deductive methods and automatic techniques (including model checking). The similarities and differences with software verification will be discussed.

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. Modelling on different timescales. Temporal abstraction. [2 lectures]
Property specification and checking. Introduction to temporal logic and model checking algorithms. [4 lectures]

Objectives

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. 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. Formal treatment of simple CMOS examples and edge-triggered D-type registers. The strengths and weaknesses of various transistor models. Temporal abstraction. Transition systems. Expressing properties in temporal logic (including CTL, LTL and PSL). Symbolic modelling with BDDs. Model checking.

Recommended reading

Comprehensive notes supplied.

Next: System-on-Chip Design Up: Lent Term 2009: Part Previous: Specification and Verification I Contents