====== Tutorials ======

===== Modelling causality and concurrency =====

In these tutorials you will learn how to use [[wp>Finite-state_machine|Finite State Machine]], [[wp>Petri_net|Petri net]], and other models to capture causality and concurrency relations between events.

{{page>tutorial:toc-modelling&inline}}

===== Design of asynchronous circuits =====

A Signal Transition Graph (STG) is basically a [[wp>Petri net]] whose transitions are labelled with signal events. This makes STG a convenient formalism for specification, synthesis and verification of [[wp>asynchronous circuit|asynchronous circuits]]. In this series of tutorials you will learn how to specify the intended behaviour of an asynchronous circuit using [[:overview:stg|Signal Transition Graphs]] plugin, synthesise its asynchronous implementation, capture the circuit schematic in [[overview:circuit|Digital Circuit]] plugin and formally verify it against the initial specification.

{{page>tutorial:toc-designing&inline}}

===== Other training materials =====
  * [[tutorial:design:basic_buck-wtg:start|Design of Waveform Transition Graph for basic buck controller]]
  * [[tutorial:model:d_flip_flop:start|Modelling D flip-flop with WTG guards]]
  * [[tutorial:model:instruction_decoder:start|Design of instruction decoder with WTG]]
  * [[tutorial:design:communication_fabrics:start|Analysis and Verification of Communication Fabrics]]
  * [[tutorial:model:investigation:start|Structured Occurrence Nets for Crime and Accident Scenes]]  
  * [[tutorial:design:wait2:start|Design of WAIT2 component]]