A Gray counter is a binary counter with its Gray image registered beside it. Both registers update together in the source domain, and only the Gray register crosses. Registering matters: a Gray value computed combinationally from the counter can glitch while the binary bits settle, putting several changing bits on the crossing in the very cycle the rule must hold.
The conversion g = b ^ (b >> 1) applies to the next binary value, so the two registers always agree. The destination decodes Gray back to binary with a running XOR from the top bit down, or compares Gray values directly as FIFO full and empty logic does (see async FIFO design).
A 4-bit Gray counter and a testbench that steps through all 16 values and checks that every step, including the wrap from 15 back to 0, flips exactly one bit, and that every value is visited.
`timescale 1ns/1ps
// 4-bit Gray counter for crossings: the binary count advances, and the Gray
// image of the NEXT value is registered alongside it. The crossing taps the
// registered Gray output, never a combinational conversion, so no glitch can
// reach the synchroniser.
module gray_counter (
input logic clk, rst_n, en,
output logic [3:0] gray
);
logic [3:0] bin, bin_next, gray_next;
assign bin_next = bin + (en ? 4'd1 : 4'd0);
assign gray_next = (bin_next >> 1) ^ bin_next;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) begin bin <= '0; gray <= '0; end
else begin bin <= bin_next; gray <= gray_next; end
endmodule
The Gray register is a flop in the source domain, fed by the conversion, with no logic between it and the synchroniser.
The adjacency proof covers the wrap step, not just the counting steps.
The enable cannot skip: when en is high the binary count advances by exactly one.
The counting steps prove single-bit change along the sequence, but only the wrap step proves the sequence is a cycle. A sequence that is Gray-ordered but does not wrap cleanly tears exactly when the pointer rolls over, which is the hardest failure to catch in system test.