We extend the time separations of events (TSE) timing analysis algorithm into the symbolic domain, that is, we allow symbolic variables to be used to specify unknown parameters of the model (essentially, unknown delays) and verification algorithms which are capable of identifying not just failure or success, but also the constraints on these symbolic variables which will ensure successful verification. The two contributions are (1) an iterative algorithm which continuously narrows down the domain of interest and (2) a practical method for reducing the representation of symbolic expressions containing minimizations and maximizations defined for a given domain. The algorithm applies to asynchronous circuits without conditional behavior. Although this may seem a severe restriction, this is a large and useful subclass which includes, e,g,, pipeline structures. We report experimental results for several asynchronous circuits to demonstrate that symbolic analysis is feasible and that the output provided is what a designer (or perhaps a synthesis tool) would often want to know.

The combinational logic-level equivalence problem is to determine whether two given combinational circuits implement the same Boolean function. This problem arises in a number of computer-aided design (CAD) applications, for example when checking the correctness of incremental design changes (performed either manually or by a design automation tool). This paper introduces a data structure called Boolean expression diagrams (BEDs) and two algorithms for transforming a BED into a reduced ordered binary decision diagram (OBDD). BEDs are capable of representing any Boolean circuit in linear space and can exploit structural similarities between the two circuits that are compared. These properties make BEDs suitable for verifying the equivalence of combinational circuits. BEDs can be seen as an intermediate representation between circuits (which are compact) and OBDD's (which are canonical). Based on a large number of combinational circuits, we demonstrate that BEDs either outperform or achieve results comparable to both standard OBDD approaches and the techniques specifically developed to exploit structural similarities for efficiently solving the equivalence problem. Due to the simplicity and generality of BEDs, it is to be expected that combining them with other approaches to equivalence checking will be both straightforward and beneficial.

This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs) which can represent any Boolean circuit in linear space and still maintain many of the desirable properties of BDDs. Two algorithms are described for transforming a BED into a reduced ordered BDD. One closely mimics the BDD apply-operator while the other can exploit the structural information of the Boolean expression. The efficacy of the BED representation is demonstrated by verifying that the redundant and non-redundant versions of the ISCAS 85 benchmark circuits are identical. In particular, it is verified that the two 16-bit multiplication circuits (c6288 and c6288nr) implement the same Boolean functions. Using BEDs, this verification problem is solved in less than a second, while using standard BDD techniques this problem is infeasible. BEDs are useful in applications where the end-result as a reduced ordered BDD is small, for example for tautology checking.

Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. Applications range from logic optimization of asynchronous digital circuits to evaluation of execution times of programs for real-time systems. We present an efficient algorithm to find exact (tight) bounds on the separation time of events in an arbitrary process graph without conditional behavior. This result is more general than the methods presented in several previously published papers as it handles cyclic graphs and yields the tightest possible bounds on event separations. The algorithm is based on a functional decomposition technique that permits the implicit evaluation of an infinitely unfolded process graph. Examples are presented that demonstrate the utility and efficiency of the solution. The algorithm will form a basis for exploration of timing-constrained synthesis techniques.>

Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. We present results of applying an efficient algorithm to solve this problem of three different application domains. These are: analysis of instruction execution times of an asynchronous multiprocessor, analysis of a high-performance mixed asynchronous/synchronous communication interface, and isochronic fork analysis in asynchronous circuit synthesis. The algorithm we use yields exact (tight) bounds on the separation time of events in an arbitrary process graph without conditional behavior. This class of graphs is quite large and includes graphs that are not strongly connected. The algorithm is based on a functional decomposition technique that permits the implicit evaluation of an infinitely unfolded process graph.

Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. Applications range from logic optimization of asynchronous digital circuits to evaluation of execution times of programs for real-time systems. We present an efficient algorithm to find exact (tight) bounds on the separation time of events in an arbitrary process graph without conditional behavior. The algorithm is based on a functional decomposition technique that permits the implicit evaluation of an infinitely unfolded process graph.>