Interface Timing Verification with Combined Max and Linear Constraints

A fundamental timing analysis problem in the verification and synthesis of interface logic circuitry is the determination of the possible and allowable time separations, or skews between interface events, given timing constraints and propagation delays between the events generated by the circuits the interface connects. These skews are used to verify timing properties and determine allowable propagation delays for logic synthesis. The main contributions of this report are two-fold. First, this report shows that the verification problem can be expressed with constraints of the form x i Maxfx j1 + \Delta j1 ;i ; : : : ; x jm + \Delta jm ;i g; such as those described in several other domains including the fMax; +g algebra used in modeling discrete event systems [1]. Second, this report presents and proves correct an algorithm that provides tight upper bounds on the time separation between all pairs x i ; x j for such a constraint set in less time and with tighter bounds than previous a..