Verification of asynchronous circuits by Petri net unfoldings

In this paper we use the interpreted Petri nets (signal transition graph (STG) model) for a verification of asynchronous circuits. The main property in the analysis is the speed-independence of a circuit, i.e. the independence of circuit functioning from the delays of gates. The idea of analysis is based on the PN unfolding into an occurrence net. The improved method of unfolding is suggested, in which the size of the obtained description is always not larger than the size of a corresponding state graph. In terms of unfolding, the necessary and sufficient conditions for speed-independence are formulated. The algorithms of these conditions analysis are polynomial from the size of STG unfolding. The efficiency of the suggested algorithms is considered on the set of benchmarks.<>