VericodeRTL · DV · QUIZTìm bài học, kiến thức…Ctrl K
Học để hiểu. Thực hành để vững.

Local variables trong SVA: giữ dữ liệu riêng cho các attempt chồng lấn

Khoảng 55 phútMức 3/3Bản nháp: một số khẳng định chưa đối chiếu spec

Tiên quyết

Sau bài này bạn sẽ

  • Capture dữ liệu tại match và dùng lại ở deadline của chính attempt
  • Phân biệt local storage với một thanh ghi dùng chung
  • Chọn local variable hoặc history có độ sâu cố định theo bài toán

Giá trị mới nhất chưa chắc thuộc yêu cầu đang kiểm

Dữ liệu có thể thay đổi trước khi kết quả cần được kiểm. Nếu hai yêu cầu đang chờ, mỗi yêu cầu phải giữ giá trị của chính nó.

Giả sử lần đầu mang dữ liệu 3, lần sau mang 5. Khi kết quả của lần đầu về, đọc “giá trị mới nhất” sẽ lấy nhầm 5. Biến local trong property giúp gắn dữ liệu với attempt đang theo dõi.

Hai attempt chồng lấn giữ hai giá trị khác nhau

Xét yêu cầu phải được đáp ứng sau đúng hai tick. Hai cặp start liên tiếp tạo các nghĩa vụ sau:

Tick start Giá trị cần giữ Deadline Response sampled Kết luận
1 3 3 valid=1, out=3 Đúng
2 5 4 valid=1, out=5 Đúng
6 7 8 valid=1, out=7 Đúng
7 9 9 valid=1, out=8 Vi phạm

Khi attempt từ tick 2 đã giữ 5, attempt từ tick 1 vẫn cần 3. Response cuối cố ý sai để phân biệt kiểm nội dung với việc chỉ thấy out_valid là cho qua.

Assignment action gắn việc capture với một match

Property có thể khai báo bit [3:0] v;, rồi dùng (start, v=data) |-> ##2 (out_valid && out==v).

Dấu phẩy ở đây không tách ra một lệnh procedural chạy độc lập. Giá trị capture phải được dùng đúng trên đường match đã gán nó.

Khi start false, antecedent không match nên không tạo nghĩa vụ consequent cần v. Nếu bỏ implication, một sequence đứng riêng không tự có cùng cơ chế vacuity.

Vì sao biến dùng chung tạo báo động sai

Giả sử một biến module-level latest được cập nhật mỗi khi có start. Tới tick 3, latest đã bằng 5 từ yêu cầu tại tick 2; so response 3 với latest sẽ báo nhầm lỗi. Tới tick 8, tình huống tương tự xảy ra giữa dữ liệu 7 và 9.

Tick 9 lại có lỗi thật: response bằng 8 thay vì 9. Biến dùng chung vì thế vừa tạo báo động sai vừa khó chỉ ra nguồn dữ liệu của từng phép so.

Có một thanh ghi lưu giá trị gần nhất chưa có nghĩa đã có storage riêng cho mọi yêu cầu đang sống.

Khi history hai tick cũng trả đúng dữ liệu

Với độ trễ cố định hai tick và lịch sử hợp lệ, out == $past(data, 2) tại deadline cũng tìm đúng mẫu từ tick start.

Ở deadline tick 3, history hai tick trả data của tick 1 là 3. Hai attempt chồng lấn không tự làm cách dùng history cố định này sai.

Chọn local capture khi cần giữ giá trị gắn với một match cụ thể. Chọn history khi quan hệ số tick và điều kiện lịch sử hợp lệ đã rõ. Ví dụ này chưa giải quyết response đảo thứ tự, clock gating hoặc mọi độ trễ thay đổi.

Scope, kiểu dữ liệu và lúc giá trị hợp lệ

Biến v được khai báo trong property, còn latest nằm ở module. Đổi tên biến hoặc đưa nó vào một always block không tự tạo storage cho mỗi attempt.

Chọn kiểu và độ rộng đủ giữ biểu thức capture. Dữ liệu bị cắt hoặc đổi signedness vẫn có thể được lưu ổn định nhưng mang sai giá trị.

Biến cũng cần được gán hợp lệ trước khi đọc. Không suy từ một đường capture đơn rằng mọi nhánh and/or/intersect đều có thể chia sẻ và đọc biến theo cùng cách.

Bốn lỗi khi lưu dữ liệu cho attempt

  • Dùng giá trị gần nhất để kiểm mọi yêu cầu đang chờ.
  • Cho mọi lần capture cùng một giá trị nên không phát hiện mất isolation.
  • Chỉ kiểm out_valid mà chưa đối chiếu nội dung.
  • Dùng history sai độ sâu hoặc trước khi lịch sử hợp lệ.

Ghi lại tick start, dữ liệu được giữ và deadline. Sau đó mới chọn local storage, history cố định hay scoreboard theo ID.

Tự truy nguồn dữ liệu của từng phép so

  1. Tại tick 3, biến local, latest và history một tick lần lượt lấy dữ liệu từ đâu?
  2. Nếu đổi dữ liệu của start tại tick 2 thành 3, lỗi dùng chung storage nào sẽ khó thấy hơn?
  3. Nếu chuyển deadline từ hai tick xuống một tick, bảng cần đổi những dòng nào?
  4. Vì sao vẫn cần giữ response sai tại tick 9 khi kiểm một checker?

Kiểm tra

Capture theo từng attempt

  1. Start ở tick 1 capture giá trị 3, start ở tick 2 capture giá trị 5. Response cho start ở tick 1 đến tại tick 3 với out=3. v của attempt đầu phải bằng bao nhiêu?
  2. Theo bảng bốn yêu cầu, property giữ dữ liệu riêng và property dùng latest chung lần lượt báo bao nhiêu vi phạm?
  3. Failure thật duy nhất của property local nằm ở tick nào?
  4. Độ trễ trong ví dụ cố định hai tick. So out với $past(data,2) tại deadline có thể cho cùng kết quả với biến local không?
  5. Đổi so sánh out==v thành out==latest và đối chiếu lại từng yêu cầu trong bảng. Điều gì sẽ xảy ra?

Bằng chứng kiểm chứng

Expected tính trước chạy: LOCAL VAR CHECK samples=12 starts=4 responses=4 local_failures=1 local_mask=512 shared_failures=3 shared_mask=776 past_failures=1 past_mask=512 time_ns=120. Mười hai tick chạy qua deadline cuối 9 tới 12, và thời gian kết thúc thật được kiểm bằng $time.

SVA local-vars

Expected tính trước chạy: LOCAL VAR CHECK samples=12 starts=4 responses=4 local_failures=1 local_mask=512 shared_failures=3 shared_mask=776 past_failures=1 past_mask=512 time_ns=120

tb.sv testbench
`timescale 1ns/1ps// Expected before execution: starts1/2/6/7 capture3/5/7/9; responses3/4/8/9 are3/5/7/8.// Per-attempt local storage and fixed $past(data,2) each fail only at9 (mask512).// Shared latest fails3/8/9 (mask776).module tb_sva_local_variables;  bit clk = 0, start = 0, out_valid = 0;  bit [3:0] data = 0, out = 0, latest = 0;  int tick = 1, samples = 0, starts = 0, responses = 0;  int local_failures = 0, local_mask = 0, shared_failures = 0, shared_mask = 0;  int past_failures = 0, past_mask = 0;  always #5 clk = ~clk;  always @(posedge clk) begin    samples++;    if (start) begin starts++; latest <= data; end    if (out_valid) responses++;  end  property capture_per_attempt;    bit [3:0] v;    @(posedge clk) (start, v=data) |-> ##2 (out_valid && out==v);  endproperty  A_local: assert property (capture_per_attempt)    else begin local_failures++; local_mask |= 1 << tick; end  A_past: assert property (@(posedge clk) start |-> ##2 (out_valid && out==$past(data, 2)))    else begin past_failures++; past_mask |= 1 << tick; end  // Intentionally incorrect comparison: independent requests share the latest capture.  A_shared: assert property (@(posedge clk) start |-> ##2 (out_valid && out==latest))    else begin shared_failures++; shared_mask |= 1 << tick; end  initial begin    for (int cycle = 1; cycle <= 12; cycle++) begin      if (cycle > 1) @(negedge clk);      tick = cycle;      start = cycle==1 || cycle==2 || cycle==6 || cycle==7;      case (cycle)        1: data = 3;        2: data = 5;        6: data = 7;        7: data = 9;        default: data = 0;      endcase      out_valid = cycle==3 || cycle==4 || cycle==8 || cycle==9;      case (cycle)        3: out = 3;        4: out = 5;        8: out = 7;        9: out = 8;        default: out = 0;      endcase    end    @(negedge clk);    $display("LOCAL OBSERVED local=%0d mask=%0d shared=%0d mask=%0d", local_failures, local_mask, shared_failures, shared_mask);    if ($time!=120 || samples!=12 || starts!=4 || responses!=4 || local_failures!=1 ||        local_mask!=512 || past_failures!=1 || past_mask!=512 || shared_failures!=3 || shared_mask!=776)      $fatal(1, "per-attempt local variable isolation oracle");    $display("LOCAL VAR CHECK samples=12 starts=4 responses=4 local_failures=1 local_mask=512 shared_failures=3 shared_mask=776 past_failures=1 past_mask=512 time_ns=%0d", $time);    $finish;  endendmodule

Đã kiểm chứng thế nào

  • Phân tích và elaborate theo LRM (pyslang 12.1.0)
  • Mô phỏng, exit 0 và output khớp kỳ vọng tính tay (Verilator 5.050, 2-state)

Output phải khớp: LOCAL VAR CHECK samples=12 starts=4 responses=4 local_failures=1 local_mask=512 shared_failures=3 shared_mask=776 past_failures=1 past_mask=512 time_ns=120

Verilator 2 state, unsigned 4 bit, four starts, fixed 2 tick deadlines. No general variable-flow, arbitrary latency, X/Z or out-of-order scoreboard claim.

Shared latest is an intentionally incorrect comparison. Fixed-depth past is valid in this chosen contract and compared independently.

Các kiểm tra chạy lúc xây dựng nội dung (2026-11-06), không chạy trong trình duyệt. Kỳ vọng được tính tay trước khi chạy.

Property shared được đặt cạnh property local để minh họa lỗi lưu expected, không phải một đề xuất checker tốt. Property past là đối chiếu đúng cho contract cố định đang dùng. Cả sample/start/response count và các mask đều được kiểm, nên đổi stimulus hoặc tắt checker không thể chỉ giữ một dòng output đẹp.

Giữ nguyên bốn mutant: capture data+1, dùng latest thay v, đổi deadline hai tick thành một tick và đổi history hai tick thành một tick. Chúng parse/build rồi bị bắt ở runtime. Property shared là đối chứng sai có chủ đích; property history là đối chiếu đúng trong hợp đồng độ trễ cố định này. Mô phỏng chỉ xét unsigned 4 bit, dữ liệu 0–9 và mô hình 2-state; chưa kiểm X/Z hoặc flow biến qua các nhánh sequence phức tạp.

[2] [3]

Bài liên quan

Nguồn và mức độ đối chiếu

  1. IEEE 1800-2023 SystemVerilog LRM, Assertion local variables, match items and variable flow — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. Local Variables in Assertion Properties — bản chụp resources.zip, The Problem: A Signal Can Change Before You're Ready to Check It; Declaring and Assigning a Local Variable; Comparing Both Versions on the Same Trace; Local Variables Track Each Attempt Independently; Common Beginner Mistakes. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. Thí nghiệm nguyên bản B8.local-vars, Four overlapping captures, fixed-depth history comparison and four runtime mutants. Trích dẫn; nguồn đã đọc toàn văn.
  4. IEEE 1800-2023 SystemVerilog LRM, Sequence operators and assertion local variables — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).