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
- Post-Quantum Digital Signature IP Core
- Compact Embedded RISC-V Processor
- Power-OK Monitor
- RISC-V-Based, Open Source AI Accelerator for the Edge
- Securyzr™ neo Core Platform
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
- DRsam: Detection of Fault-Based Microarchitectural Side-Channel Attacks in RISC-V Using Statistical Preprocessing and Association Rule Mining
- ShuffleV: A Microarchitectural Defense Strategy against Electromagnetic Side-Channel Attacks in Microprocessors
- Practical Considerations of LDPC Decoder Design in Communications Systems
- A Direct Memory Access Controller (DMAC) for Irregular Data Transfers on RISC-V Linux Systems
- A logically correct SoC design isn’t an optimized design