Read more
Informationen zum Autor Michael Yoeli, PhD , is Professor Emeritus in the Department of Computer Science, Technion, Israel. He is the author or editor of several books on digital networks and formal verification. His research interests include theory and applications of Petri nets, formal verification of hardware design, formal verification and synthesis of modular asynchronous networks, and computer-assisted analysis of parallel systems. He was awarded a Certificate of Acknowledgment by the Israel Section of the IEEE and the Israel Chapter of the IEEE Computer Society. Rakefet Kol, PhD , is a member of the Electrical Engineering Department, Technion, Israel. Her research interests include computer architectures, asynchronous design, formal verification of hardware designs, and software engineering. She is a senior member of the IEEE and a professional member of the ACM. Klappentext A Step-by-Step Guide to Verification of Digital SystemsThis 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, exercises, and easy-to-follow tutorials, complete with the downloadable toolsets available via referenced Web sites, this book serves as an ideal text in advanced undergraduate and graduate courses in computer science and electrical engineering. It is also valuable as a desktop reference for practicing verification engineers who are interested in verifying that designed digital systems meet specifications and requirements. Zusammenfassung This book provides a step-by-step interactive introduction to formal verification of systems and circuits. In view of the complexity of current parallel digital systems, a formal approach to their analysis and verification becomes essential. This text makes use of two powerful analysis tool sets: LOTOS-based CADP & Petri-Net based PETRIFY. Inhaltsverzeichnis 1. Introduction 1 1.1 Event-Based Approach 2 1.2 Event-Based Systems 2 1.3 Types of Verification 2 1.4 Toolsets Used 3 1.5 Level-Based Approach 3 1.6 Overview of the Book 3 1.7 References 5 2. Processes 7 2.1 Introduction 7 2.2 Examples of Processes and Basic Concepts 7 2.3 About Prefixing 10 2.4 Process Graphs 10 2.5 Choice Operator 11 2.6 Another Process Example 13 2.7 Equivalences 13 2.7.1 Strong Equivalence 13 2.7.2 Observation Equivalence 14 2.7.3 Some Additional Laws 15 2.8 Labeled Transition Systems (LTSs) 15 2.9 Parallel Operators 16 2.9.1 Parallel Composition 16 2.9.2 Synchronization Operator k (Blot Version) 16 2.9.3 Examples of Parallel Compositions 17 2.9.4 More Laws 17 2.9.5 Sample Proof 18 2.9.6 Interleaving Operator kj 18 2.10 Sequential Composition 18 2.11 Further Reading 19 2.12 Selected Solutions 20 2.13 References 21 3. From Digital Hardware to Processes 23 3.1 The C-Element 23 3.1.1 The 2-Input CEL-Circuit 23 3.1.2 The 3-Input CEL-Circuit 25 3.1.3 The 4-Input CEL-Circuit 26 3.2 The XOR-Gate 26 3.2.1 The 2-Input XOR-Gate 26 3.2.2 The 3-Input XOR-Gate 27 3.3 TOGGLES 29 3.4 Modulo-N Transition Counters 30 3.4.1 Modulo-N Transition Counter Specification 30 3.4.2 Modulo-N Transition Counter Implementations 30 3.5 Modular Networks 31 3.6 Propositional Logic: A Review of Known Concep...
