ACCU Home page ACCU Conference Page
Search Contact us ACCU at Flickr ACCU at GitHib ACCU at Google+ ACCU at Facebook ACCU at Linked-in ACCU at Twitter Skip Navigation

Search in Book Reviews

The ACCU passes on review copies of computer books to its members for them to review. The result is a large, high quality collection of book reviews by programmers, for programmers. Currently there are 1918 reviews in the database and more every month.
Search is a simple string search in either book title or book author. The full text search is a search of the text of the review.
    View all alphabetically
Hardware Verification: Methods and Systems in Comparison
Colin Paul Gloster
Appeared in:

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


is dismissed partially because "syntactically it is clumsy and not easy to generalize to an arbitrary value of n" but its replacement is sorely lacking a loop:





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