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

Mishchenko et al., 2005 - Google Patents

FRAIGs: A unifying representation for logic synthesis and verification

Mishchenko et al., 2005

View PDF
Document ID
5187767772763993316
Author
Mishchenko A
Chatterjee S
Jiang R
Brayton R
Publication year

External Links

Snippet

AND-INV graphs (AIGs) are Boolean networks composed of twoinput AND-gates and inverters. In the known applications, such as equivalence checking and technology mapping, AIGs are used to represent and manipulate Boolean functions. AIGs powered by …
Continue reading at ptolemy.berkeley.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/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/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/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/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/5018—Computer-aided design using simulation using finite difference methods or finite element 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/5072—Floorplanning, e.g. partitioning, placement
    • 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
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • G06F17/30386—Retrieval requests
    • G06F17/30424—Query processing
    • G06F17/30442—Query optimisation
    • G06F17/30448—Query rewriting and transformation
    • G06F17/30474—Run-time 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/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
    • 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
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/08—Multi-objective optimization
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/12—Design for manufacturability
    • 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
    • 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
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N3/00—Computer systems based on biological models
    • G06N3/12—Computer systems based on biological models using genetic models
    • G06N3/126—Genetic algorithms, i.e. information processing using digital simulations of the genetic system

Similar Documents

Publication Publication Date Title
Mishchenko et al. FRAIGs: A unifying representation for logic synthesis and verification
Mishchenko et al. SAT-based complete don't-care computation for network optimization
US6301687B1 (en) Method for verification of combinational circuits using a filtering oriented approach
JP4000567B2 (en) Efficient bounded model checking method
Clarke et al. Bounded model checking using satisfiability solving
Brayton et al. ABC: An academic industrial-strength verification tool
Mishchenko et al. Improvements to combinational equivalence checking
Brayton et al. Scalable logic synthesis using a simple circuit structure
US7788616B2 (en) Method and system for performing heuristic constraint simplification
US8413090B1 (en) Temporal decomposition for design and verification
Gowda et al. Identification of threshold functions and synthesis of threshold networks
Mishchenko et al. Scalable and scalably-verifiable sequential synthesis
Yamashita et al. Fast equivalence-checking for quantum circuits
Mishchenko et al. Using simulation and satisfiability to compute flexibilities in Boolean networks
Plaisted et al. A satisfiability procedure for quantified boolean formulae
US6728665B1 (en) SAT-based image computation with application in reachability analysis
Hulgaard et al. Equivalence checking of combinational circuits using boolean expression diagrams
JP4629682B2 (en) Efficient modeling method for embedded memory in finite memory test
Pigorsch et al. An AIG-based QBF-solver using SAT for preprocessing
Disch et al. Combinational equivalence checking using incremental SAT solving, output ordering, and resets
Reda et al. On the relation between SAT and BDDs for equivalence checking
Woelfel Symbolic topological sorting with OBDDs
US7343573B2 (en) Method and system for enhanced verification through binary decision diagram-based target decomposition
Chen et al. Improvements to satisfiability-based boolean function bi-decomposition
Mishchenko et al. Fraigs: Functionally reduced and-inv graphs