ECE 598 SV - Automatic Approaches to Hardware and Software Verification and Validation

Verification and validation are the most challenging problems facing system development today, presenting exciting opportunities for innovative, effective solutions. This course will introduce the student to verification and validation techniques to check hardware designs, systems-on-a-chip and embedded software. This course is accessible to those who do not have a formal methods/verification background. It provides a comprehensive treatment of practical applications of verification and validation techniques in contemporary environments. There will be extensive exposure (demos, homeworks, project) to verification and testing tools to familiarize students with the state-of-the-art in these tools.

The course will discuss automatic verification techniques such as: model checking, equivalence checking, BDD-based verification and testing methods, symbolic execution and SAT solving algorithms. Additionally the course will introduce recent successes with hardware verification methods (BDD-based, SAT based etc) in software test and debugging. A new component of the course is the addition of static analysis techniques for hardware verification as well as software validation. Automatic test patttern generation techniques in hardware will also be covered.

There will be 4 labs. A non-trivial system with hardware and software components (eg: Digital radio Mondiale module implemented in software with a Viterbi decoder implemented in hardware) will be decided at the beginning of class. Students will verify this design using the different algorithms discussed in class. The algorithms are implemented in the tools listed below:

a. Incisive (Cadence Inc., Available on EWS workstations)
b. b. Software static analysis tools (from Microsoft Research and Coverity )
c. Formality (Synopsys Inc., Available on EWS workstations)
d. SMV (Available for free download)
e. JPF, BLAST, CBMC (Available for download)

These tools provide an option for equivalence checking, SAT based model checking, BDD-based verification and validation techniques, static analysis of software using SAT, BDD and ATPG like methods and a software verification environment.

Project:
The project will involve a choice between the following options:
a. Students can implement an algorithm learnt in class (or enhancements to these algorithms), and verify the non-trivial design used in the labs using their prototype. If their implementation is able to perform better than an existing implementation due to some heuristics, they will be graded higher.
b. Students can verify a substantially larger design (eg: RTL of a protocol implementation, multiplier etc) or software than the one done in the labs using different algorithms in the tools, and prove overarching correctness theorems to stitch the proofs together. The relative complexity of the verification task chosen will determine the grading.

The project deliverables will comprise the following:
a. Project report (6-10 pages)
b. Project presentation (20 mins in class)