FIFO bất đồng bộ hai clock (con trỏ Gray)

Khi dữ liệu đi giữa hai miền clock không liên quan, ví dụ từ bộ thu 125 MHz sang bus hệ thống 100 MHz, người ta dùng FIFO bất đồng bộ. Đây là câu phỏng vấn "boss" của mảng RTL: nó gom gần đủ mọi thứ về CDC (clock domain crossing). Bài này theo kiến trúc kinh điển: con trỏ mã Gray đi qua bộ đồng bộ 2 flip-flop.

module afifo (
  // miền ghi
  input  logic       wclk,
  input  logic       wrst_n,     // reset bất đồng bộ, tích cực thấp
  input  logic       winc,       // ghi wdata ở sườn lên này (bị bỏ qua nếu wfull = 1)
  input  logic [7:0] wdata,
  output logic       wfull,
  // miền đọc
  input  logic       rclk,
  input  logic       rrst_n,
  input  logic       rinc,       // lấy phần tử đầu ra khỏi FIFO ở sườn lên này (bị bỏ qua nếu rempty = 1)
  output logic [7:0] rdata,      // phần tử đầu: hợp lệ khi rempty = 0 (first-word fall-through)
  output logic       rempty
);

Sâu 8 phần tử. Yêu cầu:

1. Đúng dữ liệu: mọi phần tử ghi vào đều đọc ra đúng thứ tự, không mất, không lặp. rdata luôn là phần tử đầu, không cần chờ một nhịp sau rinc.
2. Bảo vệ: winc khi wfull = 1 và rinc khi rempty = 1 bị bỏ qua.
3. Cờ chính xác trong miền của chính nó: nếu bên đọc không đọc thì wfull lên ngay sau lần ghi thứ 8 tính từ lúc rỗng. Nếu bên ghi không ghi thì rempty lên ngay sau khi đọc phần tử cuối.
4. Cờ ở miền bên kia được phép bi quan, nhưng trễ có giới hạn: sau một lần ghi vào FIFO rỗng, rempty về 0 trong tối đa 4 sườn rclk. Sau một lần đọc từ FIFO đầy, wfull về 0 trong tối đa 4 sườn wclk.
5. wfull và rempty là ngõ ra flip-flop. Sau reset (cả hai reset cùng lúc): rempty = 1, wfull = 0.

Testbench đổi tín hiệu của mỗi miền ở sườn xuống của clock miền đó, và chỉ ghi khi wfull = 0, chỉ đọc khi rempty = 0 (trừ các case cố ý vi phạm để kiểm yêu cầu 2).

Mô phỏng RTL không có metastability. Dùng con trỏ nhị phân đi thẳng qua miền kia cũng có thể qua test, nhưng sẽ hỏng trên silicon. Lời giải đúng phải dùng Gray + 2 flip-flop. Phần lời giải giải thích vì sao.