SVA cho bắt tay req/ack: $rose, |-> hay |=>, $past và disable iff

Assertion (SVA) là cách ghi đặc tả giao tiếp thành code mà simulator tự kiểm ở mọi nhịp. Ba câu tiếng Việt dưới đây trông đơn giản, nhưng mỗi câu có một chi tiết thời gian mà dịch sai sang SVA là checker im lặng bỏ qua bug, hoặc báo lỗi rác.

Giao tiếp req/ack, lấy mẫu ở cạnh lên clk, reset rst_n tích cực mức thấp:

• P1. Mỗi khi req chuyển từ 0 lên 1, ack phải bằng 1 ở ít nhất một trong 1, 2 hoặc 3 nhịp sau đó.
• P2. Ở nhịp nào có req = 1 và ack = 0, thì ở nhịp kế tiếp req vẫn phải bằng 1 (không được rút yêu cầu khi chưa được trả lời).
• P3. Mỗi khi ack chuyển từ 0 lên 1, ở nhịp trước đó req phải bằng 1.
• Trong lúc rst_n = 0, không kiểm gì, và mọi lần kiểm đang dở bị huỷ.

Viết module checker, mỗi vi phạm tăng bộ đếm tương ứng đúng một lần:

module reqack_chk (
  input  logic clk, rst_n, req, ack,
  output int   e1, e2, e3       // số lần vi phạm P1, P2, P3 (bắt đầu từ 0)
);
  // Gợi ý cấu trúc:
  //   p1: assert property (@(posedge clk) disable iff (!rst_n) …) else e1++;
endmodule

Testbench đổi req, ack ở cạnh xuống và so các bộ đếm với mô hình của nó sau mỗi kịch bản.