A TECHNIQUE FOR FINDING AND VERIFYING SPEED-DEPENDENCES IN GATE CIRCUITS

RADU NEGULESCU
Department of Computer Science
University of Waterloo
Waterloo, Ontario, Canada N2L 3G1
email: radu@maveric.uwaterloo.ca

Before sizing the delays of the components in a circuit, it is often necessary to find delay constraints that would ensure the correctness of the circuit, and to verify the sufficiency of these constraints. We formalize constraints of a certain type as processes in a metric-free model. The circuit specification and components are also represented as processes, to be coupled and compared with the constraint processes. We use a BDD-based tool to verify a circuit together with a set of constraints, and to find hints as to which constraints are needed. We illustrate this technique on a circuit that uses extended isochronic forks.