The use of Petri nets for the design and verification of asynchronous circuits and systems

Petri nets(46,37,45,48) are a powerful formalism for modeling concurrent systems. They are capable of implicitly describing a vast state space by a succinct representation which gracefully captures the notions of causality, concurrency and conflict between events. Petri nets have also been chosen by many authors as a formalism to describe the behavior of asynchronous circuits by interpreting the events as signal transitions, thus coining the term Signal Transition Graph (STG).(50,4) A design framework for asynchronous systems involves three main aspects: formal specification, verification and synthesis. In this paper we review the main techniques we have used to cover these aspects in recent years, with a special focus on asynchronous circuits.