Detailed Syllabus:

Overview: Introduction to verification, Developing Verification strategies, Applying Verification strategies, E-standard Programming Constructs, RTL ports and interfaces, Modeling hardware interfaces with concurrency constructs, simulating testbenches using Fork-join, stimulus synchronization using conventional synchronization constructs like Mailboxes, Semaphores, regions and events.

Hardware Verification Languages: Fundamentals of HVLs, concurrency Issues, Class definitions and instantiations, tasks and functions, Concurrent techniques, Automatic Stimulus generation and randomized testing using HVLs, Building Transactors and Stubs, Result checking, Coverage and Regression, Debuggng

Advanced Functional Verification: RTL verification; Processor verification issues, functional verification using constraint modelling.

Basics of Formal Verification: Property Checking. Comparision with simulation based technique; Decision Diagrams, Use of CUDD

Summary: In this course we shall learn the following:

1. Verification Aims and Techniques

2. Simulation based verification

3. How to use Langauge e?

4. Basics of Formal Verification

Text Books:

Design Verification with 'e': By Samir Palnitkar.

Hardware Design Verification: Simulation and Formal Method-Based Approaches: By William K. Lam, Prentice Hall

Writing Testbenches: Functional Verification of HDL Models: By Janick Bergeron, Springer

Logic in Computer Science modelling and reasoning about systems: By Michael Huth and Mark Ryan, Cambridge

Presentations for the class:

Introduction to Verification.

Slides on Verilog.

Introduction (contd.)

The Specman Elite Tutorial : Verification using language 'e'.

Advanced Concepts in Simulation Based Verification.

Decision Diagrams and Equivalence Checking.

Introduction to Model Checking.


First Tutorial: Part A (submission deadline: 10.2.08)

First Tutorial: Part B (submission deadline: 10.2.08)

Second Tutorial (submission deadline: )

Third Tutorial (submission deadline: )

Quizes and Questions:

First Quiz

Second Quiz

Mid-Semester, 2008

End Semester, 2007

End Semester, 2008

Papers to Read:

An Overview on HDLs and HVLs

Using when subtyping effectively using Specman

Extracting FSM Coverage using Specman

The e-Language: A Fresh Separation of Concerns


Getting Started in 'e'

Verification of an arithmetic block to compute remainder of CRC-8

Transaction Level Test-Bench Writing

An Overview on Verilog Tasks and Functions

A Tutorial on Specman Elite

Specman Language Reference Manual

e- A Quick Reference