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.