In: 97: Proceedings of the Workshop on Petri Nets in System Engineering (PNSE'97), Hamburg, September 25-26, 1997 / Farwer, B.; Moldt, D.; Stehr, M.-O.: Report FBI-HH-B-205, pages 123-134. Universität Hamburg, September 1997.
Abstract: Signal Transition Graphs (STGs) are net systems with an interpretation, modelling the behaviour of asynchronous digital circuits by sequences of changes of the circuit signals. Although they have became very popular, only restricted syntactical subclasses (free choice nets) are considered in general. Moreover, the analysis techniques applied to these models are essentially based on the state space obtained from the STG, giving rise to the classical state space explosion problem. In this paper we propose a model based on the STGs, that is a net system without interpretation allowing to represent the same circuit behaviour as a classical STG. This new model consists of the underlying net system of the STG plus a set of places representing the values of the circuit signals. Considering this model, we show how general structural analysis techniques can be applied to verify properties of the system, as consistency, CSC or USC. These analysis techniques avoid the construction of the state space. Moreover, we show that with this kind of model no restrictions on the kind of Petri nets to be used are needed.
Keywords: modelling asynchronous circuit behaviour; structural methods of verification; application of petri nets in asynchronous circuits; signal transition graphs.