Constant HW_MUTEX 

pub const HW_MUTEX: &str = "# Mutual Exclusion\n\
                            # The two grants are never high in the same cycle.\n\
                            \n\
                            Always, not both grant0 is high and grant1 is high.\n";

Mutual exclusion as one English sentence. Certified equivalent to its SVA like every spec above, but kept out of HARDWARE_EXAMPLES because the vacuity check only applies to implication-shaped specs (this one has no trigger to fire — “not both” is unconditional).