[go: up one dir, main page]

Kim et al., 2008 - Google Patents

Automated formal verification of scheduling with speculative code motions

Kim et al., 2008

Document ID
7021758399330235920
Author
Kim Y
Mansouri N
Publication year
Publication venue
Proceedings of the 18th ACM Great Lakes symposium on VLSI

External Links

Snippet

We present a methodology for formal verification of scheduling phase of High-Level Synthesis (HLS) when speculative code motions are performed during this process. Verification relies on establishing functional equivalence between the result of scheduling …
Continue reading at dl.acm.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/5022—Logic simulation, e.g. for logic circuit operation
    • G06F17/5031—Timing analysis
    • 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/505—Logic synthesis, e.g. technology mapping, optimisation
    • 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/5009—Computer-aided design using simulation
    • G06F17/5036—Computer-aided design using simulation for analog modelling, e.g. for circuits, spice programme, direct methods, relaxation methods
    • 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
    • G06F11/3672—Test management
    • 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
    • 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
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/44—Encoding
    • 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
    • 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
    • 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
    • G06F7/00—Methods or arrangements for processing data by operating upon the order or content of the data handled
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q10/00—Administration; Management

Similar Documents

Publication Publication Date Title
Brayton et al. ABC: An academic industrial-strength verification tool
Atasu et al. An integer linear programming approach for identifying instruction-set extensions
US7890901B2 (en) Method and system for verifying the equivalence of digital circuits
US8156457B2 (en) Concurrent simulation of hardware designs with behavioral characteristics
US20040117168A1 (en) Global analysis of software objects generated from a hardware description
Amarú et al. SAT-sweeping enhanced for logic synthesis
Huang et al. AQUILA: An equivalence checking system for large sequential designs
Jiang et al. PyH2: Using PyMTL3 to create productive and open-source hardware testing methodologies
Kim et al. Automated formal verification of scheduling with speculative code motions
Penczek et al. Abstractions and partial order reductions for checking branching properties of time Petri nets
Goli et al. Automated design understanding of SystemC-based virtual prototypes: Data extraction, analysis and visualization
Fezzardi et al. Using efficient path profiling to optimize memory consumption of on-chip debugging for high-level synthesis
US20020055829A1 (en) High level verification of software and hardware description and sharing resources among concurrent processes
US7257786B1 (en) Method and apparatus for solving constraints
Chen et al. Reliability-aware operation chaining in high level synthesis
Herber The rescue approach-towards compositional hardware/software co-verification
Carmona et al. Synthesis of asynchronous controllers using integer linear programming
Bombieri et al. Reusing RTL assertion checkers for verification of SystemC TLM models
Ghasempouri et al. Engineering of an effective automatic dynamic assertion mining platform
Zeng et al. False timing path identification using ATPG techniques and delay-based information
Ruf et al. Bounded Property Checking with Symbolic Simulation.
Toma et al. Combining several paradigms for circuit validation and verification
Ludwig et al. Property-driven development of a RISC-V CPU
Radhakrishnan et al. An approach to high-level synthesis system validation using formally verified transformations
Urdahl et al. Architectural system modeling for correct-by-construction RTL design