Sampling 'clk' in concurrent SVA

In reply to Jartar:

If clk remains unknown, you will never get an assertion failure.

There might be performance overhead depending on the frequency of clk relative to other clocks.

A better approach might be to look at conditions that might cause clk to gho to X and perhaps use formal tools to check for that.