ELEC97107 (EE9-AO21) Hardware and Software Verification
Lecturer(s): Dr John Wickerson; Prof Peter Harrod
"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 students to techniques used to verify software and hardware. On the hardware side, we will see SystemVerilog testbenches and formal verification tools (Mentor Questasim and Cadence JasperGold). On the software side, we will see interactive theorem-provers (Isabelle) and automatic software verification tools (Dafny).
L1. Appraise the strengths, weakness, and limits of both formal verification and testing.
L2. Understand how an automated software verification tool works.
L3. Operate an automated software verification tool to verify properties of small programs.
L4. Discover how an interactive theorem prover works.
L5. Operate an interactive theorem prover to verify properties of small programs.
L6. Appraise the importance of a multi-layered approach to hardware verification in the development lifecycle.
L7. Consider the three pillars of hardware verification: stimulus, coverage and checking.
L8. Produce a testbench, generate stimulus, measure coverage and write a checker.
L9. Appreciate the principles of formal verification of hardware and how to write properties.
L10. Operate a formal verification tool and prove properties of a small RTL module.
Introduction to software verification. What it is, where it is used, how it compares to testing, what are its fundamental limits.
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.
The principles of building a testbench, with an introduction to SystemVerilog.
How an automatic software verification tool can be used to verify properties of a small program.
How an interactive theorem prover can be used to verify properties of a small program.
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.
Exam Duration: N/A
Coursework contribution: 100%
Closed or Open Book (end of year exam): N/A
Coursework only module
Oral Exam Required (as final assessment): N/A
Prerequisite module(s): None required
Course Homepage: https://bb.imperial.ac.uk