This project is funded by the German Research Council (DFG).
We model globally asynchronous - locally synchronous (GALS) systems, a special kind of circuits (GALS circuit). Usually, a GALS circuit is defined as a set of locally synchronous modules communicating with each other via asynchronous wrappers. A wrapper generates the clock signal for its module and realizes the communication between modules.
The idea of the GALS approach is to combine the advantages of synchronous and asynchronous design methodologies while avoiding their disadvantages: The clock distribution in a GALS circuit can be realized easier than in a synchronous circuit. Further advantages are usually lower power consumption and electro-magnetic interference (EMI). These aspects are reasons why GALS circuits are used in systems for mobile communication and System-on-a-chip (SoC).
We build a model that describes module and wrapper (especially the transition between module and wrapper). Our model is a Petri net, because Petri nets can model synchronous systems by sequential runs and asynchronous systems by distributed runs.
Designers of GALS systems are interested in properties of their circuit. We distinguish functional properties (liveness and safety properties) and non-functional properties (data throughput, performance, and tolerance in terms of clock rate changes). In order to verify all these properties we develop a suitable model for every property. Furthermore we work out verification techniques to prove the (non-)existence of these properties.
For example, we have built a model to analyse a wrapper for possible hazards (that is a signal of the wrapper holds an undefined value). In the Petri net model this question is reduced to the reachability of a marking which is a model checking problem. In general functional properties can be reduced to a model checking problem. The proof of non-functional properties is a more difficult task, because present models and verification techniques seem to be unsuitable.