Wendy Belluomini Defense

[Colleen Hoopes]

UNIVERSITY OF UTAH
DEPARTMENT OF COMPUTER SCIENCE
DISSERTATION DEFENSE

Algorithms for Synthesis and Verification of
Timed Circuits and Systems

Tuesday, August 31, 1999

Wendy Belluomini

Large Conference Room (3151)

Refreshments 3:15 PM
Defense 3:30 PM

In order to increase performance, circuit designers are beginning
to move away from traditional synchronous designs based on static logic.
Recent design examples have shown that significant performance gains
are realized when aggressive styles are used. Circuit correctness
in these aggressive circuit styles is highly dependent, and in industry
they are typically designed by hand. In order to automate the process
of designing and verifying timed circuits, algorithms to explore the
reachable state space of the circuit under the timing constraints are
necessary.

This thesis presents a new specification method for timed circuits,
timed event/level (TEL) structures, and new algorithms for exploring
a timed state space. The TEL structure specification allows the
designer to specify behavior controlled by signal transitions, which
is best for representing sequencing, and behavior controlled by signal
levels, which is best for representing gate level circuits. The
thesis also presents algorithms based on partially ordered sets
(POSET's) that explore the timed state space of the TEL structure.
Results using the new specification method and algorithms show orders
of magnitude improvement over previous techniques in both speed and
memory performance. The algorithms have also been successfully
applied to several circuit examples from the recently published
experimental Gigahertz processor developed at IBM. The speed and
memory performance improvements of the algorithm make automatic
synthesis and verification of complex timed circuits possible, making
them an attractive design alternative.

Presented by: Chris Myers