Overview

The objective of the course is to introduce the main formal verification methods of hardware/software systems. Topics to be covered include: formal logics for system verification (first-order logic, higher-order logic, and temporal logic), formal specifications, theorem proving systems, microprocessor verification, and system software verifications.

Topics Covered: Boolean logic, Predicate logic (optional), Satisfiability (SAT) problem, SAT-based equivalence checking, Symbolic simulation, reachability analysis of state machines, Binary decision diagrams (BDD), Linear temporal logic (LTL), Computation tree logic (CTL), CTL Fixpoint-based model checking, BDD-based symbolic model checking, Bounded model checking, and advanced verification topics.

Course structure:

• Lectures
• Homework
• Exams (midterm, final)
• Projects

Project structure:

• EDA tools from Synopsys are used for formal verification

Required TA Skills

1. Be very competent and confident with formal verification by using EDA design tools.
2. Be very competent and able to explain formal verification basis.
3. Know and be able to explain basic formal modeling and verification of digital systems.
4. Be very comfortable working with and helping students. The command of the English language must be good enough so that there are not communication issues when providing students with help.

TA Responsibilities

1. Give an introduction to the project, clarifying instructions and highlighting any important information students need to know.
2. Help students during each project, answering questions and checking each group’s progress.
3. Grade their submitted project reports in a timely manner and upload student scores and feedback to D2L.
4. Be available for an office hour outside of project time; be responsive to student email questions.
5. Be in contact with the instructor and keep them informed of any problems in the project.
6. There may be other responsibilities depending on the instructor such as holding exam review sessions, proctoring or grading exams, or other assistance to the instructor if requested.