On Deducing Timing Constraints in the Verification of Interfaces

    loading  Checking for direct PDF access through Ovid

Abstract

We formulate several device timing characteristics, and introduce the concept of separation bounds to model devices‘ waveform timing specifications. Separation bounds are used to verify that the produced timings of one device's signals satisfy the required timings of another device to which it is to be connected. We show that even if we know the bounds on two pairs of signal events, say (u, v) and (v, w), we cannot always deduce the correct bounds on (u, w). However, we show that the shortest path method proposed in [4]—to deduce tight constraints from a partial specification—is safe, in the sense that an affirmative answer to satisfiability is trustworthy while a negative answer may be pessimistic.

Related Topics

    loading  Loading Related Articles