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

Hàm sampled: bit nào đổi, lịch sử ở clock nào và log đang thấy gì?

Khoảng 55 phútMức 2/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ẽ

  • Phân biệt chuyển mức của bit thấp nhất với thay đổi của cả vector
  • Tính lịch sử một và hai tick cho pipeline, có guard đủ mẫu
  • Đọc giá trị sampled trong assertion action thay vì suy từ log live

Hai mẫu của cùng một clock khác hai thời điểm bất kỳ

Một tín hiệu có thể đổi giữa hai cạnh rồi trở về giá trị cũ. Nếu hai mẫu tại posedge bằng nhau, phép so mẫu vẫn thấy không đổi. Nó chưa trả lời tín hiệu có glitch trong cả khoảng giữa hai cạnh hay không.

Trước khi chọn hàm, xác định clock lấy mẫu và điều cần phát hiện: bit chuyển mức, vector đổi, hay giá trị từ một tick trước.

Rose và fell nhìn bit thấp nhất

Trong ví dụ 2-state, $rose(data) xét bit thấp nhất chuyển từ 0 lên 1; $fell(data) xét bit ấy chuyển từ 1 xuống 0.

Với vector hai bit, 00 đổi thành 10 chưa tạo rose của data vì bit thấp nhất vẫn bằng 0. 10 đổi thành 11 mới tạo rose. Đây không phải phép kiểm giá trị số tăng hay có bất kỳ bit nào đổi.

Các kết quả dưới đây chỉ xét 0 và 1. Chuyển mức có X/Z cần bảng quy tắc riêng, không suy từ mô phỏng 2-state.

Stable và changed so cả vector

$stable(data) so cả vector giữa hai mẫu; $changed(data) phát hiện vector thay đổi. Đổi riêng bit cao vẫn làm changed đúng.

Tick data Rose Fell Stable cả vector Changed cả vector
1 00 — — — —
2 10 0 0 0 1
3 11 1 0 0 1
4 11 0 0 1 0
5 01 0 0 0 1
6 00 0 1 0 1
7 10 0 0 0 1
8 11 1 0 0 1

Dấu — cho biết bảng không so mẫu đầu với lịch sử trước đó; nó không biểu diễn X hay false. 11 giữ 11 vẫn stable. Một tín hiệu giữ high nhiều tick cũng chỉ có rose tại chuyển mức tương ứng.

Past một tick và hai tick trong pipeline

Hai stage được cập nhật bằng non-blocking: q1 <= data và q2 <= q1 tại mỗi posedge. Trước cập nhật cạnh hiện tại, q1 chứa data của tick trước, q2 chứa data của hai tick trước.

Khi đã có đủ mẫu hợp lệ, kiểm q1 == $past(data) và q2 == $past(data, 2).

Tại tick 3 Giá trị sampled Đến từ đâu?
data 11 Input của tick 3
q1 10 Input của tick 2
q2 00 Input của tick 1

Dùng history một tick để kiểm q2 sẽ lấy 10 thay vì 00. Hãy đếm stage theo tick của clock đã chọn, không thay history bằng delay nanosecond.

Có giá trị khởi đầu chưa có nghĩa đã có lịch sử hợp lệ

Trước khi có đủ tick thật, history có thể trả giá trị khởi đầu theo kiểu và ngữ cảnh. Giá trị đó chưa nhất thiết đại diện cho một giao dịch đã đi qua pipeline.

Ví dụ này cho phép kiểm q1 từ tick 2 và q2 từ tick 3. Trong thiết kế có reset, hãy xác định khi nào dữ liệu lịch sử lại hợp lệ. Disable một property không tự chứng minh lịch sử nghiệp vụ đã được làm mới.

Gating của history chọn những tick được tính vào lịch sử; enable trong antecedent chọn lúc tạo nghĩa vụ. Hai vai trò này cần được phân biệt.

Sampled giúp action block ghi đúng mẫu đã được kiểm

Một action block đọc biến trực tiếp có thể thấy giá trị đã đổi sau lúc assertion lấy mẫu. $sampled giúp ghi lại mẫu assertion đã dùng, trong ngữ cảnh clock phù hợp.

Ví dụ stamp bằng 0 trước cạnh đầu, rồi tăng bằng blocking trong Active. Mẫu dùng cho assertion vẫn là 0, còn đọc stamp trực tiếp sau cập nhật cho 1. Việc tăng blocking này phục vụ minh họa scheduling, không phải cách viết một thanh ghi RTL.

Trong property, dữ liệu đã chịu ngữ nghĩa lấy mẫu của concurrent assertion. Không cần thêm $sampled vào mọi chỗ. Khi gọi từ ngữ cảnh khác, phải xác định tính hợp lệ và clock của lời gọi.

Bốn nhầm lẫn cần tránh

  • Dùng rose/fell để hỏi có bit bất kỳ thay đổi.
  • Dùng stable để kết luận tín hiệu không glitch giữa hai cạnh.
  • Dùng history trước khi đủ dữ liệu hợp lệ.
  • Lấy giá trị trực tiếp trong log để giải thích mẫu của assertion.

Chọn hàm từ câu hỏi cần kiểm, rồi xác định clock và độ sâu lịch sử.

Tự chọn hàm và độ sâu lịch sử

  1. Trong bảng, nếu so riêng data[0], những thay đổi nào của vector sẽ bị bỏ qua?
  2. Ở tick 3, vì sao q2 cần history hai tick thay vì một tick?
  3. Nếu action block in stamp bằng 1, có thể kết luận assertion đã kiểm mẫu 1 không?
  4. Sau reset, cần bổ sung điều kiện gì trước khi kiểm pipeline bằng $past?

Kiểm tra

Hàm sampled và lịch sử

  1. Trong hai mẫu 2-state liên tiếp, data đổi từ 00 sang 10. $rose(data) và $changed(data) là gì?
  2. data ở tick 3 và tick 4 đều bằng 11. $stable(data) ở tick 4 là gì?
  3. Ở tick 3, ba mẫu data đầu tiên lần lượt là 00/10/11. Hai stage NBA đã chạy từ đầu. q2 phải được so với giá trị nào?
  4. Trong action của cạnh đầu, sampled_stamp=0 còn raw_stamp=1. Thay $sampled(stamp) bằng stamp có giữ đúng log của mẫu đã kiểm không?
  5. Một bus có cùng giá trị ở hai posedge nhưng đổi rồi trở lại giữa hai cạnh. Stable trên hai mẫu có chứng minh bus không glitch trong khoảng đó không?

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

Expected tính trước chạy từ bảng: SAMPLED FN CHECK samples=8 edge_checks=28 rose=2 fell=1 stable=1 changed=6 past1=7 past2=6 sampled_stamp=0 raw_stamp=1 failures=0 time_ns=80. Counters nằm trong action của các property; tắt checker không thể tạo đủ 28 edge-check và các history-check bằng cách chỉ chạy stimulus.

Sampled functions, vector edges and pipeline history

Expected tính trước chạy: SAMPLED FN CHECK samples=8 edge_checks=28 rose=2 fell=1 stable=1 changed=6 past1=7 past2=6 sampled_stamp=0 raw_stamp=1 failures=0 time_ns=80

tb.sv testbench
`timescale 1ns/1ps// Expected before execution: 00,10,11,11,01,00,10,11.// Compare samples 2..8: LSB rises at3/8, falls at6; entire vector stable only at4.// Seven one-tick history checks, six two-tick checks. First stamp: sampled0/raw1.module tb_sampled_functions;  bit clk = 0;  bit [1:0] data = 0, q1 = 0, q2 = 0;  bit hist_valid = 0, hist2_valid = 0, first_tick = 0;  bit expected_rose = 0, expected_fell = 0, expected_stable = 0;  int samples = 0, stamp = 0, sampled_stamp = -1, raw_stamp = -1;  int edge_checks = 0, rose_hits = 0, fell_hits = 0, stable_hits = 0, changed_hits = 0;  int past1_checks = 0, past2_checks = 0, failures = 0;   always #5 clk = ~clk;  always @(posedge clk) begin    samples++;    stamp++; // Deliberate Active update, solely to test sampled versus live logging.    q1 <= data;    q2 <= q1;  end   A_rose: assert property (@(posedge clk) hist_valid |-> ($rose(data) == expected_rose))    begin      if (hist_valid) begin edge_checks++; if (expected_rose) rose_hits++; end    end else failures++;  A_fell: assert property (@(posedge clk) hist_valid |-> ($fell(data) == expected_fell))    begin      if (hist_valid) begin edge_checks++; if (expected_fell) fell_hits++; end    end else failures++;  A_stable: assert property (@(posedge clk) hist_valid |-> ($stable(data) == expected_stable))    begin      if (hist_valid) begin edge_checks++; if (expected_stable) stable_hits++; end    end else failures++;  A_changed: assert property (@(posedge clk) hist_valid |-> ($changed(data) == !expected_stable))    begin      if (hist_valid) begin edge_checks++; if (!expected_stable) changed_hits++; end    end else failures++;  A_past1: assert property (@(posedge clk) hist_valid |-> (q1 == $past(data)))    begin if (hist_valid) past1_checks++; end else failures++;  A_past2: assert property (@(posedge clk) hist2_valid |-> (q2 == $past(data, 2)))    begin if (hist2_valid) past2_checks++; end else failures++;  A_snapshot: assert property (@(posedge clk) 1'b1)    begin      if (first_tick) begin sampled_stamp = $sampled(stamp); raw_stamp = stamp; end    end   initial begin    for (int cycle = 1; cycle <= 8; cycle++) begin      if (cycle > 1) @(negedge clk);      case (cycle)        1, 6: data = 2'b00;        2, 7: data = 2'b10;        3, 4, 8: data = 2'b11;        5: data = 2'b01;      endcase      first_tick = cycle == 1;      hist_valid = cycle >= 2;      hist2_valid = cycle >= 3;      expected_rose = cycle == 3 || cycle == 8;      expected_fell = cycle == 6;      expected_stable = cycle == 4;    end    @(negedge clk);    if ($time != 80 || samples != 8 || edge_checks != 28 || rose_hits != 2 || fell_hits != 1 ||        stable_hits != 1 || changed_hits != 6 || past1_checks != 7 || past2_checks != 6 ||        sampled_stamp != 0 || raw_stamp != 1 || failures != 0)      $fatal(1, "sampled function history and logging oracle");    $display("SAMPLED FN CHECK samples=8 edge_checks=28 rose=2 fell=1 stable=1 changed=6 past1=7 past2=6 sampled_stamp=0 raw_stamp=1 failures=0 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: SAMPLED FN CHECK samples=8 edge_checks=28 rose=2 fell=1 stable=1 changed=6 past1=7 past2=6 sampled_stamp=0 raw_stamp=1 failures=0 time_ns=80

Verilator 2-state; excludes X/Z transitions and first-sample history defaults. Seven one-tick and six two-tick history checks only.

Gated $past probe is parsed but build unsupported, retained separately. Sampled logging is in a clocked assertion action; no claim for arbitrary procedural contexts.

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.

Đây là simulation Verilator 2-state có oracle hữu hạn, không phải proof cho mọi trace, X/Z hoặc mọi sampled-function argument. Thời gian thực được kiểm bằng $time, không chỉ in một hằng số cuối log.

Bốn mutant thay bit xét rose, thu stable xuống bit thấp, đổi độ sâu history và thay sampled bằng giá trị live đều phải parse/build rồi bị bắt ở runtime. Ví dụ chính chỉ kiểm 2-state và lời gọi history hai đối số. Thí nghiệm $past có gating được pyslang chấp nhận nhưng Verilator báo unsupported; chưa có kết quả mô phỏng đạt cho dạng đó.

[2] [3] [4]

Bài liên quan

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

  1. IEEE 1800-2023 SystemVerilog LRM, Sampled value functions, clock inference and expression history — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. SystemVerilog $rose, $fell, $stable — bản chụp resources.zip, $rose; $fell; $stable; Comparing All Four on the Same Trace; Common Beginner Mistakes. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. Assertions $past, $sampled, $changed — bản chụp resources.zip, $past: Reaching Back Further Than One Cycle; $sampled: Reading a Signal's Assertion-Visible Value; $changed: The Opposite of $stable; Common Beginner Mistakes. Trích dẫn; nguồn đã đọc các mục liên quan.
  4. Thí nghiệm nguyên bản B8.sampled-fn, Eight-sample vector trace, pipeline history, sampled logging and four runtime mutants. Trích dẫn; nguồn đã đọc toàn văn.
  5. IEEE 1800-2023 SystemVerilog LRM, Sampled value functions and clock context — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  6. IEEE 1800-2023 SystemVerilog LRM, Sampled value functions — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).