Recent design examples have shown that significant performance gains are re
alized when circuit designers are allowed to make aggressive timing assumpt
ions. Circuit correctness in these aggressive styles is highly timing depen
dent and, in industry, they are typically designed by hand. In order to aut
omate the process of designing and verifying timed circuits, algorithms for
their synthesis and verification are necessary. This paper presents timed
event/level (TEL) structures, a specification formalism for timed circuits
that corresponds directly to gate-level circuits. It also presents an algor
ithm based on partially ordered sets to make the state-spare exploration of
TEL structures more tractable. The combination of the new specification me
thod and algorithm significantly improves efficiency for gate-level timing
verification. Results on a number of circuits, including many from the rece
ntly published gigahertz unit Test Site (guTS) processor from IBM indicate
that modules of significant size can be verified using a level of abstracti
on that preserves the interesting timing properties of the circuit. Accurat
e circuit level verification allows the designer to include less margin in
the design, which can lead to increased performance.