Symbolic Time Separation of Events

We extend the TSE~\cite{Hulgaard95} 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 main 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. 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.