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

AÏT MOHAMED et al., 2004 - Google Patents

MDG-based state enumeration by retiming and circuit transformation

AÏT MOHAMED et al., 2004

View PDF
Document ID
27328563221097116
Author
AÏT MOHAMED O
Song X
Cerny E
Tahar S
Zhou Z
Publication year
Publication venue
Journal of Circuits, Systems, and Computers

External Links

Snippet

Multiway Decision Graphs (MDGs) have recently been proposed as an efficient representation for RTL designs. In this paper, we illustrate the MDG-based formal verification technique on the example of the Island Tunnel Controller. We investigate several techniques …
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/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/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
    • 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/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
    • 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/30—Arrangements for executing machine-instructions, e.g. instruction decode
    • 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/3185—Reconfiguring for testing, e.g. LSSD, partitioning
    • 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
    • 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
    • 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
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]

Similar Documents

Publication Publication Date Title
US7890901B2 (en) Method and system for verifying the equivalence of digital circuits
US6038392A (en) Implementation of boolean satisfiability with non-chronological backtracking in reconfigurable hardware
US6163876A (en) Method for verification of RTL generated from scheduled behavior in a high-level synthesis flow
Seger et al. Formal verification by symbolic evaluation of partially-ordered trajectories
US7383166B2 (en) Verification of scheduling in the presence of loops using uninterpreted symbolic simulation
JP4000567B2 (en) Efficient bounded model checking method
US8413090B1 (en) Temporal decomposition for design and verification
US20090125766A1 (en) Method, system and computer program for hardware design debugging
Zhou et al. Formal verification of the island tunnel controller using multiway decision graphs
US7523029B2 (en) Logic verification and logic cone extraction technique
Déharbe et al. Model checking VHDL with CV
Baumgartner et al. Model checking the IBM Gigahertz Processor: An abstraction algorithm for high-performance netlists
Kroening et al. Formal verification at higher levels of abstraction
Clarke et al. Making predicate abstraction efficient: How to eliminate redundant predicates
AÏT MOHAMED et al. MDG-based state enumeration by retiming and circuit transformation
EP3842985A1 (en) Verifying a hardware design for a multi-stage component
Ruf et al. Bounded Property Checking with Symbolic Simulation.
Mohamed et al. MDG-based verification by retiming and combinational transformations
Taher et al. Learning-based diversity estimation: Leveraging the power of high-level synthesis to mitigate common-mode failure
Brandt et al. The model checking view to clock gating and operand isolation
McMillan Methods for exploiting SAT solvers in unbounded model checking
Tahar et al. Three approaches to hardware verification: HOL, MDG, and VIS compared
Tahary et al. Formal Verification of the Island Tunnel Controller using Multiway Decision Graphs
Huang et al. Static property checking using ATPG vs. BDD techniques
Mendias et al. Efficient verification of scheduling, allocation and binding in high-level synthesis