Accession Number : ADA311441

Title :   Verifying the Performance of the PCI Local Bus using Symbolic Techniques,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Campos, S. ; Clarke, E. ; Marrero, W. ; Minea, M.

PDF Url : ADA311441

Report Date : 18 JUN 1996

Pagination or Media Count : 18

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. 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.

Descriptors :   *COMPUTER ARCHITECTURE, *SYMBOLIC PROGRAMMING, ALGORITHMS, OPTIMIZATION, SYSTEMS ENGINEERING, DATA MANAGEMENT, INFORMATION TRANSFER, COMPUTER AIDED DESIGN, COMPUTER COMMUNICATIONS, TIME DEPENDENCE, MICROPROCESSORS, REAL TIME, PERFORMANCE(ENGINEERING), COMPUTER LOGIC, INPUT OUTPUT PROCESSING, SYSTEMS ANALYSIS, COMPUTER PROGRAM VERIFICATION, DESIGN CRITERIA, BUS CONDUCTORS.

Subject Categories : Computer Hardware
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE