Hardware Description and Verification
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
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.
- Peter J. Ashenden:
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
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,
- 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]
Koen Claessen and Mary Sheeran:
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
- To be read if Lava expressions make you puzzled. More
info on Haskell can be found at
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.