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

Mony et al., 2004 - Google Patents

Scalable automated verification via expert-system guided transformations

Mony et al., 2004

View PDF
Document ID
5063772443379234718
Author
Mony H
Baumgartner J
Paruthi V
Kanzelman R
Kuehlmann A
Publication year
Publication venue
International conference on formal methods in computer-aided design

External Links

Snippet

Transformation-based verification has been proposed to synergistically leverage various transformations to successively simplify and decompose large problems to ones which may be formally discharged. While powerful, such systems require a fair amount of user …
Continue reading at citeseerx.ist.psu.edu (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/5045—Circuit design
    • G06F17/505—Logic synthesis, e.g. technology mapping, optimisation
    • 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
    • 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/10—Complex mathematical operations
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/07—Error detection; Error correction; Monitoring responding to the occurence of a fault, e.g. fault tolerance
    • 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
    • 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
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N3/00—Computer systems based on biological models
    • G06N3/02—Computer systems based on biological models using neural network models
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N99/00—Subject matter not provided for in other groups of this subclass

Similar Documents

Publication Publication Date Title
Mony et al. Scalable automated verification via expert-system guided transformations
US8015528B2 (en) Enhanced verification by closely coupling a structural satisfiability solver and rewriting algorithms
EP1064601B1 (en) A method and an apparatus for analyzing a state based system model
Mishchenko et al. Improvements to combinational equivalence checking
Burch et al. Sequential circuit verification using symbolic model checking
US7448005B2 (en) Method and system for performing utilization of traces for incremental refinement in coupling a structural overapproximation algorithm and a satisfiability solver
US7305637B2 (en) Efficient SAT-based unbounded symbolic model checking
US8407641B2 (en) Logic design verification techniques for liveness checking with retiming
US7917874B2 (en) Reversing the effects of sequential reparameterization on traces
US7356792B2 (en) Method and system for enhanced verification by closely coupling a structural overapproximation algorithm and a structural satisfiability solver
Lee et al. Scalable exploration of functional dependency by interpolation and incremental SAT solving
Gupta et al. SAT-based verification methods and applications in hardware verification
US7921394B2 (en) Enhanced verification through binary decision diagram-based target decomposition
Touati et al. Testing language containment for ω-automata using BDDs
Lind-Nielsen et al. Verification of large state/event systems using compositionality and dependency analysis
US7290229B2 (en) Method and system for optimized handling of constraints during symbolic simulation
Baumgartner et al. Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies
Bryant et al. Convergence testing in term-level bounded model checking
US7350169B2 (en) Method and system for enhanced verification through structural target decomposition
Păun et al. On closure under stuttering
EP3842985A1 (en) Verifying a hardware design for a multi-stage component
Engelhardt et al. Model checking knowledge and linear time: PSPACE cases
Bryant et al. Microprocessor verification using efficient decision procedures for a logic of equality with uninterpreted functions
Abdi et al. Automatic generation of equivalent architecture model from functional specification
Mendias et al. Efficient verification of scheduling, allocation and binding in high-level synthesis