Mutually exclusive Attribute

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.

Example

(* 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.