[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Bhagwati et al., 1994 - Google Patents

Automatic verification of pipelined microprocessors

Bhagwati et al., 1994

View PDF
Document ID
170611603689674055
Author
Bhagwati V
Devadas S
Publication year
Publication venue
Proceedings of the 31st annual Design Automation Conference

External Links

Snippet

We address the problem of automatically verifying large digital designs at the logic level, against high-level specifications. In this paper, we present a methodology which allows for the verification of a specific class of synchronous machines, namely pipelined …
Continue reading at dl.acm.org (PDF) (other versions)

Classifications

    • 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
    • G06F9/30003—Arrangements for executing specific machine instructions
    • G06F9/30007—Arrangements for executing specific machine instructions to perform operations on data operands
    • 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
    • G06F9/30003—Arrangements for executing specific machine instructions
    • G06F9/3004—Arrangements for executing specific machine instructions to perform operations on memory
    • 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
    • G06F9/38—Concurrent instruction execution, e.g. pipeline, look ahead
    • G06F9/3836—Instruction issuing, e.g. dynamic instruction scheduling, out of order instruction execution
    • G06F9/3842—Speculative instruction execution
    • 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
    • G06F9/38—Concurrent instruction execution, e.g. pipeline, look ahead
    • G06F9/3867—Concurrent instruction execution, e.g. pipeline, look ahead using instruction pipelines
    • 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
    • G06F9/38—Concurrent instruction execution, e.g. pipeline, look ahead
    • G06F9/3885—Concurrent instruction execution, e.g. pipeline, look ahead using a plurality of independent parallel functional units
    • G06F9/3889—Concurrent instruction execution, e.g. pipeline, look ahead using a plurality of independent parallel functional units controlled by multiple instructions, e.g. MIMD, decoupled access or execute
    • 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
    • G06F9/32—Address formation of the next instruction, e.g. incrementing the instruction counter, jump
    • G06F9/322—Address formation of the next instruction, e.g. incrementing the instruction counter, jump for non-sequential address
    • 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
    • G06F9/38—Concurrent instruction execution, e.g. pipeline, look ahead
    • G06F9/3861—Recovery, e.g. branch miss-prediction, exception handling
    • 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
    • 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/44—Arrangements for executing specific programmes
    • G06F9/4421—Execution paradigms
    • 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
    • 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
    • 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/46—Multiprogramming arrangements
    • 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
    • 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/70—Fault tolerant, i.e. transient fault suppression
    • 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
    • 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
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2207/00—Indexing scheme relating to methods or arrangements for processing data by operating upon the order or content of the data handled

Similar Documents

Publication Publication Date Title
Burch et al. Sequential circuit verification using symbolic model checking
Velev et al. Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction
Burch et al. Automatic verification of pipelined microprocessor control
Burch Techniques for verifying superscalar microprocessors
US8108810B2 (en) Synchronous circuit synthesis using an asynchronous specification
Sawada et al. Trace table based approach for pipelined microprocessor verification
US6597664B1 (en) Digital circuit synthesis system
Hosabettu et al. Decomposing the proof of correctness of pipelined microprocessors
Bhagwati et al. Automatic verification of pipelined microprocessors
Bryant et al. Convergence testing in term-level bounded model checking
Chandra et al. Architectural verification of processors using symbolic instruction graphs
Tahar et al. A practical methodology for the formal verification of RISC processors
Fox et al. Algebraic models of correctness for microprocessors
Dave Designing a reorder buffer in Bluespec
Fox et al. Algebraic models of superscalar microprocessor implementations: A case study
Kroening et al. Proving the Correctness of Pipelined Micro-Architectures.
Lis Superscalar processors via automatic microarchitecture transformations
Kaufmann et al. Verification of pipeline circuits
Manolios Refinement and theorem proving
Harcourt et al. High level timing specification of instruction-level parallel processors
Hosabettu et al. A practical methodology for verifying pipelined microarchitectures
Mahajan et al. Utility of transaction-level hardware models in refinement checking
JPH0765046A (en) Logical device verifying method
Su Symbolic simulation techniques for verifying rtl circuits combining datapaths and controllers
Marinescu et al. A synthesis algorithm for modular design of pipelined circuits