[go: up one dir, main page]

Fang et al., 2023 - Google Patents

r-map: Relating Implementation and Specification in Hardware Refinement Checking

Fang et al., 2023

Document ID
16581993557520005715
Author
Fang W
Hu G
Zhang H
Publication year
Publication venue
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

External Links

Snippet

Refinement checking is an important formal verification method that checks if a hardware implementation complies with (in other words, refines) a given specification. It has been widely used in processor and nonprocessor verification. In refinement checking, a …
Continue reading at ieeexplore.ieee.org (other versions)

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/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/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
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/362—Software debugging
    • G06F11/3636—Software debugging by tracing the execution of the program
    • 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
    • G06F11/3648—Software debugging using additional hardware
    • 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
    • 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/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • 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/3668—Software testing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • 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
    • G06F9/30—Arrangements for executing machine-instructions, e.g. instruction decode
    • 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
    • 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
    • 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
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/68—Processors
    • 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
    • G06F1/00—Details of data-processing equipment not covered by groups G06F3/00 - G06F13/00, e.g. cooling, packaging or power supply specially adapted for computer application

Similar Documents

Publication Publication Date Title
Huang et al. Instruction-level abstraction (ila) a uniform specification for system-on-chip (soc) verification
Chen et al. System-level validation: high-level modeling and directed test generation techniques
Mishra et al. Architecture description languages for programmable embedded systems
Manerkar et al. RTLCheck: Verifying the memory consistency of RTL designs
US11734480B2 (en) Performance modeling and analysis of microprocessors using dependency graphs
Urdahl et al. Path predicate abstraction for sound system-level models of RT-level circuit designs
Nguyen et al. Formal hardware/software co-verification by interval property checking with abstraction
Devarajegowda et al. Gap-free processor verification by s 2 qed and property generation
Fadiheh et al. Symbolic quick error detection using symbolic initial state for pre-silicon verification
Laeufer et al. Rtl-repair: Fast symbolic repair of hardware design code
Fang et al. r-map: Relating Implementation and Specification in Hardware Refinement Checking
Zhang et al. Automatic test program generation for out-of-order superscalar processors
Urdahl et al. Properties first? A new design methodology for hardware, and its perspectives in safety analysis
Bombieri et al. Reusing RTL assertion checkers for verification of SystemC TLM models
CN117172166A (en) Processor model construction method and processor formal verification method
Das et al. CoVerPlan: A Co mprehensive Ver ification Plan ning Framework Leveraging PSS Specifications
Gilani Methodologies for Accelerated Open-Source Hardware Verification and Optimization
Wu et al. Verification-driven design for asynchronous VLSI
Assayad et al. A Novel Architecture Prototyping Framework With Generic Properties Verification for Sub-architectures
Plassan et al. Improving the efficiency of formal verification: the case of clock-domain crossings
Li et al. A retargetable software timing analyzer using architecture description language
Ludwig et al. Democratizing Formal Verification
Sun et al. ISAAC: Intelligent, Scalable, Agile, and Accelerated CPU Verification via LLM-aided FPGA Parallelism
Loitz et al. Formal hardware/software co-verification of application specific instruction set processors
Villarraga Formal Verification of Firmware-Based System-on-Chip Modules