Compiling FPGA netlists for formal verification
02/06/2006 9:00 AM EST, EE Times
Multi-million gate system-on-a–chip (SoC) designs easily fit into today’s FPGAs. Due to the ever increasing demand for more speed, less area, and less power, the transformation of a customer’s RTL description into a bitstream format that can program the FPGA is increasingly complicated. This in turn increases the demand for verifying the design transformations.
Even though FPGAs are reprogrammable, an error detected late in the design cycle, or even after the board has gone into production, can still be very expensive. In addition, some FPGA vendors offer migration to structured ASICs, in which a fabricated design cannot be reprogrammed. Therefore, it is even more important for designs targeted towards structured ASIC device families that implementation errors are caught early in the development phase.
For all of the above reasons, customers want to verify the functional correctness of the RTL-to-bitstream design transformations. Formal methods are becoming increasingly popular in the FPGA design methodology, as they offer several advantages over the traditional method of vector-based simulation. Some of these advantages are shorter runtime, better functional coverage, and no need for test vectors.
E-mail This Article | Printer-Friendly Page |
Related Articles
New Articles
- An Introduction to Post-Quantum Cryptography Algorithms
- The Rise of RISC-V and ISO 26262 Compliance
- Synopsys 3DIO Solution for Multi-Die Integration (2.5D/3D)
- SoC NoCs: Homegrown or Commercial Off-the-Shelf?
- From a Lossless (~1.5:1) Compression Algorithm for Llama2 7B Weights to Variable Precision, Variable Range, Compressed Numeric Data Types for CNNs and LLMs
Most Popular
- System Verilog Assertions Simplified
- System Verilog Macro: A Powerful Feature for Design Verification Projects
- Enhancing VLSI Design Efficiency: Tackling Congestion and Shorts with Practical Approaches and PnR Tool (ICC2)
- An Introduction to Post-Quantum Cryptography Algorithms
- Dynamic Memory Allocation and Fragmentation in C and C++