Mentor provides a tool call questa CDC formal, that read the modelsim/questa data base and analyze the code to check if the minimum double flops are present to exchange data from one clock domain to another clock domain.
By simulation, it is not really easy to check this. Random clock frequency could help, with huge number of simulation.
"paper" analysis to find/detect the worst clock ratio....