Symbolic timing verification of timing diagrams using Presburger formulas

Abstract

We present a novel set of tools for performing symbolic timing verification of timing diagrams. The tools are multi-purpose with uses in verification, derivation of synthesis constraints, and design evaluation. Our methodology is based on using techniques for manipulating Presburger formulas. We demonstrate using several interesting examples that the method is efficient in practice and should be considered for inclusion in commercial tools.