Advanced Tutorial on Hardware Design and Petri Nets

Material for public:

Handouts:
Main part (PDF) (1.5 MB)
Performance Section(PDF) (724 Kb)

Powerpoint slides (with some animation): All slides (zipped)

Intended audience:

Researchers, PhD students working in the area of digital system design (looking for methods and tools to aid their design techniques), and those working with Petri nets and models of concurrency (looking for applications to their modelling, analysis, verification and synthesis methods).

Aims:

We aim at familiarising the audience with the basic ideas, techniques, and tools and developing practical skills in using Petri nets for modelling, analysing, verifying and synthesising digital systems, with the emphasis on asynchronous circuits.

Contents:

Hardware Modelling

Here we will consider methods for representing the behaviour of (predominantly asynchronous) hardware using Petri nets. The behaviour of circuits will be described at different levels of abstraction, ranging from high level models of processors down to the models of low level switching behaviour of logic circuits. Petri nets with suitable interpretation, such as Signal Transition Graphs (STGs) will be introduced. Problems with adequate capturing of hardware with analogue components, such as arbiters and circuits with hazards, as well as circuits with timing conditions will also be addressed.

Synthesis of Asynchronous Circuits

We will define the overall problem of synthesis of asynchronous circuits from their formal specifications based on interpreted Petri nets. The logic synthesis from STGs will be considered to a greater detail, covering steps involving the transformation of behavioural models at the STG and state graph levels. Some problems involved in efficient synthesis of large-scale asynchronous controllers will be discussed.

Analysis and Verification of Asynchronous Circuits

Techniques for compact representation of the state spaces generated by asynchronous circuits, under bounded and unbounded delays, will be considered. These will be based on symbolic methods(such as BDDs) and partial orders (such as net unfoldings). Essential properties of circuits (such as hazard-freedom) and their interpretation in terms of the corresponding Petri net models will be defined. Methods for traversing the state spaces and analysing circuits (e.g. wrt speed-independence) will be presented. Problems involved the analysis of circuits under timing constraints will also be addressed.

Petri net models for Quasi-Static Scheduling in Codesign

We will discuss the problem of scheduling a concurrent process network with initially unbounded queues, in order to execute it on limited computational and storage resources. The model that we consider includes both data-dependent and control-dependent choice, concurrency and sequencing. Applications in the area of multi-media processing will be considered.

Other aspects of hardware design with Petri nets

We will overview the following main topics:

• relationship between Petri nets and Hardware Description Languages, such as VHDL and Verilog.
• use of Petri nets for analysis of performance of hardware structures
• real-life design examples involving use of Petri nets

Schedule of the tutorial