THE USE OF PETRI NETS FOR THE DESIGN AND VERIFICATION OF ASYNCHRONOUS CIRCUITS AND SYSTEMS
Alex Kondratyev, Michael Kishinevsky, Alexander Taubin, Jordi Cortadella, Luciano Lavagno · Journal of Circuits Systems and Computers · 1998
Petri nets46,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.