Beer et al., 1995 - Google Patents
Establishing PCI compliance using formal verification: a case studyBeer et al., 1995
View PDF- Document ID
- 11810940983941704617
- Author
- Beer I
- Ben-David S
- Eisner C
- Engel Y
- Gewirtzman R
- Landver A
- Publication year
- Publication venue
- Proceedings International Phoenix Conference on Computers and Communications
External Links
Snippet
This paper presents a case study in the practical application of formal verification. Specifically, we describe our experience in applying the formal verification technique of symbolic model checking to the verification of PCI bus bridges. During the last 2 years, we …
- 238000000034 method 0 abstract description 12
Classifications
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5009—Computer-aided design using simulation
- G06F17/5022—Logic simulation, e.g. for logic circuit operation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5009—Computer-aided design using simulation
- G06F17/504—Formal methods
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5045—Circuit design
- G06F17/5054—Circuit design for user-programmable logic devices, e.g. field programmable gate arrays [FPGA]
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5068—Physical circuit design, e.g. layout for integrated circuits or printed circuit boards
- G06F17/5081—Layout analysis, e.g. layout verification, design rule check
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5045—Circuit design
- G06F17/505—Logic synthesis, e.g. technology mapping, optimisation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/30—Monitoring
- G06F11/34—Recording or statistical evaluation of computer activity, e.g. of down time, of input/output operation; Recording or statistical evaluation of user activity, e.g. usability assessment
- G06F11/3457—Performance evaluation by simulation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2217/00—Indexing scheme relating to computer aided design [CAD]
- G06F2217/86—Hardware-Software co-design
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2217/00—Indexing scheme relating to computer aided design [CAD]
- G06F2217/70—Fault tolerant, i.e. transient fault suppression
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F9/00—Arrangements for programme control, e.g. control unit
- G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F8/00—Arrangements for software engineering
- G06F8/30—Creation or generation of source code
- G06F8/34—Graphical or visual programming
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/362—Software debugging
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/20—Handling natural language data
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2217/00—Indexing scheme relating to computer aided design [CAD]
- G06F2217/78—Power analysis and optimization
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2217/00—Indexing scheme relating to computer aided design [CAD]
- G06F2217/74—Symbolic schematics
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F8/00—Arrangements for software engineering
- G06F8/20—Software design
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F8/00—Arrangements for software engineering
- G06F8/40—Transformations of program code
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2201/00—Indexing scheme relating to error detection, to error correction, and to monitoring
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06T—IMAGE DATA PROCESSING OR GENERATION, IN GENERAL
Similar Documents
Publication | Publication Date | Title |
---|---|---|
US5222030A (en) | Methodology for deriving executable low-level structural descriptions and valid physical implementations of circuits and systems from high-level semantic specifications and descriptions thereof | |
US6240376B1 (en) | Method and apparatus for gate-level simulation of synthesized register transfer level designs with source-level debugging | |
US6336087B2 (en) | Method and apparatus for gate-level simulation of synthesized register transfer level design with source-level debugging | |
Kumar et al. | The Codesign of Embedded Systems: A Unified Hardware/Software Representation: A Unified Hardware/Software Representation | |
US5493508A (en) | Specification and design of complex digital systems | |
US5933356A (en) | Method and system for creating and verifying structural logic model of electronic design from behavioral description, including generation of logic and timing models | |
US5801958A (en) | Method and system for creating and validating low level description of electronic design from higher level, behavior-oriented description, including interactive system for hierarchical display of control and dataflow information | |
US6295636B1 (en) | RTL analysis for improved logic synthesis | |
US6378123B1 (en) | Method of handling macro components in circuit design synthesis | |
US5867399A (en) | System and method for creating and validating structural description of electronic system from higher-level and behavior-oriented description | |
US5870308A (en) | Method and system for creating and validating low-level description of electronic design | |
Berge et al. | VHDL designer’s reference | |
US6289491B1 (en) | Netlist analysis tool by degree of conformity | |
US9710750B1 (en) | Proving latency associated with references to a data store | |
US6415420B1 (en) | Synthesizing sequential devices from hardware description languages (HDLS) | |
Lavagno et al. | Design of embedded systems | |
Kuhn et al. | A framework for object oriented hardware specification, verification, and synthesis | |
Beer et al. | Establishing PCI compliance using formal verification: a case study | |
Bailey et al. | Tlm-driven design and verification methodology | |
Bailey | Comparison of vhdl, verilog and systemverilog | |
Davie | A Formal, Hierarchical Design and Validation Methodology for VLSI | |
Davare et al. | A platform-based design flow for kahn process networks | |
Foulk et al. | Aids-an integrated design system for digital hardware | |
Vahid et al. | SpecCharts: A language for system level specification and synthesis | |
Lipman | Chip hardware and software: Why can't they just get along? |