The Community for Technology Leaders
Proceedings of ICCD '95 International Conference on Computer Design. VLSI in Computers and Processors (1995)
Austin, Texas
Oct. 2, 1995 to Oct. 4, 1995
ISSN: 1063-6404
ISBN: 0-8186-7165-3
pp: 72
S. Campos , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
E. Clarke , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
W. Marrero , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
M. Minea , Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
ABSTRACT
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; however it 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. Our results allow a more detailed analysis of a model than is possible with tools that simply determine whether a property is satisfied or not. We present algorithms that determine the exact bounds on the time interval between two specified events and the number of occurrences of another event in such an interval. To demonstrate how our method works, we have modelled the PCI local bus and analyzed its temporal behavior. The results demonstrate the usefulness of our technique in analyzing complex modem designs.
INDEX TERMS
system buses; performance evaluation; logic testing; PCI local bus; symbolic techniques; finite-state systems; model checking techniques; timing information; temporal behavior
CITATION

W. Marrero, M. Minea, E. Clarke and S. Campos, "Verifying the performance of the PCI local bus using symbolic techniques," Proceedings of ICCD '95 International Conference on Computer Design. VLSI in Computers and Processors(ICCD), Austin, Texas, 1995, pp. 72.
doi:10.1109/ICCD.1995.528793
90 ms
(Ver 3.3 (11022016))