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.


Property Specification Language Reference Manual

Questa Commands - Readme

Questa SIM User’s Manual

QuestaTM SV/AFV Tutorial

Questa Demo


NEW!! Demo of using Specman with Modelsim at RISE Lab

NEW!! Develop a Verification plan, Test cases in Specman and provide the verification results along with coverage for the ESI cache specification that can be obtained by clicking here . The verilog code for the same can be got by clicking here . Note that in the cache model given to you there are two caches each with only ONE cache line. All addresses shall map onto the same line. The associativity of the cache is also one. Very simple indeed!!!!


NEW!! Coverage-Oriented Verification

Verification of Translate Lookaside Buffer (TLB)


The Specification click here

The Presentation click here

The C++ code click here

NEW!! Develop a similar model with scenarios for the ESI cache design.


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