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

SVA sampling: property thấy mẫu trước cạnh, log có thể thấy giá trị mới

Khoảng 50 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ẽ

  • Tách sampled q khỏi raw q đổi trong Active
  • Phân biệt clock explicit với default clocking trong scope đã kiểm
  • Dùng property sai có chủ đích để phát hiện checker bị tắt

Vì sao property thấy 0 còn log in ra 1?

Tại cạnh clock đầu tiên, DUT đổi q từ 0 sang 1. Một property kiểm q == 0 vẫn có thể đúng ở cạnh ấy, dù log sau cập nhật in ra 1.

Hai kết quả dùng dữ liệu ở hai thời điểm quan sát khác nhau. Concurrent assertion dùng giá trị đã lấy mẫu; log đọc trực tiếp tín hiệu có thể thấy giá trị vừa thay đổi. Hãy theo một cạnh clock để thấy rõ sự khác biệt.

Một cạnh clock đi qua nhiều vùng xử lý

Ví dụ chuẩn bị q = 0 và seen = 0 trước cạnh lên tại 5 ns. Ở cạnh đó, DUT gán q = 1 bằng blocking và tăng seen bằng non-blocking.

Minh họa sampling: q được lấy mẫu bằng 0 trước cạnh 5 ns; giá trị trực tiếp đổi thành 1 sau Active. Hình giải thích, không phải waveform trích từ mô phỏng.

Trong mô hình scheduling của SystemVerilog, concurrent assertion lấy mẫu ở Preponed, rồi đánh giá property ở Observed. Action block được xử lý sau bước đánh giá. Những bước này có thể cùng timestamp 5 ns mà dùng các giá trị khác nhau.

[2]

Theo dõi q và seen tại cạnh đầu

Bước q đọc trực tiếp seen đọc trực tiếp Mẫu dùng trong property
Trước cạnh 5 ns 0 0 q = 0, seen = 0
Active: gán q bằng blocking 1 0; phép tăng đang chờ NBA Vẫn q = 0, seen = 0
Sau cập nhật NBA 1 1 Vẫn q = 0, seen = 0
Observed: đánh giá property 1 1 q = 0, seen = 0
Đọc trực tiếp tại 6 ns 1 1 Không thay đổi mẫu của cạnh trước

Bảng là minh họa thứ tự xử lý. Khi property dùng điều kiện seen == 0, nó chọn mẫu của cạnh đầu. Giá trị seen đã tăng sau NBA không làm mẫu cũ biến thành 1.

Viết clock ngay trong property

Property @(posedge clk) (seen == 0) |-> (q == 0) kiểm mẫu q tại cùng tick có mẫu seen bằng 0. Theo bảng, điều kiện này đúng ở cạnh đầu.

Nếu đổi vế phải thành q == 1, property phải báo vi phạm ở cạnh ấy. Nó vẫn nhìn mẫu 0, dù câu lệnh trong DUT đã ghi giá trị mới bằng 1.

Trong ví dụ này, phép gán blocking tạo khác biệt rõ giữa mẫu và giá trị trực tiếp. Khi viết state RTL, hãy áp dụng kỷ luật non-blocking đã học ở A7; đừng sao chép cách bố trí thí nghiệm vào mọi register.

Dùng clock mặc định của scope

Khai báo default clocking cb @(posedge clk); endclocking cung cấp clock mặc định trong scope. Property hợp lệ có thể dùng context ấy mà không lặp lại event ở từng biểu thức.

Tên biến clk tự nó không cung cấp clock cho property. Cũng đừng đồng nhất việc dùng clock mặc định với việc đọc một clocking input có skew: đó là những câu hỏi khác nhau. Bài này chỉ xét clock mặc định với cạnh lên đã nêu.

[3]

Ghi log đúng giá trị cần quan sát

Trước khi so một log với property, hãy hỏi: dòng log đang mô tả mẫu tại cạnh clock hay giá trị trực tiếp lúc in?

Khi cần quan sát mẫu của assertion trong action block, dùng $sampled với biểu thức và ngữ cảnh clock phù hợp. Đọc q trực tiếp sau cập nhật có thể trả lời một câu hỏi khác. Tại 6 ns, q và seen đều bằng 1; điều đó không viết lại mẫu 0 của cạnh 5 ns.

Các hàm $past, $rose và lịch sử mẫu được học riêng ở bài sampled-value functions. Trước hết hãy xác định đúng mẫu hiện tại và clock đang dùng.

Dùng một lỗi biết trước để kiểm checker

Giữ một property cố ý đòi mẫu q == 1 ở cạnh đầu. Ta đã biết yêu cầu ấy sai, nên checker phải báo đúng một vi phạm. Nếu không báo, cần kiểm cấu hình bật assertion và điều kiện kích hoạt.

Đối chứng này bổ sung cho các property đúng. Nó phát hiện tình huống “không có lỗi” chỉ vì checker không chạy. Hãy giữ đối chứng sai cố ý khi kiểm công cụ, đồng thời tách nó khỏi yêu cầu đúng của thiết kế.

Ba nhầm lẫn cần tránh

  • Lấy giá trị sau cập nhật để giải thích một property dùng mẫu trước cập nhật.
  • Suy clock từ tên tín hiệu, bỏ qua scope và context của property.
  • Thấy zero failure rồi bỏ qua việc guard hoặc disable đã chặn mọi lần kiểm hữu ích.

Khi gặp kết quả khó hiểu, vẽ lại ba mốc: lấy mẫu, cập nhật dữ liệu, đánh giá property. Gắn từng giá trị trong log vào đúng mốc ấy.

Tự giải thích rồi thử thay đổi

  1. Nếu property đòi q == 1 thay cho q == 0, tại sao log trực tiếp bằng 1 vẫn không cứu được property?
  2. Nếu bỏ clock viết trong property, cần tìm khai báo nào trong scope?
  3. Nếu cả property đúng lẫn property sai cố ý đều không báo lỗi, nên kiểm điều gì trước?

Tự kiểm tra: sampling

  1. Ở cạnh đầu của ví dụ, property q==0 dùng mẫu q bằng bao nhiêu?
  2. Mỗi property sai cố ý đòi mẫu q bằng 1 phải báo bao nhiêu vi phạm?
  3. Property không viết lại event trong ví dụ lấy clock ở đâu?
  4. Tại 6 ns, giá trị đọc trực tiếp của q và seen bằng bao nhiêu?
  5. Vì sao ví dụ giữ một property sai có chủ đích bên cạnh các property đúng?

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

Ví dụ giữ hai context clock: explicit và default. Mỗi context có một property dùng mẫu 0 và một property sai cố ý đòi mẫu 1. Bộ tự kiểm yêu cầu từng counter khớp; tắt assertion làm bài kiểm thất bại.

SVA sampling: property thấy mẫu trước cạnh, log có thể thấy giá trị mới

Expected tính trước chạy: SVA SAMPLE CHECK first_pre_q=0 raw_q=1 explicit_bad=1 default_bad=1 valid_failures=0 seen=1 time_ns=6

tb.sv testbench
`timescale 1ns/1ps// First posedge: qbefore0, blocking DUTsets1 inActive. Concurrent must sample0; rawq at6ns is1.module tb_sva_sampling; bit clk=0,q=0; int seen=0,sampled_failures=0,post_value_failures=0,default_failures=0,default_post_failures=0; default clocking cb @(posedge clk);endclocking always #5 clk=~clk; always @(posedge clk)begin q=1;seen<=seen+1;end A_pre:assert property(@(posedge clk)(seen==0)|->(q==0))else sampled_failures++; A_wrong:assert property(@(posedge clk)(seen==0)|->(q==1))else post_value_failures++; D_pre:assert property((seen==0)|->(q==0))else default_failures++; D_wrong:assert property((seen==0)|->(q==1))else default_post_failures++; initial begin  @(posedge clk);#1;  if(q!=1||seen!=1||sampled_failures!=0||post_value_failures!=1||default_failures!=0||default_post_failures!=1||$time!=6)$fatal(1,"SVA preponed versus raw oracle");  $display("SVA SAMPLE CHECK first_pre_q=0 raw_q=1 explicit_bad=1 default_bad=1 valid_failures=0 seen=1 time_ns=6");$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: SVA SAMPLE CHECK first_pre_q=0 raw_q=1 explicit_bad=1 default_bad=1 valid_failures=0 seen=1 time_ns=6

Một cạnh,2 state; explicitposedge vàdefaultclocking cùngclk. Không claim multiclock/XZ hoặc mọi SVA sampled function.

Hai wrongproperties phải fail 1; disabled-assertion probe riêng bảo vệ zero-failure falsepositive.

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.

Nguồn đã được parse và mô phỏng với Verilator 5.050, mô hình 2-state. Tại 6 ns, bộ kiểm yêu cầu giá trị trực tiếp của q và seen bằng 1, hai property đúng không có vi phạm và mỗi property sai cố ý có một vi phạm. Biến thể đổi yêu cầu mẫu 0 sang mẫu 1 cũng bị phát hiện.

Bằng chứng này không bao phủ X/Z, nhiều clock hoặc mọi vùng xử lý của SystemVerilog. Hình và bảng phía trên là minh họa, không mang nhãn waveform VCD.

[4]

Bài liên quan

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

  1. IEEE 1800-2023 SystemVerilog LRM, Immediate/concurrent assertions, clocks, sampling and sequences — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. SystemVerilog Concurrent Assertions — bản chụp resources.zip, SystemVerilog Concurrent Assertions. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. SystemVerilog Clocking Blocks Part 1 — bản chụp resources.zip, Basic Syntax; Declaring a Clocking Block Inside an Interface. Trích dẫn; nguồn đã đọc các mục liên quan.
  4. Thí nghiệm nguyên bản B8.sampling, Source, explicit/default-clock checks và disabled-assertion probe. Trích dẫn; nguồn đã đọc toàn văn.