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, 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, including a Quick Start lecture on VHDL.

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 alternative 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. You should be able to access the book through the Chalmers library if you are on the Chalmers network.

Alan J. Hu: Formal Hardware Verification with BDDs: An Introduction [online]

Carl-Johan Seger, An Introduction to Formal Hardware Verification [online], UBC CS TR-92-13, 1992.

Learning Haskell

Here are some resources for those who have not seen Haskell before, and for those who have seen it but are rusty:

Learn you a Haskell, a light, funny read and a good place to start.

An interactive, online Haskell tutorial

Programming in Haskell by Graham Hutton This is an excellent introductory textbook. It is also accompanied by slides and by vidoes.

Real World Haskell for more information about practical appiications of Haskell.

Thanks to Anton Ekblad for good tips.

Second part (may be revised)

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.