Primary
- Papers and articles to be announced in class.
- Class notes.
Current Reading List
- Selected sections (dealing with topics covered in class)
from Petri nets: Properties, analysis and applications
, T. Murata, pp. 541-580 in "Proceedings of the IEEE",
Vol 77, No. 4, April 1989 (available in Central Library).
- Programming in VLSI: From Concurrent Processes to Delay-Insensitive
Circuits, A. J. Martin, pp 1-64 in
"Developments in Concurrency and Communication", Addison Wesley, 1997
(available in Central Library).
- Class lecture notes on specification and synthesis using STGs, and
algorithm for solving CSC conflicts.
- Selected sections from
A Region Based Theory for State Assignment in Speed-Independent
Circuits, J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno,
A. Kondratyev, pp. 793-812, IEEE Transactions on Computer-Aided Design
of Integrated Circuits and Systems, Vol. 16, No. 8, Aug 1997.
[PDF]
- Selected chapters (Chapter 3 -- in particular, sections 3.3.2, 3.3.3 and
3.3.4 -- and Chapter 4) from Luciano Lavagno's impressive
Ph.D. thesis for more on STG based synthesis.
- Ivan Sutherland's seminal paper on Micropipelines
[PDF]
- Class lecture notes on CTL, LTL and verification using
model checking.
- Selected sections from Alur and Dill's paper on A Theory of Timed
Automata . [Postscript].
You need to read from pages 4 to 11 of Alur and Dill's paper to
understand the nuts and bolts of timed automata. You may go through the
introductory material in pages 1-3 to get some perspective, but this
is not necessary if you're short on time. Also look at the nice
example given on Page 13 (Example 3.16).
- Chapter on Temporal Logics in the book "Model Checking", by Edmund
Clarke Jr., Orna Grumberg and Doron Peled, The MIT Press (pages 27-31).
References for the more interested ...
- Asynchronous Circuit Design,
Chris J. Myers
John Wiley and Sons
- Asynchronous Sequential Switching Circuits,
Stephen Unger
Wiley-Interscience, New York
- Communicating Sequential Processes,
C.A.R. Hoare
Prentice Hall International Series in Computer Science
- The Theory and Practice of Concurrency,
A. W. Roscoe
Prentice Hall International Series in Computer Science
- Proceedings of the IEEE - Special Issue on Asynchronous
Circuits and Systems, Feb 1999
- Hardware Design and Petri Nets,
A. Yakovlev, L. Gomes and L. Lavagno
Kluwer Academic Publishers
- Concurrent Hardware: The Theory and Practice of Self-Timed Design,
A. Kondratyev, A. Taubin and V. Varshavsky
John Wiley and Sons
|
| Date | Topics details |
|---|
| Dec 30 | Introduction, basic notion of synchronous and
asynchronous systems; globally synchronized
views of time. Notion of a system and its environment.
Delay models: delay insensitive,
quasi-delay insensitive, speed independent and
timed systmes |
| Jan 2 | Small examples of delay insensitive, quasi-delay
insensitive and timed systems. Petri Nets as a
mechanism of specifying behaviour at the interface
between a system and its environment. Petri Net
basics: definition, markings, rules for transition
firing, mathematical notation. Representing concurrency,
synchronization, choice/conflict, sequencing,
merge of events using Petri Nets. k-safeness and
1-safeness of Petri Nets |
| Jan 8 | Talk by Prof. Jordi Cortadella. Trace set of a Petri Net.
More on equivalence of k-safe and 1-safe Petri Nets |
| Jan 9 | Petri Nets: free choice, extended free choice, liveness.
1-safe Petri Nets and state transition diagrams:
comparison of benefits of each formalism. Going from
Petri Nets to state transition diagrams and vice versa.
Introduction to a CSP-based process algebra:
syntax and semantics. Finite and infinite processes.
Sequential composition, non-deterministic choice,
guarded actions, tail recursion for defining
infinite processes
|
| Jan 15 | Institute holiday |
| Jan 16 | More of process algebra syntax and semantics: parallel
or concurrent composition. Expressive equivalence of
process algebra described and Petri Nets. Converting
Petri Nets to process algebraic descriptions and vice
versa. Example of a scalable queue described using
process algebraic constructs.
|
| Jan 22 | Handshakes as a mechanism of communication: two and
four-phase handshakes. Notion of channels, ports,
active and passive handshakes. Martin's CHP
description of processes; their handshaking expansion.
Effect of placing handshaking actions at different
points in a sequence of handshakes.
Example of a sequencer process with a passive L
port and two active R (R1, R2) ports:
its CHP description.
|
| Jan 23 | Expansion of CHP of description of sequencer
into 2-phase handshakes. Production rules (PR):
definition, identifying PRs from a handshaking
expansion, naive implementation from PRs.
Implementation of sequencer and its environment
using wires (buffers) and a negation gate.
4-phase handshaking expansion of sequencer CHP
description; obtaining PRs from this expansion.
Stability and non-interference of PRs.
Interference among PRs obtained from 4-phase handshaking
expansion of the sequencer. Reshuffling of
handshaking actions, and how it helps remove
some of the interference between PRs.
|
| Jan 29 | Further reshuffling of 4-phase handshaking events
of sequencer. Illustration of how reshuffling can
help yield simpler designs. Strongest precondition
of an event in a process description. Mutually
exclusive strongest preconditions. Deriving stable
guards (strongest guards) from strongest
preconditions.
|
| Jan 30 | Tutorial 1: Toggle and Merge elements.
Combining Toggle and Merge elements to obtain
a 2-phase to 4-phase (or vice versa) handshake
converter.
|
| Feb 5 | Combining strongest preconditions of same event (action)
occurring at different points in a process description.
Mutually exclusive strongest preconditions:
necessary and sufficient conditions for existence
of a stable PR set. Deriving strongest and weakest
guards of an event.
|
| Feb 6 | Simplifying strongest guards of PRs using don't-care
sets from process description. Illustration
with simple sequencer having 4-phase handshakes.
Strengthening weakest guards of PRs by inspection,
while ensuring that there are
no conflicting assignments to the same variable/port.
Symmetrization of guards enabling assignment of
conflicting values to same variable/port.
Illustration with simple sequencer.
|
| Feb 12 | Decomposition of a process into an interconnection
of linear processes using specialized elements like
Merge, C-element (synchronizer), Arbiter. Notion of
waking up and going to sleep in the context of
processes.
|
| Feb 14 | More on decomposition of processes. Dealing with
concurrency, synchronization, choice
when decomposing a process. Simple examples
illustrating how different process descriptions
can lead to the same interconnection of basic
elements.
|