Don't over-constrain in formal property verification (FPV) flows
Anders Nordstrom, Synopsys
EDN (February 04, 2016)
Formal property verification (FPV) is increasingly being used to complement simulation for system-on-chip (SoC) verification. Adding FPV to your verification flow can greatly accelerate verification closure and find tough corner-case bugs, but it is important to understand the differences between the technologies. The main difference is that FPV uses properties, i.e., assertions and constraints, instead of a testbench. Assertions are used in simulation as well, but the role of constraints is different. An understanding of constraints is necessary for successful use of FPV.
Constraints
Constraints play a central role in FPV. They define what is legal stimulus to the design under test, i.e., what state space can be reached. Assertions define the desired behavior of the DUT for the legal stimulus.
Constraints describe how inputs to the DUT are allowed to behave, what values should be taken, and temporal relationships between inputs. Constraints can be thought of as the stimulus in simulation. In constrained random simulation, the constraint solver generates an input vector for the next cycle that satisfies all constraints. It will continue to generate cycle after cycle of stimulus until the end of simulation, or until it reaches a situation where no legal stimulus can be generated.
In contrast, constraints for formal verification can describe, for example, how to legally communicate within a given protocol.
To read the full article, click here
Related Semiconductor IP
- Process/Voltage/Temperature Sensor with Self-calibration (Supply voltage 1.2V) - TSMC 3nm N3P
- USB 20Gbps Device Controller
- SM4 Cipher Engine
- Ultra-High-Speed Time-Interleaved 7-bit 64GSPS ADC on 3nm
- Fault Tolerant DDR2/DDR3/DDR4 Memory controller
Related White Papers
- Formal property verification: A tale of two methods
- Bridging Design Verification Gaps with Formal Verification
- Formal, simulation, and AMBA verification IP combine to verify configurable powerline networking SoC
- How formal verification saves time in digital IP design
Latest White Papers
- Fault Injection in On-Chip Interconnects: A Comparative Study of Wishbone, AXI-Lite, and AXI
- eFPGA – Hidden Engine of Tomorrow’s High-Frequency Trading Systems
- aTENNuate: Optimized Real-time Speech Enhancement with Deep SSMs on RawAudio
- Combating the Memory Walls: Optimization Pathways for Long-Context Agentic LLM Inference
- Hardware Acceleration of Kolmogorov-Arnold Network (KAN) in Large-Scale Systems