ELEC70056 Hardware and Software VerificationLecturer(s): Dr John Wickerson Aims
"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).
Learning Outcomes
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 principles of formal verification of hardware. 5. Validate the properties of a small RTL module through a formal verification tool. Syllabus
- Introduction to software verification. What it is, where it is used, how it compares to testing, What are its fundamental limits.
- Live demonstration of an automatic software verification tool being used to verify properties of a small program. - Coursework: Using automatic software verification tool to verify properties of another small program. - Live demonstration of an interactive theorem prover being used to verify properties of a small program. - Coursework: Using an interactive theorem prover to verify properties of another small program. - Introduction to hardware verification and its importance in the development cycle. Formal methods for hardware verification. Demonstration of a Formal methods tool. - Coursework: Using a Formal verification tool to prove properties of a small RTL module.N98Modu Exam Duration: N/A Exam contribution: 0% Coursework contribution: 100% Term: Autumn Closed or Open Book (end of year exam): N/A Coursework Requirement: Coursework only module Oral Exam Required (as final assessment): N/A Prerequisite module(s): None required Course Homepage: https://bb.imperial.ac.uk Book List:
|