Compiling FPGA netlists for formal verification
Joachim Pistorius and K. Chandrashekar, Altera Corp.
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.
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.
To read the full article, click here
Related Semiconductor IP
- JESD204E Controller IP
- eUSB2V2.0 Controller + PHY IP
- I/O Library with LVDS in SkyWater 90nm
- 50G PON LDPC Encoder/Decoder
- UALink Controller
Related Articles
- Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
- How formal verification saves time in digital IP design
- Don't over-constrain in formal property verification (FPV) flows
- Formal Verification Has It Covered!
Latest Articles
- Crypto-RV: High-Efficiency FPGA-Based RISC-V Cryptographic Co-Processor for IoT Security
- In-Pipeline Integration of Digital In-Memory-Computing into RISC-V Vector Architecture to Accelerate Deep Learning
- QMC: Efficient SLM Edge Inference via Outlier-Aware Quantization and Emergent Memories Co-Design
- ChipBench: A Next-Step Benchmark for Evaluating LLM Performance in AI-Aided Chip Design
- COVERT: Trojan Detection in COTS Hardware via Statistical Activation of Microarchitectural Events