In these tutorials you will learn how to use Finite State Machine, Petri net, and other models to capture causality and concurrency relations between events.

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

• Design of Waveform Transition Graph for basic buck controller
• Modelling D flip-flop with WTG guards
• Design of instruction decoder with WTG
• Analysis and Verification of Communication Fabrics
• Structured Occurrence Nets for Crime and Accident Scenes
• Design of WAIT2 component