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

Ben-David et al., 2003 - Google Patents

Model checking at IBM

Ben-David et al., 2003

View PDF
Document ID
2482974765185082517
Author
Ben-David S
Eisner C
Geist D
Wolfsthal Y
Publication year
Publication venue
Formal Methods in System Design

External Links

Snippet

Over the past nine years, the Formal Methods Group at the IBM Haifa Research Laboratory has made steady progress in developing tools and techniques that make the power of model checking accessible to the community of hardware designers and verification engineers, to …
Continue reading at www.researchgate.net (PDF) (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
    • 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
    • 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
    • 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/10—Complex mathematical operations
    • G06F17/11—Complex mathematical operations for solving equations, e.g. nonlinear equations, general mathematical optimization problems
    • 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
    • G01—MEASURING; TESTING
    • G01R—MEASURING ELECTRIC VARIABLES; MEASURING MAGNETIC VARIABLES
    • G01R31/00—Arrangements for testing electric properties; Arrangements for locating electric faults; Arrangements for electrical testing characterised by what is being tested not provided for elsewhere
    • G01R31/28—Testing of electronic circuits, e.g. by signal tracer
    • G01R31/317—Testing of digital circuits
    • G01R31/3181—Functional testing
    • G01R31/3183—Generation of test inputs, e.g. test vectors, patterns or sequence
    • G01R31/318342—Generation of test inputs, e.g. test vectors, patterns or sequence by preliminary fault modelling, e.g. analysis, simulation
    • 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
    • G06F2201/00—Indexing scheme relating to error detection, to error correction, and to monitoring

Similar Documents

Publication Publication Date Title
Bryant Binary decision diagrams
Ivančić et al. Efficient SAT-based bounded model checking for software verification
Moskewicz et al. Chaff: Engineering an efficient SAT solver
Ben-David et al. Model checking at IBM
Ivancic et al. Model checking C programs using F-Soft
Chen et al. Automated design debugging with maximum satisfiability
US8751984B2 (en) Method, system and computer program for hardware design debugging
Ciesielski et al. Taylor expansion diagrams: A canonical representation for verification of data flow designs
US20020053064A1 (en) Dynamic detection and removal of inactive clauses in sat with application in image computation
US6728665B1 (en) SAT-based image computation with application in reachability analysis
Gupta et al. SAT-based verification methods and applications in hardware verification
JP4629682B2 (en) Efficient modeling method for embedded memory in finite memory test
Parthasarathy et al. An efficient finite-domain constraint solver for circuits
Wachter et al. Probabilistic model checking modulo theories
Franco et al. SBSAT: a state-based, BDD-based satisfiability solver
Li et al. Digital system verification: A combined formal methods and simulation framework
Parthasarathy et al. Safety property verification using sequential SAT and bounded model checking
Cabodi et al. Strengthening model checking techniques with inductive invariants
Baumgartner et al. Model checking the IBM Gigahertz Processor: An abstraction algorithm for high-performance netlists
Isles et al. Computing reachable control states of systems modeled with uninterpreted functions and infinite memory
Drechsler et al. System level validation using formal techniques
Gallardo et al. Refinement of LTL formulas for abstract model checking
Chockler et al. Coverage of implementations by simulating specifications
Borrione et al. HDL-based integration of formal methods and CAD tools in the PREVAIL environment
Bryant et al. Formal methods for functional verification