In Section 14.3

Change the first paragraph from:

All input or inout signals in a clocking domain are sampled at the clocking event of the corresponding

clocking. If the signal has a non-zero input skew then the value of the signal is sampled skew time units before

the clock edge (see figure 13-1 in section 13.3).

to (changes in blue):

All clocking domain inputs (input or inout) are sampled at the corresponding clocking event. If the input skew is non-zero then the value sampled corresponds to the signal value at read-only-sync [ROSYNC] of the time step skew time-units prior to the clocking event (see figure 13-1 in section 13.3). If the input skew is zero then the value sampled corresponds to the signal value at the start of the verification phase.

Add the following new paragraph at the end of Section 14.3

When the same signal is an input to multiple clocking domains, the semantics are straightforward; each clocking domain samples the corresponding signal with its own clocking event.