IFV is doing a formal proof and to do so it reduces the circuit description to a cycle-based model. As a cycle-based model, all of the timing information is ignored. The circuit will only change state on the edges of the clocks that you've defined. The effects of a clocking block will only be visible during a simulation run.
Thank you, TAM1, you've corrected my understanding!
Yes, exactly, I can see the timing effect during the simulation run(In QestaSim) but not the IFV.
BTW, I want to confirm again, you mean the "only simulation run", is that something like such one? Since I successed the timing effect in this pattern.
program automatic test(...) ;