In reply to Have_A_Doubt:
1800, pg 461 rule3 is a property declared in module top. The assert statement a1 starts checking the property from the beginning to the end of simulation."
1800, [g 493 A final procedure may be specified within a checker in the same manner as in a module (see 9.2.3 ). This allows for the checker to check conditions with immediate assertions or print out statistics at the end of simulation. The operation of the final procedure is independent of the instantiation context of the checker that contains it. It will be executed once at the end of simulation for every instantiation of that checker. There is no implied ordering in the execution of multiple final procedures. A final procedure within a checker may include any construct allowed in a non-checker final procedure.
After the $finish, there are no other clocks.
// instead of
$rose(a) |=> ( !b throughout $rose(simulatn_ends)[->1] );
// what about
$rose(a) |=> s_always[1:2^31] !b );
// you can also do the following instead of the s_always
final assert(!b); // b==0 at end of sim