An approach to symbolic timing verification

Symbolic timing verification is a critical tool in the development of higher-level synthesis tools. The authors present an approach to symbolic timing verification using constraint logic programming techniques. The techniques are quite powerful in that they not only yield simple bounds on delays but also relate the delays in linear inequalities so that tradeoffs are apparent. They model circuits as communicating processes and the current implementation can verify a large class of mixed synchronous and asynchronous specifications. The utility of the approach is illustrated with some examples