Search in Book Reviews

This book is not intended for newcomers to hardware verification. I had been lectured for less than a semester each in VDM (for specification, and not necessarily for hardware); Z (as for VDM); and PVS (for hardware verification) before reading this book.

In each chapter, an advocate of a rival tool applied it to a subset of the same examples from IFIP WG 10.5 as the book's other tools for the sake of comparison. Some chapters contained code for these comparisons, others contained only prose thus thwarting comparison. Some coauthors admitted that their techniques are inferior for some of these examples. The appendix documenting the examples is incomplete referring to the Internet but the editor advised me "Finally it became so outdated that we took it from the internet".

One example is called both "Benchmark 17" (on Page 69) and "Benchmark 11" (on Page 71). This is one of many spelling errors in all chapters (except for the well spelt COSPAN chapter) so people involved in verification make mistakes.

Bad identifiers abound, e.g. on Page 93: "X , Y , Z are disjoint sets of variables, viz. the input, state, and output variables respectively." By the next page I couldn't remember which was the input; the state; nor the output.

Familiar characters are used bizarrely. Additionally inconvenience is caused due to the unusability of most of these characters in source code. E.g. on Page 13: a capital T sans serif "represents an inconsistent or both-true-and-false truth value". In fairness, ASCII notations outside of this book also have unconventional meanings (e.g. * for multiplication instead of convolution).

On Page 144 a long, error-prone piece of code

  <>

  <>+

  <>+

  ...

  <>+

After reading this book, I did not feel that I would choose a tool I did not already know.