This is an old revision of the document!

Synthesis and verification of asynchronous circuits

Familiarise yourself with the Signal Transition Graph plugin and Digital Circuit plugin before proceeding with these tutorials.

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.

Synthesis and verification of C-element (basic circuit, detail explanation)
Synthesis and verification of buck controller (medium complexity with some hints)
Synthesis and verification of VME bus controller (advanced material for individual work)