TITLE

Probabilistic Timing Verification and Timing Analysis for Synthesis of
Digital Interface Controllers

ABSTRACT

In this dissertation we present two techniques on the topic of digital interface design:
a probabilistic timing verification and a timing analysis for synthesis, both rooted
in a formal specification. Interface design arises when two digital components
(e.g., a processor and a memory device) are to be interconnected to build up a system.
We have extended a Petri net specification to describe the temporal behavior of the
interface protocols of digital components. The specification describes circuit delays
as random variables thus making it suitable to model process variations and timing
correlation. Interface probabilistic timing verification checks that a subsystem,
composed of components to be interconnected and the associated interface logic,
satisfies the timing constraints specified by the components' specifications.
Our verification technique not only yields tighter results than previous techniques
that do not take timing correlation into consideration but also, if the timing
constraint is not satisfied, determines the probability that a constraint will
be violated. The second technique, timing analysis for synthesis, finds tight
bounds on the delays of the interface logic, which are unknown prior to synthesis,
such that all the timing constraints given in the component specifications are
satisfied.