This paper presents a symbolic approach for the analysis of bounded Petri nets. The structure and behavior of the Petri net is symbolically modeled by using Boolean functions, thus reducing reasoning about Petri nets to Boolean calculation. The set of reachable markings is calculated by symbolically firing the transitions in the Petri net. Highly concurrent systems suffer from the state explosion problem produced by an exponential increase of the number of reachable states. This state explosion is handled by using Binary Decision Diagrams (BDDs) which are capable of representing large sets of markings with small data structures. Petri nets have the ability to model a large variety of systems and the flexibility to describe causality, concurrency, and conditional relations. The manipulation of vast state spaces generated by Petri nets enables the efficient analysis of a wide range of problems, e.g., deadlock freeness, liveness, and concurrency. A number of examples are presented in order to show how large reachability sets can be generated, represented, and analyzed with moderate BDD sizes. By using this symbolic framework, properties requiring an exhaustive analysis of the reachability graph can be efficiently verified.

Asynchronous circuits can be modeled as concurrent systems in which events are interpreted as signal transitions. The synthesis of concurrent systems implies the analysis of a vast state space that often requires computationally expensive methods. This work presents new methods for the synthesis of speed-independent circuits from a new perspective, overcoming both the analysis and computation complexity bottlenecks. The circuits are specified by free-choice signal transition graphs (STGs), a subclass of interpreted Petri nets. The synthesis approach is divided into the following steps: correctness, binary coding, implementability conditions, and logic synthesis. Each step is efficiently implemented by applying a set of structural techniques that analyze STGs without explicitly enumerating the underlying state space. Experimental results show that circuits can be generated from specifications that exceed in several orders of magnitude the largest STGs ever synthesized-with over 10/sup 27/ states. Computation times are also dramatically reduced. Nevertheless, the quality of results does not suffer from the use of structural techniques.

This paper presents a novel approach for automatic test patterngeneration of asynchronous circuits. The techniques used for thispurpose assume that the circuit can only be exercised by applyingsynchronous test vectors, as is done by real-life testers.The main contribution of the paper is the abstraction of thecircuit's behavior as a synchronous finite state machine in such away that similar techniques to those currently used for synchronouscircuits can be safely applied for testing.Currently, the fault model being used is the input stuck-at model.Experimental results on different benchmarks show that our approachgenerates test vectors with high fault coverage.

This paper presents a set of sufficient conditions for the gate-level synthesis of speed-independent circuits when constrained to a given class of gate library. Existing synthesis methodologies are restricted to architectures that use simple AND-gates, and do not exploit the advantages offered by the existence of complex gates. The use of complex gates increases the speed and reduces the area of the circuits. These improvements are achieved because of (1) the elimination of the distributivity, signal persistency and unique minimal state requirements imposed by other techniques; (2) the reduction in the number of internal signals necessary to guarantee the synthesis; and finally (3) the utilization of optimization techniques to reduce the fan-in of the involved gates and the number of required memory elements.

In this paper, a review of methods for the solution of general bidiagonal systems of equations is done. Gaussian Elimination, the r-Cyclic Reduction family of algorithms and the Divide and Conquer algorithm are analyzed. A unified view of the three types of methods is proposed. The work is focussed on two basic aspects of the methods: parallelism and grain. The influence of the architecture of the target computer on the parallelism and grain of the methods is evaluated. In particular, vector processors are analyzed as target architecture and one vector processor of the Convex C-3480 is taken as a case study. For the special case of Divide and Conquer, a model is made in order to tune parallelism and grain for its optimal execution. Two conclusions can be outlined from the analysis of the methods. First, the execution time of the r-Cyclic Reduction family of algorithms is lower as r grows reaching a lower significative bound in r=9. This means that the classic use of Cyclic Reduction on vector computers is outdated from now on. Second, the higher rank versions of the r-Cyclic Reduction family of algorithms and the optimized version of Divide and Conquer behave similarly on vector computers.