Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCSISBN: 9780471704492
231 pages
March 2008

Description
This practical book provides a stepbystep, interactive introduction to formal verification of systems and circuits. The book offers theoretical background and introduces the application of three powerful verification toolsets: LOTOSbased CADP, Petri nets–based PETRIFY, and CCSbased CWB. The book covers verification of modular asynchronous circuits, alternatingbit protocols, arbiters, pipeline controllers, updown counters, and phase converters, as well as many other verification examples.
Using the given detailed examples, exercises, and easytofollow 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.
Table of Contents
1. Introduction 1
1.1 EventBased Approach 2
1.2 EventBased Systems 2
1.3 Types of Verification 2
1.4 Toolsets Used 3
1.5 LevelBased 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 CElement 23
3.1.1 The 2Input CELCircuit 23
3.1.2 The 3Input CELCircuit 25
3.1.3 The 4Input CELCircuit 26
3.2 The XORGate 26
3.2.1 The 2Input XORGate 26
3.2.2 The 3Input XORGate 27
3.3 TOGGLES 29
3.4 ModuloN Transition Counters 30
3.4.1 ModuloN Transition Counter Specification 30
3.4.2 ModuloN Transition Counter Implementations 30
3.5 Modular Networks 31
3.6 Propositional Logic: A Review of Known Concepts 33
3.6.1 Logical Operators 34
3.6.2 Proving Logical Equivalences 35
3.6.3 Tautologies and the EQUIV Operator 36
3.7 Selected Solutions 36
3.8 References 37
4. Introducing LOTOS 39
4.1 From Blot to Basic LOTOS 39
4.1.1 Recursion 40
4.2 Some Semantics 41
4.3 From LTS to LOTOS 42
4.4 Comparing Parallel Operators 43
4.5 Sequential Composition 44
4.6 Hiding 44
4.7 Equivalences and Preorders 44
4.8 About CADP 45
4.8.1 Getting Started with CADP 45
4.8.2 Verifying Equivalences and Preorders Using CADP 46
4.8.3 Generating LTS of Choice Using CADP 47
4.8.4 Generating LTS of Recursion Using CADP 48
4.9 Full LOTOS—An Introduction 49
4.9.1 The FullLOTOS NOTGate Example 49
4.9.2 The NonTerminating NOTGate 51
4.9.3 The Max Specifications 52
4.10 The Regular MuCalculus (RMC) 53
4.10.1 Introducing RMC by Examples 53
4.11 Further Reading 55
4.12 Selected Solutions 56
4.13 References 57
5. Introducing Petri Nets 59
5.1 About Petri Nets 59
5.1.1 Petri Graphs and Petri Nets 59
5.1.2 Enabling and Firing 60
5.1.3 Another Definition of Petri Nets 61
5.2 About Languages 61
5.3 About PETRIFY 62
5.4 Illustrating Petri Nets 64
5.5 Labeled Nets 66
5.6 Bounded Nets 68
5.7 Observation Equivalence of LPNs 70
5.8 From Blot to Petri Nets 70
5.9 Liveness and Persistence 72
5.10 Simple Reduction Rules 72
5.11 Marked Graphs 74
5.12 A Simple Net Algebra 75
5.12.1 The Prefix Operator 75
5.12.2 The Choice Operator 77
5.12.3 The Star Operator 77
5.12.4 Parallel Compositions 79
5.13 ArcWeighted Nets 80
5.13.1 Enabling and Firing in ArcWeighted Nets 80
5.13.2 ArcWeighted Versus NonLabeled Nets 82
5.14 Readers–Writers System 83
5.14.1 A Readers–Writers System Net Representation 83
5.14.2 Verification of a Readers–Writers System 84
5.15 Inhibitor Nets 85
5.15.1 Introduction to Inhibitor Nets 85
5.15.2 The Expressive Power of Inhibitor Nets 85
5.16 True Concurrency 86
5.16.1 The PiLanguage 87
5.16.2 PiEquivalence 87
5.16.3 ConcurrencyPreserving Synthesis 88
5.17 Further Reading 89
5.18 Selected Solutions 89
5.19 References 93
6. Introducing CCS 95
6.1 About CCS 95
6.2 Operators ‘Prefix’ and ‘Sum’ 95
6.2.1 Semantics 96
6.3 Recursion 97
6.3.1 Semantics 97
6.4 Concurrency Operator 97
6.5 Equivalences 98
6.6 Restriction 98
6.7 CTL 99
6.7.1 Introducing CTL 99
6.8 The Concurrency Workbench (CWB) 100
6.8.1 The ‘sim’ and ‘compile’ Commands 100
6.8.2 Checking Equivalences 102
6.8.3 Checking Restrictions 103
6.8.4 HML Formulas 103
6.8.5 Equivalences—Counterexamples 104
6.8.6 More Equivalence Checking 105
6.8.7 Using the muCalculus 106
6.8.8 Using CTL 107
6.9 CCS and CWB Application Examples 109
6.9.1 The CCS XCELCircuit Example 109
6.9.2 The CCS CEL3Circuit Example 112
6.10 Further Reading 113
6.11 Selected Solutions 114
6.12 References 115
7. Verification of Modular Asynchronous Circuits 117
7.1 About Asynchronous Circuits 117
7.1.1 Modular Asynchronous Circuits 117
7.1.2 EdgeBased (Dynamic) Versus LevelBased Behavior 118
7.2 XORGates 118
7.2.1 LOTOS Representation of XORGate 118
7.2.2 Petri Net Representation of XORGate 119
7.2.3 CCS Representation of XORGate 119
7.3 CELCircuit 119
7.3.1 LOTOS Representation of CELCircuit 120
7.3.2 Petri Net Representation of CELCircuit 120
7.3.3 CCS Representation of CELCircuit 120
7.4 Other Modules 121
7.4.1 Inverter 121
7.4.2 ICELElement 121
7.4.3 TOGGLE 122
7.4.4 CALL 122
7.5 Module Extensions 123
7.5.1 XORk (k . 2) Modules 123
7.5.2 CELk (k . 2) Modules 123
7.5.3 TOGk (k . 2) 124
7.6 Modular Networks 124
7.7 Realizations 125
7.7.1 Introduction to Realization 125
7.7.2 TypeA Realization 125
7.7.3 TypeB Realization 126
7.7.4 TypeC Realization 128
7.7.5 TypeD Realization 130
7.7.6 DI Realization 131
7.8 Verification of Extended Modules 131
7.8.1 Verification of XORk (k . 2) Modules 132
7.8.2 Verification of CELk (k . 2) Modules 135
7.8.3 Verification of TOGk (k . 2) Modules 137
7.9 Verification of Parallel Control Structures 137
7.10 Further Reading 140
7.11 Selected Solutions 140
7.12 References 146
8. Verification of Communication Protocols 147
8.1 Introduction 147
8.2 Two Simple Communication Protocols 147
8.2.1 Simple Communication Protocol SCP 148
8.2.2 Simple Communication Protocol SCP1 148
8.3 The Alternating Bit (AB) Protocol 149
8.3.1 Introduction 149
8.3.2 The Reliable Channel Case 149
8.3.3 The Unreliable Channel Case 151
8.4 Further Reading 156
8.5 Selected Solutions 156
8.6 References 157
9. Verification of Arbiters 159
9.1 Introduction 159
9.2 A Random Arbiter (RGDA) 159
9.2.1 Verifying RGDA Using LOTOS 160
9.2.2 Verifying RGDA Using Petri Nets 163
9.2.3 Verifying RGDA Using CCS 165
9.3 A TokenRing Arbiter 167
9.3.1 A Petri Net Representation of a TokenRing Arbiter 167
9.3.2 Verification of a TokenRing Arbiter Using Petri Net 168
9.4 Further Reading 168
9.5 Selected Solutions 169
9.6 References 171
10. More Verification Case Studies 173
10.1 Verification of Combinational Logic 173
10.1.1 The AND Gate 173
10.1.2 Composite Gates 175
10.2 Verification of Asynchronous Pipeline Controllers 177
10.2.1 Introduction 177
10.2.2 Latch Control Unit 178
10.2.3 Phase Converters 181
10.3 Verification of Producer–Consumer Systems 183
10.3.1 Introduction 183
10.3.2 Verifying Producer–Consumer Systems Using Petri Nets 183
10.3.3 Occurrence Counts 184
10.3.4 Verifying the Producer–Consumer System Using Occurrence Counts 184
10.3.5 Verifying Producer–Consumer Systems Using LOTOS 185
10.3.6 Verification of MultipleProducer MultipleConsumer Systems 186
10.4 Verification Based on Design Approaches 188
10.4.1 Synthesis Approach #1 188
10.4.2 Synthesis Approach #2 189
10.4.3 Extending the Synthesis Method by Adding XOR Modules 190
10.4.4 A Decomposition Approach 191
10.5 Verification of Toggles and Transition Counters 193
10.5.1 Verification of kToggles 193
10.5.2 Verification of Counters without Outputs 194
10.5.3 Verification of Up–Down Counters with Output 196
10.5.4 Verification of ModuloN Transition Counters 196
10.6 Vending Machines Verification—Revisited 199
10.6.1 Verifying Vending Machines VeMa Using CCS 199
10.6.2 Verifying Vending Machines VeMa Using LOTOS 200
10.7 PiRealizations 201
10.7.1 More on Modular Networks 202
10.7.2 Introducing Circuits 203
10.7.3 Concurrent Behavior of Circuits 204
10.7.4 PiSpecifications of Circuits 205
10.7.5 Simple Verification Examples 206
10.7.6 Applying Net Algebra 206
10.7.7 Another Verification Example 207
10.7.8 Some Pi Propositions 209
10.8 A Comparison of Equivalence Relations 210
10.8.1 An Equivalence Theorem 210
10.8.2 An Application of the Equivalence Theorem 211
10.9 Selected Solutions 211
10.10 References 223
11. Guide to Further Studies 225
11.1 Verification of Telecommunication Systems 225
11.1.1 Plain Old Telephone System (POTS) 225
11.1.2 Advanced Telephone Systems 226
11.1.3 ISDN Telephony 226
11.2 Verification Using Colored Petri Nets 226
11.3 Verification of Traffic Signal Control Systems 226
11.4 References 227
Index 229
Author Information
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.
Buy Both and Save 25%!
Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS (US $130.00)
and LargeScale Computing Techniques for Complex System Simulations (US $111.95)
Total List Price: US $241.95
Discounted Price: US $181.46 (Save: US $60.49)