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

Disable iff: hủy nghĩa vụ đang chờ và phân biệt với gating

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 antecedent false với attempt bị hủy
  • Theo dõi nghĩa vụ trước, trong và sau reset
  • Đọc đúng giới hạn clock-visible reset của ví dụ đã chạy

Reset có được hủy yêu cầu đang chờ không?

Một start yêu cầu done sau hai tick. Nếu reset xuất hiện trước deadline, yêu cầu ấy còn phải được đáp ứng không?

Hãy trả lời từ yêu cầu thiết kế. Trong ví dụ này, reset được phép hủy nghĩa vụ đang chờ. Hủy nghĩa vụ khác với đáp ứng thành công, và cũng khác với một vi phạm.

Theo dõi yêu cầu trước và sau reset

Clock có cạnh lên ở 5, 15, 25 ns rồi tiếp tục mỗi 10 ns. Reset high từ 12 đến 23 ns: sau start tại tick 1 nhưng trước deadline ở tick 3. Done chỉ đúng tại tick 10.

Start Deadline Có disable iff (rst) Chỉ có !rst trong antecedent
Tick 1 Tick 3 Nghĩa vụ bị hủy trong reset Vẫn cần done tại tick 3, nên vi phạm
Tick 5 Tick 7 Vi phạm vì done bằng 0 Vi phạm vì done bằng 0
Tick 8 Tick 10 Done đáp ứng đúng hạn Done đáp ứng đúng hạn

Lỗi tại tick 7 cho thấy yêu cầu sau reset vẫn phải được kiểm. Không nên kéo reset tới hết mô phỏng chỉ để mọi vi phạm biến mất.

Điều kiện disable khác mẫu Boolean của antecedent

Dạng có clock explicit là @(posedge clk) disable iff (rst) start |-> ##2 done.

Với (!rst && start) |-> ##2 done, reset lại nằm trong antecedent được lấy mẫu theo clock. Đó là một cách chọn điều kiện tạo nghĩa vụ, không phải cú pháp hủy nghĩa vụ cũ.

Gating chỉ đổi lúc tạo nghĩa vụ mới

Tại tick 1, reset low nên cả hai cách viết đều tạo nghĩa vụ cho tick 3. Reset high sau đó không làm mẫu antecedent ở tick 1 trở thành false. Nghĩa vụ cũ của cách viết chỉ gating vẫn còn.

Gating không có nghĩa concurrent assertion ngừng được đánh giá ở các tick của nó. Trong ví dụ này, nó ngăn tạo nghĩa vụ non-vacuous mới khi reset được sample high.

Sau reset, cần kiểm cả việc bắt đầu yêu cầu mới và việc phát hiện lỗi hợp lệ. Lịch sử nghiệp vụ của $past cũng cần điều kiện hợp lệ riêng; hủy attempt không tự chứng minh dữ liệu lịch sử đã được làm mới.

Thử reset nằm giữa hai cạnh clock

Reset có thể đổi giữa hai cạnh clock. Ví dụ, xung từ 12 đến 13 ns nằm sau start tại 5 ns nhưng kết thúc trước cạnh kế tại 15 ns.

Nếu yêu cầu thiết kế cho phép reset ấy hủy nghĩa vụ đang chờ, hãy kiểm riêng tình huống này. Nó khác tình huống reset high qua cạnh sample trong bảng trên.

Cũng cần thử trường hợp reset xuất hiện khi chưa có nghĩa vụ và khi nhiều nghĩa vụ đang sống. Phần bằng chứng cuối bài ghi rõ trường hợp công cụ hiện tại đã chạy đúng và trường hợp còn chưa đạt.

Không đoán ưu tiên khi reset đổi đúng cạnh clock

Khi reset đổi đúng cạnh clock, cần biết phép cập nhật nằm trong Active hay NBA và điều kiện disable được xét tại đâu. Không suy thứ tự thực thi từ vị trí hai block trong file.

Ví dụ trong bảng tránh điểm tranh chấp: reset lên tại 12 ns và xuống tại 23 ns, tách khỏi các cạnh 5, 15, 25 ns. Nó chưa giải quyết mọi cách release reset hoặc trường hợp X/Z.

Thêm $sampled(rst) vào điều kiện disable cũng thay đổi câu hỏi đang kiểm. Hãy xác định ý nghĩa mong muốn trước khi đổi biểu thức.

Bốn lỗi thường gặp khi kiểm reset

  • Dùng gating antecedent như thể nó xóa nghĩa vụ cũ.
  • Xem nghĩa vụ bị hủy là một lần đáp ứng thành công.
  • Chỉ thử reset trước khi start, chưa thử reset giữa lúc đang chờ.
  • Hủy quá rộng khiến lỗi thật sau reset bị bỏ qua.

Một bài kiểm reset cần theo dõi trước reset, trong lúc có nghĩa vụ, sau release và deadline của yêu cầu mới.

Tự phân tích việc hủy và đáp ứng

  1. Nếu bỏ disable iff, nghĩa vụ từ start tại tick 1 sẽ kết luận thế nào?
  2. Nếu done xuất hiện sớm hơn deadline một tick, điều đó đã đáp ứng yêu cầu “đúng hai tick sau” chưa?
  3. Vì sao phải thử riêng xung reset nằm hoàn toàn giữa hai cạnh?
  4. Cần giữ một lỗi sau reset để phát hiện điều gì?

Kiểm tra

Reset, gating và cancellation

  1. Với reset 12–23 ns, start tại tick 1/5/8 và done chỉ tại tick 10 trong bảng, số vi phạm của property có disable và property chỉ gating lần lượt là bao nhiêu?
  2. Trong bảng thời gian, vi phạm còn lại của property có disable xuất hiện ở đâu?
  3. Ví dụ reset đi qua cạnh 15 ns đã chạy đúng. Kết quả đó đã xác nhận việc hủy nghĩa vụ với xung 12–13 ns chưa?
  4. Một assertion cần hai mẫu dữ liệu hợp lệ sau reset để so $past. Chỉ thêm disable iff có đủ chứng minh history nghiệp vụ hợp lệ ngay sau release không?
  5. Theo contract cancellation được trình bày, attempt bị disable hủy phải được coi là gì khi phân tích kết quả?

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

Expected tính trước chạy: DISABLE IFF CHECK samples=10 starts=3 done_samples=1 reset_pulses=1 disabled_failures=1 disabled_mask=128 gated_failures=2 gated_mask=136 time_ns=100. Main dùng Verilator 2-state và không dựa vào pass-action counter để đại diện cho cancellation.

Clock-visible reset cancellation versus antecedent gating

Expected tính trước chạy: DISABLE IFF CHECK samples=10 starts=3 done_samples=1 reset_pulses=1 disabled_failures=1 disabled_mask=128 gated_failures=2 gated_mask=136 time_ns=100

tb.sv testbench
`timescale 1ns/1ps// Expected before execution: ten samples at5..95ns; starts1/5/8 and done10.// Reset12..23ns includes sample2, so the first disable-iff obligation is canceled.// Without cancellation, deadlines3/7 fail; with it, only7 fails. Masks136/128.module tb_disable_clock_visible;  bit clk = 0, rst = 0, start = 0, done = 0;  int tick = 1, samples = 0, starts = 0, done_samples = 0, reset_pulses = 0;  int disabled_failures = 0, disabled_mask = 0, gated_failures = 0, gated_mask = 0;  time reset_rise = 0, reset_release = 0;  always #5 clk = ~clk;  always @(posedge clk) begin    samples++;    if (start) starts++;    if (done) done_samples++;  end  always @(posedge rst) begin reset_pulses++; reset_rise = $time; end  always @(negedge rst) if ($time > 0) reset_release = $time;   A_disable: assert property (@(posedge clk) disable iff (rst) start |-> ##2 done)    else begin disabled_failures++; disabled_mask |= 1 << tick; end  A_gated: assert property (@(posedge clk) (!rst && start) |-> ##2 done)    else begin gated_failures++; gated_mask |= 1 << tick; end   initial begin #12 rst = 1; #11 rst = 0; end  initial begin    for (int cycle = 1; cycle <= 10; cycle++) begin      if (cycle > 1) @(negedge clk);      tick = cycle;      start = cycle == 1 || cycle == 5 || cycle == 8;      done = cycle == 10;    end    @(negedge clk);    $display("DISABLE COUNTS disabled=%0d mask=%0d gated=%0d mask=%0d", disabled_failures, disabled_mask, gated_failures, gated_mask);    if ($time != 100 || samples != 10 || starts != 3 || done_samples != 1 || reset_pulses != 1 ||        reset_rise != 12 || reset_release != 23 || disabled_failures != 1 || disabled_mask != 128 ||        gated_failures != 2 || gated_mask != 136)      $fatal(1, "clock-visible reset cancellation oracle");    $display("DISABLE IFF CHECK samples=10 starts=3 done_samples=1 reset_pulses=1 disabled_failures=1 disabled_mask=128 gated_failures=2 gated_mask=136 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: DISABLE IFF CHECK samples=10 starts=3 done_samples=1 reset_pulses=1 disabled_failures=1 disabled_mask=128 gated_failures=2 gated_mask=136 time_ns=100

Verilator 2-state, reset 12..23 ns spans a sampled clock edge. No claim for all asynchronous cancellation, same-edge reset races or X/Z.

Separate reset 12..13 ns probe retains expected 1/mask 128 but observes 2/mask 136 and fails its runtime oracle. It is not a simulated-PASS main.

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.

Lỗi tại tick 7 có chủ đích xác nhận checker đã hoạt động sau reset. Mask giữ được thời điểm vi phạm, còn các counter stimulus/time giữ được scenario đang kiểm. Không dùng nhãn simulated của main để nâng probe giữa hai cạnh thành supported.

Phản ví dụ còn giữ: xung reset 12–13 ns có yêu cầu cancellation với một failure và mask 128, nhưng Verilator 5.050 quan sát hai failure và mask 136. Source parse/build được; kết quả runtime bị từ chối. Không đổi kỳ vọng, kéo dài pulse hoặc bỏ assertion để gọi là PASS. Ba mutant bỏ disable, đổi deadline và đưa done sớm đều bị bắt sau parse/build. Việc chạy đúng trường hợp reset 12–23 ns không chứng minh công cụ xử lý đúng abort giữa hai cạnh.

[2] [3]

Bài liên quan

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

  1. IEEE 1800-2023 SystemVerilog LRM, Concurrent assertion disabling, unsampled disable conditions and attempt lifecycle — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. SystemVerilog Assertions disable iff — bản chụp resources.zip, Syntax; Why Gating the Antecedent Isn't Enough; A Concrete Example: Aborting a Check Mid-Flight; 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.disable-iff, Clock-visible reset, deadline masks, three runtime mutants and retained between-edge cancellation failure. Trích dẫn; nguồn đã đọc toàn văn.
  4. IEEE 1800-2023 SystemVerilog LRM, Disabling versus sampled history — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  5. IEEE 1800-2023 SystemVerilog LRM, Concurrent assertion attempt lifecycle and disabling — 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, Assertion disabling and attempt cancellation — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).