[go: up one dir, main page]

Morihiro et al., 2002 - Google Patents

Formal verification of data-path circuits based on symbolic simulation

Morihiro et al., 2002

Document ID
2001311311707730711
Author
Morihiro Y
Yoneda T
Publication year
Publication venue
IEICE TRANSACTIONS on Information and Systems

External Links

Snippet

This paper presents a formal verification method based on logic simulation. In our method, some restricted class of circuits which include data paths can be verified without abstraction of data paths by using symbolic values. Our verifier extracts a transition relation from the …
Continue reading at search.ieice.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
    • 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/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/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
    • G06F17/5054—Circuit design for user-programmable logic devices, e.g. field programmable gate arrays [FPGA]
    • 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
    • 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
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • 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
US8418101B1 (en) Temporal decomposition for design and verification
US10325040B2 (en) Conditional phase algebra for clock analysis
JP2001142937A (en) Scheduling correctness checking method and schedule verifying method for circuit
Koelbl et al. Solver technology for system-level to RTL equivalence checking
US7124070B2 (en) Method of and apparatus for, and program for verifying equivalence between behavioral description and register transfer level description
KR20220017993A (en) Recovering behavior designs from flat netlists
US8418119B2 (en) Logical circuit netlist reduction and model simplification using simulation results containing symbolic values
Fujita et al. Verification techniques for system-level design
Kam et al. Comparing layouts with HDL models: A formal verification technique
Chisholm et al. Understanding integrated circuits
Singh et al. Extracting RTL models from transistor netlists
Lavagno et al. Synthesis of verifiably hazard-free asynchronous control circuits
US8201119B2 (en) Formal equivalence checking between two models of a circuit design using checkpoints
Baumgartner et al. Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies
Devadas et al. Verification of asynchronous interface circuits with bounded wire delays
Hoskote et al. Automatic verification of implementations of large circuits against HDL specifications
Morihiro et al. Formal verification of data-path circuits based on symbolic simulation
Lee et al. Automatic verification of asynchronous circuits
Mangassarian et al. Debugging RTL using structural dominance
Jeong et al. Optimal technology mapping and cell merger for asynchronous threshold networks
Hsieh et al. Synchronous equivalence for embedded systems: A tool for design exploration
JP4702357B2 (en) Method, apparatus, and program for verifying equivalence between behavior level description and register transfer level description
Mailhot Technology mapping for vlsi circuits exploiting boolean properties and operations
Diepenbeck et al. Behaviour driven development for hardware design
Baumgartner Automatic structural abstraction techniques for enhanced verification