ECE 598 SV Formal Hardware/SoC Verification

Grading policy

Project: 65%

Presentation on individually assigned topics: 15%

Exams: 15%

Summary of reading material: 5%

Summary of reading material

There will be reading material assigned before every class (roughly, although it may be 1 per 2 classes). This will typically be a seminal paper that describes the technique to be discussed in class. You will be required to submit a 1 page summary of the paper at the beginning of class. This is to ensure fruitful discussions.

Individually assigned topics

Students will present a summary of the papers assigned to them (2 per student) during a class period and lead the discussion. If you would like to present a topic of your choice, please discuss this with the instructor by Sep 5^th. It is in the interest of the class to bring about widespread exposure to diverse domains where verification is practiced. You are encouraged to contribute proactively to this classroom experience.

Course project

This is a project intensive course. Projects are intended to be research opportunities. Students are advised to start their projects from the 2^nd/3^rd week of class. Project topics can be very broad, and are not constrained to be in the hardware domain. Possible projects can include:

Implementing an efficient enhancement of a base algorithm learnt in class (eg: we will learn SAT based model checking algorithms, so you can implement the recent interpolant SAT technique)
Applying hardware verification techniques/tools to other domains (eg: embedded systems, domain specific software like middleware, communication systems etc)
Applying verification techniques from other domains to check complex hardware (eg: proof based calculi, faster decision procedures in other logics)
Applying formal methods to develop formal and semi-formal approaches to problems in allied fields (eg: hardware reliability, software testing)
Applying a combination of different hardware verification algorithms learnt in class through Synopsys and Cadence tools to check a non-trivial system (eg: a protocol implementation in Verilog/VHDL, pipelined processor RTL)

There will be a project related link on the website that can be updated online. You are expected to provide regular weekly updates. There will be two project review classes, where students will present their progress. The final project demonstration has to be shown to the instructor before Fall break. There will be a project report due on Dec 10^th.

You are highly encouraged to be innovative and creative with the project ideas and aim for a possible conference paper submission.

Course notes and textbook

There is no text book for the course. A comprehensive list of papers will be prescribed. Course notes will be put up for specific topics, but not for every class. Instruction will be on the blackboard, so transcribing notes is highly recommended.

Course schedule (tentative)

Aug 27^th	Introduction to Hardware Verification
Aug 29^th	Property checking: Safety vs Liveness Automata vs Logic Model specification: Kripke structures
Sep 1^st	Labor day. No class.
Sep 3^rd	Temporal logics: CTL and LTL
Sep 5^th	Reachability analysis Tableau construction
Sep 8^th	Symmetry reductions
Sep 10^th	Partial order reductions BDD based verification
Sep 12^th	Symbolic model checking
Sep 15^th	Boolean satisfiability and constraint solving
Sep 17^th	SAT based model checking
Sep 19^th	Symbolic simulation
Sep 22^nd	Symbolic Trajectory Evaluation
Sep 24^th	Compositional verification (Take home) Exam 1 assigned
Sep 26^th	Abstraction based verification
Sep 29^th	Counterexample guided abstraction refinement
Oct 1^st	Theorem proving techniques ACL2 for floating point verification
Oct 3^rd	Processor verification using ACL2
Oct 6^th	Project progress reviews
Oct 10^th	Combinational equivalence checking
Oct 13^th	Sequential equivalence checking using SAT and BDDs
Oct 15^th	Bisimulation, simulation relations
Oct 17^th	Hoare logic Arithmetic circuit checking using HOLs
Oct 20^th	High level verification of hardware RTL symbolic simulation
Oct 22^nd	Case study: Multiplier verification
Oct 24^th	Case study: Cache coherence protocol checking (Take home) Exam 2 assigned

The remaining portion of the schedule depends on the topics picked by students for individual presentations. The updated schedule will be on the website in the week of Sep 8^th. In the week of Nov 24^th, we may have a couple of guest lectures.

The possible topics for individual presentations include, but are not limited to:

· Probabilistic model checking

· Verification of distributed systems

· Verification of infinite state, hybrid or continuous time systems

· Correctness issues in multiprocessor systems

· Verification of real-time, embedded systems

· Application of formal methods to runtime verification/testing/fault tolerance (ATPG, assertion based checking etc)

Course summary

Let’s have fun!