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
- TSMC 7nm 0V75 / 0V9 ESD Local Clamp – Low Cap
- TSMC 65nm 3V3 ESD Local Clamp – Rad Hard
- TSMC 5nm 1V8, 1.2V and 0.9V ESD Local Protection – Low Cap
- TSMC 3nm 3V3 ESD Local Clamp
- TSMC 3nm 1V2 ESD Local Clamp – Low Capacitance
Related Articles
- Formal property verification: A tale of two methods
- Agentic AI-based Coverage Closure for Formal Verification
- IFV: Information Flow Verification at the Pre-silicon Stage Utilizing Static-Formal Methodology
- How formal verification saves time in digital IP design
Latest Articles
- LACE: Large Language Model Aided Multi-Agent Framework for Agile RISC-V Instruction Extension
- A Process-Aware Hybrid Si/IGO Monolithic-3D 6T SRAM with BEOL Pass-Gates for the 2nm Node
- Automated Estimation of MBIST Area and Test Time in Heterogeneous Memory IPs via Stacked Ensemble Framework
- VIPER: Architecture-Aware Performance Modeling for Processing-in-Memory Design-Space Exploration
- CTTE: An Open Dual-Protocol RISC-V Trace Encoder for N-Trace and E-Trace