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

Sequence có tham số: tái sử dụng mẫu thời gian, hiểu endpoint và đệ quy

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ẽ

  • Dùng một sequence cho hai kênh tín hiệu khác nhau
  • Truy biểu thức actual tới đúng tick trong sequence
  • Phân biệt endpoint, lưu dữ liệu và bước đệ quy sang clock kế tiếp

Cùng một quy tắc, hai cặp tín hiệu

Kênh A yêu cầu ack sau đúng một tick. Kênh B cũng vậy. Viết hai bản sequence gần giống nhau khiến việc sửa delay dễ lệch giữa hai kênh.

Ta có thể đặt tên cho mẫu thời gian và truyền tín hiệu vào lúc dùng. Mẫu nói “req ở tick này, ack ở tick sau”; mỗi assertion quyết định nó áp dụng cho cặp tín hiệu nào.

Việc tái sử dụng chỉ có ích khi cả tín hiệu, clock và nghĩa vụ đều được nối đúng. Tên sequence giống nhau chưa bảo đảm hai assertion kiểm cùng hợp đồng.

Theo từng request tới tick cần ack

Xét hai kênh dùng cùng clock. Mỗi request trong bảng chỉ cao một tick. Ack được lấy mẫu ở tick kế tiếp.

Kênh Tick request Tick cần ack Ack tại tick đó Kết luận
A 1 2 1 Đáp ứng
A 4 5 0 Vi phạm
A 7 8 1 Đáp ứng
A 10 11 1 Đáp ứng
B 2 3 1 Đáp ứng
B 5 6 1 Đáp ứng
B 8 9 0 Vi phạm

Ack của B tại tick 6 không trả lời request A tại tick 4. Kênh, nội dung điều kiện và thời điểm đều thuộc hợp đồng cần kiểm.

Formal là tên trong mẫu, actual là biểu thức được nối

Đây là định nghĩa được dùng trong ví dụ:

sequence transfer(req,ack);req ##1 ack;endsequence

req và ack là formal argument: tên được dùng bên trong mẫu. Trong transfer(req_a,ack_a), actual argument là các biểu thức req_a và ack_a. Một lần dùng khác là transfer(req_b,ack_b).

Assertion A đặt mẫu sau implication:

req_a |-> transfer(req_a,ack_a) dùng clock @(posedge clk).

Khi req_a false, antecedent không tạo nghĩa vụ ack cho attempt đó. Khi req_a true, mẫu bắt đầu ngay tại tick request và yêu cầu ack_a ở tick kế tiếp. Formal req lặp lại điều kiện đầu của mẫu; nó không tự thay thế vai trò gating của implication.

Truy biểu thức tới đúng tick

Trong mẫu này, req được xét ở điểm bắt đầu; ack được xét sau ##1. Ở request A tại tick 1, ack_a đang bằng 0 nhưng tới tick 2 bằng 1, nên lần kiểm ấy vẫn được đáp ứng.

Truyền ack_a vào formal không có nghĩa chụp giá trị 0 tại tick 1 rồi giữ nó cho cả sequence. Đó là bài toán lưu dữ liệu khác; biến local và capture đã được học ở bài trước.

Clock trong ví dụ được ghi rõ tại assertion là @(posedge clk). ##1 là một tick của clock đó. Đổi chu kỳ clock không tự đổi quan hệ “tick kế tiếp” thành một delay cố định theo ns.

Nếu truyền ack_b vào assertion A, mẫu vẫn có cấu trúc hợp lệ nhưng quan sát nhầm kênh. Hãy lần đường actual → formal → tick sử dụng, thay vì chỉ kiểm tên khai báo.

Endpoint là lúc mẫu hoàn tất

Với req ##1 ack, nếu req tại tick 1 và ack tại tick 2 cùng đáp ứng, endpoint của match là tick 2. Chưa thấy ack ở tick 1 không có nghĩa mẫu đã thất bại: nó còn đang chờ tới tick cần kiểm.

Khi nối mẫu bằng implication |->, điều kiện phía sau bắt đầu tại endpoint của antecedent. Viết bảng start/endpoint trước sẽ giúp phân biệt cách nối mẫu với việc đọc một cờ “đã xong” lưu trong thanh ghi.

Sequence method như .triggered liên quan tới trạng thái match và clock context. Nguồn training cũng có tên .ended; cần đối chiếu đúng cú pháp/ngữ nghĩa của bản IEEE đang dùng trước khi thay tên method. Không coi một method là cờ done giữ nguyên tới khi reset.

Trong bộ ví dụ hiện tại, dạng .triggered mới được parser chấp nhận và chưa có mô phỏng thành công. Phạm vi này được ghi trong bằng chứng cuối bài.

Đệ quy cần một bước sang thời gian sau

Thay vì liệt kê mọi tick chờ, một property có thể tự gọi lại trên tick sau. Source minh họa dùng:

property recur(x); x or (1'b1 |=> recur(x));endproperty

Bảng minh họa nhánh dừng khi x cuối cùng true:

Tick đang xét x Cách lần theo biểu thức
1 0 Xét tiếp bước gọi ở tick 2
2 0 Xét tiếp bước gọi ở tick 3
3 1 Nhánh x đã đáp ứng tại tick này

Bước thời gian làm các lần tự gọi khác nhau. Nếu chỉ thay |=> bằng |->, lời gọi quay lại ngay ở cùng tick; không còn sự tiến triển thời gian đang mô tả.

Nếu simulation dừng khi vẫn chờ, chưa thể dùng bảng trên để kết luận pass. Quy tắc strong/weak, finite-end, polarity và reset wrapper của property đệ quy còn cần đối chiếu chuẩn. Source đệ quy ở bài mới có bằng chứng parser, chưa có bằng chứng chạy mô phỏng.

Bốn nhầm lẫn khi tái sử dụng sequence

  • Nối nhầm actual từ kênh khác dù tên formal vẫn đúng.
  • Coi argument là giá trị đã capture ở thời điểm bắt đầu.
  • Dùng ##0 hoặc ##2 khi yêu cầu là đúng tick kế tiếp.
  • Coi endpoint là trạng thái lưu vĩnh viễn, hoặc gọi đệ quy mà không tiến sang thời gian sau.

Tách ba câu hỏi khi đọc: mẫu nhận biểu thức nào, biểu thức được xét ở tick nào, và attempt nào tạo nghĩa vụ kiểm mẫu đó?

Đổi kênh, đổi delay và lần theo nghĩa vụ

  1. Với request A tại tick 4, có được dùng ack B tại tick 6 để gọi A đáp ứng không? Vì sao?
  2. Nếu đổi ##1 thành ##0, tại tick nào cần kiểm ack của request A tại tick 1?
  3. Nếu cần so dữ liệu ở deadline với dữ liệu lúc request, argument đơn thuần đã đủ giữ dữ liệu chưa?
  4. Trong bảng đệ quy, vì sao bước từ tick 2 sang tick 3 cần tiến triển thời gian?
  5. Parser chấp nhận một property đã đủ chứng minh hành vi khi chạy và lúc kết thúc simulation chưa?

Kiểm tra

Tái sử dụng mẫu thời gian đúng kênh

  1. Request A ở tick 1. Với transfer(req_a,ack_a) dùng delay một tick, ack_a phải đáp ứng ở tick nào?
  2. Assertion của B cần kiểm ack của chính B. Actual tương ứng với formal ack nên là biểu thức nào?
  3. Trong ví dụ formal không khai báo kiểu/hướng, ack_a bằng 0 lúc request và bằng 1 ở tick sau. Điều gì được kiểm ở cuối sequence?
  4. Trong recur(x) ở bài, vì sao bước tự gọi dùng |=> thay cho việc quay lại ngay cùng tick?
  5. Source dùng sequence method được parser chấp nhận nhưng simulator chưa build được. Có thể kết luận gì?

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

Expected tính trước chạy từ bảng: SVA ARG CHECK samples=12 starts_a=4 starts_b=3 failures_a=1 mask_a=32 failures_b=1 mask_b=512 time_ns=120. Hai vi phạm ở tick 5 và 9 tạo mask 32 và 512. Stimulus đổi ở cạnh xuống; chạy đủ 12 sample tới 120 ns, qua deadline cuối 11.

Sequence arguments on two independent request channels

Expected trước chạy: 12 tick, bốn request A và ba request B; thiếu ack tại tick 5 và 9. SVA ARG CHECK samples=12 starts_a=4 starts_b=3 failures_a=1 mask_a=32 failures_b=1 mask_b=512 time_ns=120

tb.sv testbench
`timescale 1ns/1psmodule tb_args;bit clk=0,req_a=0,ack_a=0,req_b=0,ack_b=0;int tick=0,starts_a=0,starts_b=0,failures_a=0,failures_b=0;int mask_a=0,mask_b=0;sequence transfer(req,ack);req ##1 ack;endsequencealways #5 clk=~clk;always @(posedge clk)begin tick++;if(req_a)starts_a++;if(req_b)starts_b++;endA:assert property(@(posedge clk)req_a |-> transfer(req_a,ack_a))else begin failures_a++;mask_a|=1<<tick;endB:assert property(@(posedge clk)req_b |-> transfer(req_b,ack_b))else begin failures_b++;mask_b|=1<<tick;endinitial begin for(int n=1;n<=12;n++)begin  if(n>1)@(negedge clk);  req_a=(n==1||n==4||n==7||n==10);ack_a=(n==2||n==8||n==11);  req_b=(n==2||n==5||n==8);ack_b=(n==3||n==6); end @(negedge clk); if(tick!=12||starts_a!=4||starts_b!=3||failures_a!=1||mask_a!=32||failures_b!=1||mask_b!=512||$time!=120)  $fatal(1,"sequence argument contract samples=%0d fa=%0d ma=%0d fb=%0d mb=%0d",tick,failures_a,mask_a,failures_b,mask_b); $display("SVA ARG CHECK samples=12 starts_a=4 starts_b=3 failures_a=1 mask_a=32 failures_b=1 mask_b=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: SVA ARG CHECK samples=12 starts_a=4 starts_b=3 failures_a=1 mask_a=32 failures_b=1 mask_b=512 time_ns=120

Explicit posedge, two-state bit inputs and one-cycle delay on two channels. No argument direction, local/output formal, type conversion or multiclock claim.

Triggered and recursive forms have separate parsed-only examples; ended member access is rejected by the pinned parser and retained separately.

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.

Guard kiểm tick/start count của hai kênh, số failure, mask và thời gian thật. Hai ack thiếu là lỗi cố ý: tắt assertion làm failure trở về 0 và oracle phải từ chối. Bốn mutant giữ nguyên kỳ vọng: nối nhầm ack, đổi delay thành 0, đổi thành 2, dùng gate của A cho B. Cả bốn parse/build được rồi bị bắt ở runtime.

Sequence triggered: parsed only

Source riêng cho sequence method được pyslang chấp nhận; chưa có executable mô phỏng thành công với Verilator đã ghim.

tb.sv testbench
`timescale 1ns/1psmodule tb;bit clk=0,r=1,a=0;int samples=0, failures=0;always #5 clk=~clk;always @(posedge clk) samples++;sequence pair;@(posedge clk)r ##1 a;endsequence A:assert property(@(posedge clk)pair.triggered |-> a)else failures++;initial begin @(negedge clk);r=0;a=1; @(negedge clk);a=0; #20; if(samples!=4||failures!=0||$time!=40)$fatal(1,"research contract"); $display("RESEARCH CHECK samples=4 failures=0 time_ns=40");$finish;endendmodule

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

  • Phân tích và elaborate theo LRM (pyslang 12.1.0)

Verilator 5.050 cannot resolve the sequence triggered member in this source. No runtime or endpoint-timing claim.

The four-tick counters and checks are retained in source; a parser result does not establish them.

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.

Recursive property: parsed only

Property tự gọi qua tick kế tiếp được pyslang chấp nhận; giữ source và phân biệt kết quả parser với mô phỏng.

tb.sv testbench
`timescale 1ns/1psmodule tb;bit clk=0,r=1,a=0;int samples=0, failures=0;always #5 clk=~clk;always @(posedge clk) samples++;property recur(x); x or (1'b1 |=> recur(x));endproperty A:assert property(@(posedge clk)r |-> recur(a))else failures++;initial begin @(negedge clk);r=0;a=1; @(negedge clk);a=0; #20; if(samples!=4||failures!=0||$time!=40)$fatal(1,"research contract"); $display("RESEARCH CHECK samples=4 failures=0 time_ns=40");$finish;endendmodule

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

  • Phân tích và elaborate theo LRM (pyslang 12.1.0)

Verilator 5.050 reports Unsupported Recursive property call. No finite-end, strength, runtime or assertion-control claim.

This positive recursive form has an explicit later-clock call. All recursion restrictions remain pending IEEE cross-check.

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.

Pyslang chấp nhận hai source trên; Verilator 5.050 không resolve được .triggered và báo unsupported recursive property call. Dạng .ended bị parser đã ghim từ chối với InvalidMemberAccess. Các probe được giữ riêng; không nâng giới hạn một công cụ thành quy tắc của IEEE, không đổi cú pháp/kỳ vọng để gọi đã simulated PASS.

Main chỉ chạy formal không khai báo kiểu/hướng, tín hiệu bit 2-state, một clock và delay một tick. Chưa kiểm local/output formal, conversion, multiclock, phương thức endpoint hay kết thúc property đệ quy. Bảng đệ quy là minh họa lập luận, không phải trace mô phỏng. Nguồn training có bảng bị hỏng và ví dụ chưa rõ clock/reset, nên không sao chép code/diagnostic của tutorial làm bằng chứng cho bài.

[2] [3] [4] [5]

Bài liên quan

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

  1. IEEE 1800-2023 SystemVerilog LRM, Sequence arguments, endpoint methods and recursive properties — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. Sequence in Assertions — formal arguments, What Is an SVA Sequence?; Where does the Clock Come From?; The sequence with a formal argument; Multiple sequences example; Common Mistakes. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. If expression and ended sequence — tài liệu training, ended in sequence; ended in sequence example; Points to Remember. Trích dẫn; nguồn đã đọc các mục liên quan.
  4. Recursive property — tài liệu training, What Makes a Property Recursive?; How the Recursive Property Works; Why a Time Delay Is Required; Restrictions on Recursive Properties; Legal reset wrapper. Trích dẫn; nguồn đã đọc các mục liên quan.
  5. Thí nghiệm nguyên bản B8.advanced, Two-channel sequence arguments, four runtime mutants and retained endpoint/recursion limitations. Trích dẫn; nguồn đã đọc toàn văn.
  6. IEEE 1800-2023 SystemVerilog LRM, Sequence formal arguments, actual expressions and sampling — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  7. IEEE 1800-2023 SystemVerilog LRM, Sequence endpoint methods 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ở).
  8. IEEE 1800-2023 SystemVerilog LRM, Recursive properties, time progress and restrictions — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).