If you bring the count value to output ports, i.e. if you need those exact values, then it will synthesize to what you want. Otherwise, internally it is synthesizing to what is generally the best result. Generally the only reason to use a gray-code counter is to cross clock-domains(and therefore remove the glitches). But otherwise you want what the original binary code. EVERYTHING has different delays in a device, so when you look at multiple signals as a group, they will always look like they're glitching to a different value. That is what static timing analysis does, is it basically determines that your transitiions occur between clock edges, and when the clock samples a state, all the signals are not transitioning and are at the correct state. In your original attachment where you show the "wrong state", it is not what you want, but since you're not using the value of count until the next clock edge, these glitched have filtered out. (Unless you're crossing asynchronous domains). So your code was fine without doing a gray-code.