This practical book provides a step-by-step, interactive introduction to formal verification of systems and circuits. The book offers theoretical background and introduces the application of three powerful verification toolsets: LOTOS-based CADP, Petri nets-based PETRIFY, and CCS-based CWB. The book covers verification of modular asynchronous circuits, alternating-bit protocols, arbiters, pipeline controllers, up-down counters, and phase converters, as well as many other verification examples.

Using the given detailed examples,...