"Verification" refers to a process that aims to guarantee that a piece of software or hardware has certain properties. These properties might include: "implements the specified behaviour", "does not crash", "does not hang", or "always responds within so-many microseconds". This module will introduce you to techniques used to verify software and hardware. On the hardware side, you will see SystemVerilog testbenches and formal verification tools (actual tool TBD). On the software side, you will see interactive theorem-provers (Coq or Isabelle) and automatic software verification tools (Dafny).

On successful completion of the module you will be able to: 1. Validate the properties of small programs throught an automated software verification tool. 2. Argue how an interactive theorem prover works. 3. Validate the properties of small programs through a interactive theorem prover. 4. Consider the three pillars of hardware verification: stimulus, coverage and checking. 5. Produce a testbench, generate stimulus, measure coverage and write a checker. 6. Consider the principles of formal verification of hardware. 7. Validate the properties of a small RTL module through a formal verification tool.

Lecture 1: Introduction to software verification. What it is, where it is used, how it compares to testing, what are its fundamental limits. Lecture 2: Live demonstration of an automatic software verification tool being used to verify properties of a small program. Coursework 1: Using automatic software verification tool to verify properties of another small program. Lecture 3: Live demonstration of an interactive theorem prover being used to verify properties of a small program. Coursework 2: Using an interactive theorem prover to verify properties of another small program. Lecture 4: Introduction to hardware verification and its importance in the development cycle. The three pillars of hardware verification: stimulus, coverage and checking. Top-level versus constrained random unit-level verification. Lecture 5: The principles of building a testbench, with an introduction to SystemVerilog. Coursework 3: Using SystemVerilog to build a testbench, including a checker and constrained random test generator, and demonstrating that coverage metrics can be achieved for a small RTL module. Lecture 6: Formal methods for hardware verification. Writing SystemVerilog assertions (SVAs) and how these can be used for both RTL bring-up and bug-finding. Demonstration of a formal methods tool. Coursework 4: Write properties as SystemVerilog assertions and use a formal verification tool to prove these properties on the same RTL module as used in coursework 3.