Reachable vs. non-reachable X statements

Rule: do not code reachable X statements. It is OK to code non-reachable X statements.

What does this mean? Basically, the designer knows when the X statement is reachable or not. Let's take case statements as an example. If it is a full case, then it's obvious that the default X statement is not reachable. If it is not a full case, there are two options:

1) Designer knows that case expression will never take certain values and synthesis can optimize for those truly don't-care situations. This is non-reachable X.
case (condition)
2'b01: A=1'b1;
2'b10: A=1'b0;
default: A='bx;

Designer knows that 'condition' will never have the values {2'b00, 2'b11} which makes the default X non-reachable. In this situation, designer should also add an SVA assertion to check his assumption so that during simulation the assertion checker will fire if 'condition' ever equals the above values.

2) Designer knows that case expression can take on all the values, but functionally only {2'b01, 2'b10} are important. This is reachable X. We do not allow synthesis to optimize for this case because the resulting gate-level will not be equal to RTL and bugs may be inadvertently introduced. There is no easy way to check the designer's assumption about the don't-care. In this situation, all case conditions should be explicitly specified to create a full case or the default statement should be assigned to a 2-state value.