High level verification of (a)synchronous circuit descriptions

In the development of a silicon compiler, one has to choose if synchronous or selftimed systems should be generated. In the silicon compiler EASY, which is in development in this department, synchronous systems will be synthesised automatically. However, for large systems it may be profitable to split up the whole system into several smaller systems which interact with eachother. This interaction is in fact a matter of communication and this communication happens in an asynchronous way. Protoeals have to be designed for this interaction to assure the correct behaviour of the whole system. Therefore, such a protocol and the environment it is working in must be verified. Petri nets have been proven very useful in the verification of communication protocols. In that case, the verification can be done with help of petri net analysis methods. This method suits also very well for the silicon compiler, since the data structure of the higher levels of the silicon compiler can be mapped one to one onto a petri net. Also, this data structure neects only a slight extension to model asynchronous features. Therefore, as well as the functional description of the system as the protoeals can be written in the same way and this results in just one model which has to be verified. This method of verification gives good results. Ho wever, it is a rather space and time consuming analysis method, since all possible states of the system have to be computed. Therefore, some efforts are made for reducing the complexity of the state space. Since only that states which give new information about the behaviour of the system need to be computed, it is useful not to compute the redundant states. Such reductions are proposed and implemented. The result is a far less space and time consuming method for analysing petri nets. Therefore, this method can be used for the verification of the behaviour of a set of interacting systems in the silicon compiler. The verification does not only give an answer to the question whether a specified protocol has a correct behaviour or not, but may also give some hints for constraints. When these constraints are applied to the system, the behaviour of the protocol and its environment may be correct. These constraints have to be passed to the hardware synthesis phase of the silicon compiler to generate a circuit which fulfills the functional description.