@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(Verifying the Performance of the PCI Local Bus
using Symbolic Techniques)
@heading(CMU-CS-96-147)
@center(@b(Sergio Campos, Edmund Clarke, Wilfredo Marrero, Marius Minea))
@center(June 1996@foot<Revised version of the paper appearing in the @i[Proceedings of IEEE International Conference in Computer Design], Austin, TX, October 1995.>)
@center(FTP: CMU-CS-96-147.ps)
@blankspace(1)
@begin(text)

Symbolic model checking is a successful technique for checking
properties of large finite-state systems. This method has been used to
verify a number of real-world hardware designs. This methodology,
however, is not able to determine timing or performance properties
directly. Since these properties are extremely important in the design
of high-performance systems and in time-critical applications, we have
extended model checking techniques to produce timing information.
These results allow a more detailed analysis of a model than is
possible with tools that simply determine whether a property is
satisfied of not. We present algorithms that determine the exact
bounds on the delay between two specified events and the number of
occurrences of another event in all such intervals. To demonstrate how
our method works, we have modelled the PCI local bus and analyzed its
temporal behavior. These results show the usefulness of this technique
in analyzing complex modern designs.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Real-time systems, formal verification, symbolic model
checking, quantitative time analysis, PCI Local Bus>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(17 pages)])