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.
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. 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. Expressing properties in temporal logic. Model checking.
