Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

A Step-by-Step Guide to Verification of Digital Systems This practical book provides a step-by-step, interactiveintroduction to formal verification of systems and circuits. Thebook offers theoretical background and introduces the applicationof three powerful verification toolsets: LOTOS-based CADP, Petrinets-based PETRIFY, and CCS-based CWB. The book coversverification of modular asynchronous circuits, alternating-bitprotocols, arbiters, pipeline controllers, up-down counters, andphase converters, as well as many other verification examples. Using the given detailed examples, exercises, and easy-to-followtutorials, complete with the downloadable toolsets available viareferenced Web sites, this book serves as an ideal text in advancedundergraduate and graduate courses in computer science andelectrical engineering. It is also valuable as a desktop referencefor practicing verification engineers who are interested inverifying that designed digital systems meet specifications andrequirements.