The scheduler always attempts to deduce when two rules are mutually exclusive (based on their predicates). However, this deduction can fail even when two rules are actually exclusive - either because the scheduler effort limit is exceeded or because the mutual exclusion depends on a higher-level invariant that the scheduler does not know about. The mutually_exclusive attribute allows the designer to overrule the scheduler's deduction and forces the generated schedule to treat the annotated rules as exclusive.
(* mutually_exclusive = "r1, r2, r3" *)
This example specifies that every pair of rules that are in the annotation (i.e (r1, r2), (r1, r3), and (r2, r3)) is a mutually-exclusive rule pair.
Since an asserted mutual exclusion does not come with a proof of this exclusion, the compiler will insert code that will check if two rules ever execute during the same clock cycle during simulation. This allows a designer to find out when their use of the mutually_exclusive attribute is incorrect.