Dumitrescu et al., 1998 - Google Patents
Identification of non-redundant memorizing elements in VHDL synchronous designs for formal verification toolsDumitrescu et al., 1998
View PDF- Document ID
- 1481145012120967941
- Author
- Dumitrescu E
- Ostier P
- Publication year
- Publication venue
- Proceedings of the Fifth International Workshop on Symbolic Methods and Applications in Circuit Design (SMACD)
External Links
Snippet
Formal tools for the verification of HDL synchronous descriptions are currently in development for both the Verilog [2, 3] and VHDL languages [1], but little work has been done on tools able to handle both languages [8]. The well known reason is that VHDL and …
- 230000001360 synchronised 0 title abstract description 19
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
- G06F17/5031—Timing analysis
-
- 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/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/20—Handling natural language data
- G06F17/27—Automatic analysis, e.g. parsing
- G06F17/2705—Parsing
- G06F17/271—Syntactic parsing, e.g. based on context-free grammar [CFG], unification grammars
-
- 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
- G06F17/21—Text processing
- G06F17/22—Manipulating or registering by use of codes, e.g. in sequence of text characters
-
- 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/86—Hardware-Software co-design
-
- 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
-
- 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/06—Constraint-based CAD
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2217/00—Indexing scheme relating to computer aided design [CAD]
- G06F2217/74—Symbolic schematics
-
- 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
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
Similar Documents
Publication | Publication Date | Title |
---|---|---|
US7383166B2 (en) | Verification of scheduling in the presence of loops using uninterpreted symbolic simulation | |
Burch et al. | Symbolic model checking for sequential circuit verification | |
US7890901B2 (en) | Method and system for verifying the equivalence of digital circuits | |
US6148436A (en) | System and method for automatic generation of gate-level descriptions from table-based descriptions for electronic design automation | |
US20050091025A1 (en) | Methods and systems for improved integrated circuit functional simulation | |
EP1769407B1 (en) | Loop manipulation in a behavioral synthesis tool | |
Große et al. | Quality-driven SystemC design | |
Bombieri et al. | HIFSuite: Tools for HDL code conversion and manipulation | |
US6415420B1 (en) | Synthesizing sequential devices from hardware description languages (HDLS) | |
JPH07160744A (en) | Autonomously evolving hardware design system | |
Kumar et al. | Structuring and automating hardware proofs in a higher-order theorem-proving environment | |
Wolf | Yosys manual | |
Déharbe et al. | Model checking VHDL with CV | |
Gawanmeh et al. | Interfacing ASM with the MDG tool | |
Dumitrescu et al. | Identification of non-redundant memorizing elements in VHDL synchronous designs for formal verification tools | |
Kemper | SAT-based verification for timed component connectors | |
Alizadeh et al. | Using integer equations for high level formal verification property checking | |
Borrione et al. | HDL-based integration of formal methods and CAD tools in the PREVAIL environment | |
Carmona et al. | Synthesis of asynchronous hardware from petri nets | |
Caballero et al. | Two type extensions for the constraint modeling language MiniZinc | |
Wenzel et al. | Automatically Restructuring HDL Modules for Improved Reusability in Rapid Synthesis | |
Tahar et al. | Comparing HOL and MDG: A case study on the Verification of an ATM Switch Fabric | |
Vinco et al. | Design domains and abstraction levels for effective smart system simulation | |
Borrione et al. | An approach to Verilog-VHDL interoperability for synchronous designs | |
Borrione et al. | Using macros to mimic VHDL |