personal or class-room use is granted without fee provided that copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication and its date appear, and notice is given that copying is

An important practical approach to automatic verification of finite state concurrent systems is temporal logic model checking.However, a major barrier towards wider application of such methods is the state explosion problem that often occurs during the composition of complex communicating systems.In addition to being large, many systems have very deep state spaces as well.In this paper, we propose an abstraction method based on time abstraction which can significantly reduce both the size as well as the depth of the state space that must be explored during model checking.It is especially suited for applications involving systems that are loosely coupled in the sense that communication activity is relatively sparse, such as applications involving DSPs, which have large intervals of autonomous processing, with communication activity in between.All properties expressible with the temporal logic CTL or CTL -X are strongly preserved under the proposed abstraction.In particular, we give a method that can replace a chain of states by a single state with a time label.The abstracted model is represented by means of a timed label transition system model.We give a composition algorithm for composing the individually time abstracted models to form a global model that can be converted back to a conventional, but potentially much reduced,state space suitable for model checking.Furthermore, a similar approach can be followed in dealing with wait states in which a system is idling while waiting for an escape signal.For many cases, our approach is successful in alleviating the state explosion problem that often arises in composition of communicating systems.

The SFG-tracing methodology addresses the automatic verification of digital synchronous circuit implementations as specified at the algorithmic level as signal- (SFG) or data flow graphs. The SFG-tracing methodology is a multi-level design verification paradigm that aims at bridging the gap between higher level specifications down to lower level implementations up to the transistor switch level. The concepts of the SFG-tracing methodology are illustrated by the automatic verification of a transistor level implementation of a small chip generated from its high level specification by the Cathedral-II silicon compiler. This application, although simple, includes a datapath, register files, a multi-branch micro coded controller, and additional circuitry as necessary for design for testability measures. This application illustrates the SFG-tracing verification methodology as applied to one member of a partitioned SFG behavioral specification. Experimental results on more complex, completely verified designs of 32000 transistors demonstrate the feasibility of the approach.>