Chipress

Assert and assume properties often use a triggering event, or a precondition, to define when the test expression should be checked. If the precondition is unreachable, then the assert property will never trigger, and it does not check what was intended. Consequently, the tool can never find a violation trace regardless of the logic driving the test expression.

Jasper Gold elaborates the RTL embedded SVA properties, and extracts precondition reachability checks. This becomes handy to make sure good FV coverage and automate the precondition check process.

For example, if we have an SVA embedded in RTL like this:

 assert property (@(posedge clk) vld & ~rdy |=> $stable(vld));

Jasper Gold will automatically generate cover properties with a suffix identifying the precondition type, like “:preconditionN”. In the above example, the tool automatically creates a cover property equivalent to:

cover property (@(posedge clk) vld & ~rdy);

One can diable precondition reachability checks for embedded properties during design elaboration phase, by using “-no_preconditions” option:

elaborate … -no_preconditions