Questa Property Checking (PropCheck) supports general assertion-based formal verification to ensure that the design meets its specific functional requirements. With support for PSL, SVA, and OVL, including multi-clocked assertions, PropCheck easily verifies even very large designs with many assertions; analyzing the behavior of the design vs. the desired behavior described by the assertions to identify all design states that are reachable from the initial state.
This analysis allows PropCheck to explore the whole state space in a breadth-first manner, in contrast to the depth-first approach used in simulation. PropCheck is therefore able to exhaustively discover any design errors that can occur, without needing specific stimulus to detect the bug. This ensures that the verified design is bug-free in all legal input scenarios. At the same time, this approach inherently identifies unreachable coverage points, which helps accelerate coverage closure.
Under the hood, PropCheck’s world-class, high capacity, high throughput engines effectively build on their respective strengths by cooperating with each other in real time; thus completing verification faster. Sharing a common language front end with the Questa Advanced Simulator and leveraging the integration with the Unified Coverage Database (UCDB), Questa PropCheck is the perfect tool to accelerate bug detection, error correction and coverage closure.
Learn more ->
