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 sequence: đếm tick, cửa sổ match và repetition trước khi viết property

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

  • Tính endpoint của delay/repetition từ tick khởi đầu
  • Phân biệt sequence match với implication/vacuity
  • Không đếm attempt chưa kết luận thành thành công

Một match không phải một lệnh chờ procedural

“Ready xuất hiện sau start” chưa đủ rõ: sau đúng hai tick, hay trong một khoảng cho phép? Sequence giúp mô tả thứ tự các mẫu theo clock.

Hãy đánh số tick trước khi viết cú pháp. Một match là một lần các mẫu thỏa chuỗi điều kiện; nhiều lần bắt đầu có thể được theo dõi cùng lúc.

Delay ##n tính theo clock tick đã chọn

Với a ##2 b, nếu a đúng ở tick 1 thì b cần đúng ở tick 3. Khoảng cách là hai tick của clock đã chọn.

Tick 1 2 3
Điều kiện cần xét a Chờ một tick b

Nếu chu kỳ clock là 10 ns, hai tick cách nhau 20 ns. Đổi chu kỳ clock làm đổi thời gian ấy, còn yêu cầu hai tick vẫn giữ nguyên. ##2 không phải delay procedural #2.

Sequence cũng khác implication. a ##2 b mô tả một chuỗi match; start |-> ##2 ready chỉ tạo nghĩa vụ kiểm ready khi mẫu start đúng.

Một cửa sổ cho nhiều endpoint có thể hợp lệ

start |-> ##[1:2] ready cho phép ready xuất hiện sau start một hoặc hai tick. Chỉ cần một endpoint hợp lệ trong cửa sổ.

Tick có start Các tick có thể đáp ứng Ready trong ví dụ Kết luận
1 2 hoặc 3 3 Đáp ứng ở biên cuối
5 6 hoặc 7 Không có Vi phạm
9 10 hoặc 11 11 Đáp ứng ở biên cuối

Yêu cầu này không đòi ready giữ high ở mọi tick trong cửa sổ. Nếu đổi thành [1:1], hai lần ready ở biên sau hai tick không còn đáp ứng.

Repetition [*2] yêu cầu hai tick liên tiếp

ready[*2] yêu cầu ready đúng ở hai tick liên tiếp. Trong start |-> ##2 ready[*2], lần kiểm đầu ở sau start hai tick, lần tiếp ở tick kế đó.

Start Hai tick cần ready Ready thực tế Kết luận
1 3 và 4 Chỉ tick 3 Vi phạm
5 7 và 8 Không có Vi phạm
9 11 và 12 Cả hai tick Đáp ứng

Đây là lý do một xung ready có thể thỏa cửa sổ delay mà chưa thỏa yêu cầu giữ liên tiếp.

Ba start độc lập, không reset lịch sử của nhau

Mỗi start có mốc bắt đầu và hạn đáp ứng riêng. Ready ở tick 11 đáp ứng start tại tick 9; nó không sửa được nghĩa vụ từ tick 5 đã hết hạn ở tick 7.

Khi đọc một trace, ghi một dòng cho mỗi lần bắt đầu. Tránh dùng câu “đã thấy ready” để kết luận cho tất cả yêu cầu đang chờ.

Goto và non-consecutive đặt endpoint khác nhau

Goto [->n] gắn endpoint với lần điều kiện đúng thứ n. Non-consecutive [=n] có thể kéo endpoint qua các tick false sau đó. Phần nối tiếp vì thế có thể được xét ở những tick khác nhau.

Ví dụ a đúng ở tick 2 và 5, còn b đúng ở tick 7. Với goto hai lần rồi ##1 b, endpoint tại tick 5 dẫn tới việc kiểm b ở tick 6. Với non-consecutive, endpoint có thể kéo tới tick 6 rồi nối b ở tick 7.

Hãy tính cả endpoint và phần nối tiếp; chỉ đếm đủ hai lần a đúng chưa phân biệt được hai cách viết. Phạm vi công cụ đã kiểm và phần còn chờ đối chiếu chuẩn nằm ở cuối bài.

Kết thúc simulation không biến pending thành pass

Một yêu cầu không có hạn trên có thể còn chờ khi mô phỏng dừng. Chưa ghi nhận lỗi không có nghĩa hành vi mong đợi đã xảy ra.

Nếu mục tiêu là “ready phải xuất hiện”, hãy xác định thêm cách nhận biết hoàn tất và điều kiện kết thúc phép kiểm. Với yêu cầu hữu hạn, chạy qua deadline cuối để các nghĩa vụ có thể kết luận.

Bốn nhầm lẫn khi đọc sequence

  • Nhầm tick của assertion với nanosecond của procedural delay.
  • Biến cửa sổ cho phép một match thành yêu cầu giữ đúng ở mọi tick.
  • Dùng một ready muộn để giải thích cho yêu cầu đã hết hạn.
  • Tính attempt còn chờ như một lần đáp ứng thành công.

Trước khi đổi operator, hãy vẽ lại tick bắt đầu, các endpoint được phép và điều kiện cần giữ.

Tự tính endpoint rồi làm bài tập

  1. Nếu ready ở tick 3 đổi sang tick 2, cửa sổ [1:2] còn thỏa không?
  2. Nếu chỉ bỏ ready ở tick 12, yêu cầu nào của start tại tick 9 sẽ thay đổi?
  3. Nếu dừng mô phỏng trước deadline cuối, có thể kết luận gì từ việc chưa thấy lỗi?

Tự kiểm tra: sequences

  1. Theo hai bảng thời gian trong bài, yêu cầu cửa sổ và yêu cầu liên tiếp lần lượt có bao nhiêu vi phạm?
  2. Start ởtick 1 và delay 2 nhìn phần tiếp tại tick nào?
  3. Ready chỉ high ởtick 3, còn 4 bằng 0. Yêu cầu ready[*2] bắt đầu 3 có match không?
  4. Một attempt không có upperbound chưa kết luận lúc simulation dừng có tự được tính là pass thật không?
  5. Công cụ chưa biên dịch được ví dụ so sánh goto với non-consecutive. Có thể kết luận điều gì từ các ví dụ còn lại đã chạy?

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

Expected trước chạy: SVA SEQUENCE CHECK samples=14 starts=3 window_failures=1 consecutive_failures=2 time_ns=140. Main parse/simulate với Verilator, input chuẩn bị ởnegedge để ổn định ởposedge.

SVA sequence: đếm tick, cửa sổ match và repetition trước khi viết property

Expected tính trước chạy: SVA SEQUENCE CHECK samples=14 starts=3 window_failures=1 consecutive_failures=2 time_ns=140

tb.sv testbench
`timescale 1ns/1ps// Starts1/5/9; ready3/11/12. Window+1..2 fails only@5; +2then2consecutive fails@1/@5,passes@9.module tb_sva_sequences; bit clk=0,start=0,ready=0; int samples=0,starts=0,window_failures=0,consecutive_failures=0; always #5 clk=~clk; always @(posedge clk)begin samples++;if(start)starts++;end A_window:assert property(@(posedge clk)start|->##[1:2]ready)else window_failures++; A_repeat:assert property(@(posedge clk)start|->##2 ready[*2])else consecutive_failures++; initial begin  for(int cycle=1;cycle<=14;cycle++)begin   if(cycle>1)@(negedge clk);   start=(cycle==1||cycle==5||cycle==9);   ready=(cycle==3||cycle==11||cycle==12);  end  @(negedge clk);  if(samples!=14||starts!=3||window_failures!=1||consecutive_failures!=2||$time!=140)$fatal(1,"SVA sequence accounting oracle");  $display("SVA SEQUENCE CHECK samples=14 starts=3 window_failures=1 consecutive_failures=2 time_ns=140");$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 SEQUENCE CHECK samples=14 starts=3 window_failures=1 consecutive_failures=2 time_ns=140

Main explicitposedge,2 state, finite[1:2]/[*2] với 14 samples. Advanced[=2]comparison có buildfail riêng; không claim mọi sequence operator hoặc pending=pass.

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.

Hai mutant thu window hoặc giảm repetition bị accountingoracle bắt. Probe nâng cao không được nhập vào mainPASS bằng việc bỏ assertion hoặc đổi comparison theo diagnostic của tool.

Giới hạn: ví dụ chạy dùng cửa sổ và repetition hữu hạn. Thí nghiệm phân biệt goto với non-consecutive được pyslang chấp nhận, nhưng Verilator báo lỗi clocking/internalUnexpectedCall trong hai cấu hình đã thử. Không có bằng chứng mô phỏng đạt cho phép so sánh đó; không sửa kỳ vọng hay bỏ assertion để đổi nhãn kết quả.

[1] [2] [3] [4]

Bài liên quan

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

  1. SystemVerilog Assertions with time delay — bản chụp resources.zip, The ## Operator; Multiple Instances Run in Parallel. Trích dẫn; nguồn đã đọc các mục liên quan.
  2. SystemVerilog Sequence Repetition Operator — bản chụp resources.zip, Consecutive Repetition: [*n]; Range Repetition: [*n:m] and [*n:$]. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. SystemVerilog Sequence Repetition Operator — bản chụp resources.zip, Goto Repetition: [->n]; Non-Consecutive Repetition: [=n]; Comparing goto and non-consecutive on the Same Trace. Trích dẫn; nguồn đã đọc các mục liên quan.
  4. Thí nghiệm nguyên bản B8.sequences, Source, finite-window/repetition oracles và advanced-repeat probes. Trích dẫn; nguồn đã đọc toàn văn.
  5. 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ở).