SVA cho valid/ready: giữ valid, giữ data và $onehot0

Giao tiếp valid/ready là xương sống của hầu hết bus on-chip: bên gửi đưa valid cùng data; giao dịch xảy ra ở nhịp có valid && ready. Hai quy tắc ổn định làm cho nó an toàn, và cả hai phải được kiểm bằng assertion trong mọi môi trường DV:

• P1. Ở nhịp nào có valid = 1 và ready = 0 (giao dịch đang chờ), ở nhịp kế tiếp valid vẫn phải bằng 1.
• P2. Trong cùng tình huống đó, ở nhịp kế tiếp data phải giữ nguyên giá trị của nhịp hiện tại.
• P3. Ở mọi nhịp, sel (4 bit) có nhiều nhất một bit 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ỷ.

Khi không có giao dịch đang chờ (valid = 0, hoặc ngay sau nhịp có valid && ready), valid và data được tự do thay đổi.

module vr_chk (
  input  logic       clk, rst_n, valid, ready,
  input  logic [7:0] data,
  input  logic [3:0] sel,
  output int         e1, e2, e3     // số lần vi phạm P1, P2, P3 (bắt đầu từ 0)
);

Mỗi vi phạm tăng bộ đếm tương ứng đúng một lần (dùng action block else eN++ của assert property). Testbench đổi tín hiệu ở cạnh xuống và so các bộ đếm với mô hình của nó.