Ciesielski et al., 2015 - Google Patents
Verification of gate-level arithmetic circuits by function extractionCiesielski et al., 2015
View PDF- Document ID
- 18090593031505388028
- Author
- Ciesielski M
- Yu C
- Brown W
- Liu D
- Rossi A
- Publication year
- Publication venue
- Proceedings of the 52nd Annual Design Automation Conference
External Links
Snippet
The paper presents an algebraic approach to functional verification of gate-level, integer arithmetic circuits. It is based on extracting a unique bit-level polynomial function computed by the circuit directly from its gate-level implementation. The method can be used to verify …
- 238000000605 extraction 0 title description 6
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/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/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/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/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/30—Information retrieval; Database structures therefor; File system structures therefor
- G06F17/30861—Retrieval from the Internet, e.g. browsers
-
- 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
-
- 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/20—Handling natural language data
-
- 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
- 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/70—Fault tolerant, i.e. transient fault suppression
-
- 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
- G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
- G06F21/60—Protecting data
- G06F21/62—Protecting access to data via a platform, e.g. using keys or access control rules
- G06F21/6218—Protecting access to data via a platform, e.g. using keys or access control rules to a system of files or objects, e.g. local or distributed file system or database
-
- 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
- G06F7/38—Methods or arrangements for performing computations using exclusively denominational number representation, e.g. using binary, ternary, decimal representation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2221/00—Indexing scheme relating to security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
-
- 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
- G06F2207/00—Indexing scheme relating to methods or arrangements for processing data by operating upon the order or content of the data handled
Similar Documents
Publication | Publication Date | Title |
---|---|---|
Ciesielski et al. | Verification of gate-level arithmetic circuits by function extraction | |
Yu et al. | Formal verification of arithmetic circuits by function extraction | |
Yu et al. | Fast algebraic rewriting based on and-inverter graphs | |
Farahmandi et al. | Gröbner basis based formal verification of large arithmetic circuits using gaussian elimination and cone-based polynomial extraction | |
Sicklinger et al. | Interface Jacobian‐based co‐simulation | |
Yuan et al. | Modeling design constraints and biasing in simulation using BDDs | |
Ciesielski et al. | Taylor expansion diagrams: A canonical representation for verification of data flow designs | |
US10762261B2 (en) | Methods and apparatus for transforming the function of an integrated circuit | |
Yu et al. | Efficient parallel verification of galois field multipliers | |
Yu et al. | Formal analysis of Galois field arithmetic circuits-parallel verification and reverse engineering | |
Yu et al. | Automatic word-level abstraction of datapath | |
Yasin et al. | Functional verification of hardware dividers using algebraic model | |
Basith et al. | Algebraic approach to arithmetic design verification | |
Farahmandi et al. | Effective combination of algebraic techniques and decision diagrams to formally verify large arithmetic circuits | |
Ciesielski et al. | Function extraction from arithmetic bit-level circuits | |
Haghbayan et al. | Formal verification and debugging of array dividers with auto-correction mechanism | |
Chou et al. | 2022 cad contest problem a: Learning arithmetic operations from gate-level circuit | |
Ciesielski et al. | Arithmetic bit-level verification using network flow model | |
Hasan et al. | Automated formal synthesis of Wallace tree multipliers | |
Haghbayan et al. | Automated formal approach for debugging dividers using dynamic specification | |
Yu et al. | Spectral approach to verifying non-linear arithmetic circuits | |
Pavlenko et al. | Modeling of custom-designed arithmetic components for ABL normalization | |
Yu et al. | Verification of arithmetic datapath designs using word-level approach—A case study | |
Azarbad et al. | Scalable SMT-based equivalence checking of nested loop pipelining in behavioral synthesis | |
Kaufmann | Formal verification of integer multiplier circuits using algebraic reasoning: A survey |