0.1
Course Contents
0.2 The
Importance of Formal Approaches
0.3
Course Objectives
0.4
Intended Course Participants
Lecture 1 ñ Propositional Logic : A
Review of Known Concepts
1.1
Logical Operators
1.2
Proving Logical Equivalences
1.3
Some Simple Exercises
1.4
Tautologies and the EQUIV Operator
1.5 The
Propositional Calculus as Formal System
1.6
More Exercises
1.7
References
Lecture 2
ñ LP (the Larch Prover)
2.1
Starting LP
2.2
Self-Test Exercises
2.3
Getting Online Help
2.4 The
XOR Operator
2.5
More Self-Test Exercises
2.6
References
Lecture 3
ñ Gates and Gate Networks
3.1
Simple Gates
3.2
Gate Networks
3.3
Applying Existential Quantifiers
3.4
Verification by Implication
3.5
Self-Test Exercises
3.6
References
Lecture 4
ñ Combinational Adder Circuits
4.1
Half Adder
4.2
Full Adder (Version 1)
4.3
Full Adder (Version 2)
4.4
More Exercises
4.5
References
Lecture 5
ñ Parameterized Networks
5.1
Structural Induction
5.2
Defining the Natural Numbers
5.3
Using Induction ñAnother Example
5.4
A Parity Checking Circuit
5.5
Exercises
5.6
References
Lecture 6
- Synchronous Circuits
6.1
LP Revisited
6.2
From Parameterized Networks to Synchronous Circuits
6.3
A Simple LOCK Circuit
6.4
A Simple Counter
6.5
A Sequential Comparator
6.6
A Sequential Adder
6.7
Exercises
6.8
References
Lecture 7
ñ Asynchronous Circuits : The
Modular Approach
7.1
Asynchronous Circuits: Advantages and Problems
7.2
The Modular Approach
7.3
Dynamic Behaviour
7.4
An Illustative Example
7.5
References
8.1
Processes
8.2
Prefixing
8.3
Observable Actions
8.4
Observation Equivalence
8.5
Recursion
8.6
Choice
8.7
Labeled Transition Systems
8.8
References
9.1
Getting Started
9.2
Equivalences
9.3
Recursion
9.4
Choice
9.5
From LTS to LOTOS
9.6
Parallel Operators
9.7
Hiding
9.8
Solved Exercises
9.9
Additional Exercises
9.10
References
10.1 A
Simplified LOTOS-Based Notation
10.2
Two-Input XOR-Gate
10.3
C-Element (CEL)
10.4
Other Modules
10.5
Modular Networks
10.6
Exercises
10.7
References
Lecture 11
ñ Verification of Asynchronous
Circuits
11.1
The Definition of Realization
11.2
Informal Motivation
11.3
Verifying Conditions 1,2
11.4
About Condition 3
11.5 A
Verification Example ñ Modulo-3 Transition Counter
11.6 A
Verification Exercise ñ The 3-TOGGLE
11.7
Up-Down Counters
11.8
Further Exercises
11.9
References
12.1
Introducing Petri Nets
12.2
Enabling and Firing
12.3
About Languages
12.4
PETRIFY
12.5
Some Solved Exercises
12.6
Additional Exercises
12.7
References
Lecture 13 - More on Petri Nets and PETRIFY
13.1
Another Definition of Petri Nets
13.2
Labeled Nets
13.3
Bounded Nets
13.4
Liveness
13.5
Persistence
13.6
Some Simple Reduction Rules
13.7
Marked Graphs
13.8
Observation-Equivalent Nets
13.9
Parallel Net Compositions
13.10 Some Solved
Exercises
13.11 Some
Self-Test Exercises
13.12 References
Lecture 14
ñ Net-Based Approach to Asynchronous Modules
14.1
XOR-Gates
14.2
CEL-Modules
14.3
TOGGLE
14.4
References
Lecture 15
ñ Net-Based Verification of
Asynchronous Circuits
15.1
The Net-Based Concept of Realization
15.2
Parallel Net Composition ñ Uniquely Labeled Nets
15.3
Multiply Labeled Nets
15.4
Observation-Equivalent Nets
15.5 A
Verification Example
15.6
References
Lecture 16
ñ Symbolic Model Checking
16.1
Introduction
16.2
CTL
16.3
SMV-Examples
16.3.1 An Introductory
Example
16.3.2 A Second Example
16.3.3 A Third Example
(the LOCK circuit)
16.4
Exercises
16.5
References
Lecture 17
ñ A Guide to Further Studies
17.1
Comparing Different Realization Concepts
17.2 CSP
17.3 HOL
17.4 Other
Theorem-Proving Approaches
17.5 Model
Checking ñ Theoretical Aspects
17.6
References
