Hardware Description and Verification

Literature

You are not required to buy any textbook for this course. We will make course materials available online, and mark them as [online] below. Read these documents!

As general reference for the course, you can use the Handbook on EDA for IC System Design, Verification, and Testing (ed. Scheffer, Lavagno, Martin).This is available as an e-Book via the Chalmers library Chalmers e-book collection (available from computers at Chalmers Chalmers, or by using your library card number). Search on CRCnetBASE. How much of this you need to look at depends on your background.

However, we also mention some other textbooks below in case you wish to consider buying them. See also the links page for further sources of information.

First part

Peter J. Ashenden: The Designer's Guide to VHDL.
This is the VHDL book, and it the most commonly used VHDL book in industry. Note all the useful supplementary material on the web page.

Suggested reading: Chapter 1-7, 8 (sect 1-4 briefly, 5 important), 11.1, 12, 20.1 (only for reference), 21.3, App A (briefly), App B-C (for reference).

Stefan Sjöholm, Lennart Lindh: VHDL för konstruktion.
This is an alternatively for those who speak Swedish. This book focuses on VHDL for synthesis, which we will not use in this course. Still, it describes VHDL well, and is a good (and cheaper) alternative to the previous book. Note that the book VHDL - en introduktion by the same authors doesn't cover everything needed in this course.

Suggested reading: chapter 1-5, 6 (except sect 6), 8 (sect 0, 1), 9 (sect 0-9), 12, 13 (sect 0), 14 (sect 1, 3, 4)

Jiri Gaisler: Notes on a Structured VHDL Design Method [online]
Cindy Eisner and Dana Fisman: A Practical Introduction to PSL.
This seems to be the book about the property specification language that we will use. I bought it on Amazon.co.uk, but it was expensive.
Alan J. Hu: Formal Hardware Verification with BDDs: An Introduction [online]
Carl-Johan Seger, An Introduction to Formal Hardware Verification [online]

Second part

Koen Claessen and Mary Sheeran: A Lava Tutorial [online] (PDF).
(For printing, you might want to use the shrunk version (PDF), with 2 pages put on one page.)
A Gentle Introduction to Haskell
To be read if Lava expressions make you puzzled. More info on Haskell can be found at haskell.org.
M. Sheeran, S. Singh and G. Stålmarck: Checking Safety Properties using Induction and a SAT-solver [online], FMCAD 2000.
K. Claessen, N. Een, M. Sheeran and N. Sörensson: SAT-solving in practice [online], WODES08.
This is a recently written tutorial paper (draft) that very briefly covers SAT-solving, bounded model checking and temporal induction, as well as giving lots of relevant references.
[ Home | News | Schedule | Literature | Assignments | Tools | Links | Course ] TH, March 2010