Chipress

During formal verification, sometimes we may see unreachable properties. Using Cadence Jasper Gold for example, it can be flagged as either unreachable cover properties, or passing yet never triggered assert properties.

This can be caused by over constraints, i.e., excessive assume properties, or design bugs.

In order to isolate the root cause, RTL designers can do the following steps:

1. Review all assume properties in the FV testbench and the ones embedded in RTL, and make sure no excessive or unnecessary assume properties exist
2. Use “check_assumptions” in Jasper GUI. This command helps to “sanitize” constraints and check if they lead to dead-end states
3. Use “get_needed_assumtpions – property <unreachable_cover>” in Jasper GUI. This command will return the constraints responsible for unreachable cover properties. If it does not return anything, then the cover property is impossible by design