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 operators: cùng start, cùng endpoint hay giữ điều kiện suốt sequence?

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

  • Chọn connective từ quan hệ giữa start, endpoint và span của các sequence
  • Phân biệt property negation với bitwise negation và điều kiện Boolean hiện tại
  • Phân biệt quan hệ thời gian cần kiểm với phạm vi hỗ trợ của công cụ

Đúng các giá trị nhưng sai quan hệ thời gian vẫn là lỗi

Hai nhánh đều xảy ra chưa có nghĩa chúng kết thúc cùng tick. Một điều kiện đúng ở đầu sequence cũng chưa có nghĩa nó giữ đúng suốt sequence.

Hãy vẽ điểm bắt đầu, endpoint và span của từng nhánh trước khi chọn operator. Ba thông tin này giúp phân biệt yêu cầu “cả hai”, “ít nhất một”, “cùng kết thúc” và “giữ suốt khoảng”.

And cần hai match còn intersect cần cùng endpoint

Xét hai sequence cùng bắt đầu tại một tick: a ##1 b và c ##2 d. and cần cả hai match, cho phép endpoint khác nhau và kéo span tới endpoint muộn hơn. intersect còn yêu cầu hai endpoint trùng nhau.

Start Nhánh a/b Nhánh c/d and intersect
1 Match tới tick 2 Match tới tick 3 Đáp ứng Không cùng endpoint
5 Match tới tick 6 Không match tại tick 7 Thiếu một nhánh Không có cặp match hợp lệ

Vì vậy đổi and thành intersect làm yêu cầu chặt thêm. Đổi and thành or lại bỏ yêu cầu cả hai nhánh phải match.

Or có thể thành công khi một nhánh không match

or cho phép match từ một trong hai nhánh. Với (a ##1 b) or (c ##2 e), nhánh a/b có thể đáp ứng dù nhánh c/e không match.

Đừng suy ra mọi sequence or chỉ có một endpoint hoặc luôn chọn endpoint sớm nhất. Nếu các nhánh có nhiều match rồi được nối thêm phần temporal, cần theo dõi những match liên quan. “Ít nhất một nhánh” không thay thế việc tính endpoint.

Throughout kiểm Boolean trên toàn span

hold_ok throughout (a ##1 b ##1 d) yêu cầu hold_ok đúng trên toàn span của match bên phải.

Tick 1 2 3
Sequence bên phải cần a b d
hold_ok trong ví dụ 1 0 1

Dù a, b, d đều xuất hiện đúng tick, hold_ok bằng 0 ở giữa làm yêu cầu không thỏa. Chỉ kiểm hold_ok tại tick đầu sẽ bỏ lọt trường hợp này.

Toán hạng bên trái là biểu thức Boolean. Không thay nó bằng một sequence nhiều tick rồi coi như vẫn cùng ý nghĩa.

Within: một match nằm trong span của match khác

within diễn tả một match nằm trong span của match khác. Hãy đánh dấu cả hai biên.

Match Bắt đầu Kết thúc
busy[*4] Tick 1 Tick 4
inner_req ##1 inner_ack Tick 2 Tick 3

Span 2–3 nằm trong span 1–4 theo mô hình containment này. Bảng là minh họa để suy luận; nó không phải waveform trích từ mô phỏng. Phạm vi hỗ trợ của ví dụ chạy nằm ở cuối bài.

First match: chọn endpoint sớm

Giả sử a ở tick 1, ready ở tick 2 và 3, còn end_ok chỉ ở tick 4. a ##[1:2] ready có thể kết thúc ở tick 2 hoặc 3.

Endpoint được chọn ##1 end_ok kiểm tại end_ok
Tick 2 Tick 3 0
Tick 3 Tick 4 1

first_match dùng để chọn match sớm. Trong mô hình này, chọn endpoint 2 dẫn tới kiểm end_ok tại 3 và không thỏa; giữ khả năng dùng endpoint 3 lại cho một đường đáp ứng.

Ví dụ giúp phân biệt việc có nhiều endpoint với việc cam kết một endpoint sớm. Nó còn chờ đối chiếu chuẩn và chưa được công cụ hiện tại xác nhận đầy đủ.

Not của property không phải phép đảo từng bit

not phủ định một property; ~ đảo từng bit của biểu thức integral. Hai toán tử thuộc hai tầng ý nghĩa khác nhau.

Trong trường hợp Boolean một tick, not (start && a) không thỏa tại tick mà cả start và a đều đúng. Ở các tick khác, biểu thức bên trong false nên property phủ định true.

Không mở rộng kết quả một tick thành quy tắc đơn giản cho mọi property nhiều tick. Còn phải xét thời điểm kết luận, pending và strong/weak.

Chọn operator từ quan hệ thời gian

  • Dùng and khi yêu cầu thật sự cần cùng endpoint.
  • Chỉ kiểm điều kiện ở đầu span thay cho throughout.
  • Gộp mọi endpoint của or thành một endpoint tùy chọn.
  • Đổi property not thành phép đảo bit.

Tự vẽ lại điểm bắt đầu, các endpoint và phần nối tiếp. Nếu chỉ đổi từ khóa cho tới khi hết lỗi, ta có thể đã đổi chính yêu cầu thiết kế.

Vẽ endpoint rồi thử thay đổi

  1. Nếu hai nhánh cùng kết thúc ở tick 3, and và intersect còn khác kết luận trong trường hợp ấy không?
  2. Nếu hold_ok chỉ sai ở tick cuối của span, cần kiểm lại yêu cầu nào?
  3. Trong bảng first_match, bỏ ready tại tick 2 sẽ đổi tập endpoint thế nào?

Quan hệ giữa các match

  1. Tại start ở tick 1, hai operand cùng bắt đầu nhưng match tại tick 2 và 3. And và intersect kết luận thế nào?
  2. Nhánh c/e của property or không match ở cả hai start trong ví dụ. Vì sao property vẫn được đáp ứng?
  3. Ở span đầu, a/b/d đúng tại tick 1/2/3 nhưng hold_ok false tại tick 2. Có thể chỉ kiểm hold_ok ở tick 1 để thay throughout không?
  4. start và a cùng true tại tick 1 và 5, false ở các tick còn lại trong 8 tick. Property not(start&&a) có bao nhiêu failure?
  5. Các ví dụ and/or đã chạy đúng, nhưng trường hợp first_match với range chưa khớp dự đoán. Có thể kết luận first_match đã được xác minh đầy đủ không?

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

Expected tính trước chạy: SVA OPERATOR CHECK samples=8 starts=2 and_failures=1 or_failures=0 intersect_failures=2 throughout_failures=2 not_failures=2 time_ns=80. Clock dùng default clocking cb ở posedge; stimulus chuẩn bị ở negedge, deadline cuối đã qua trước khi dừng.

SVA operators

Expected tính trước chạy: SVA OPERATOR CHECK samples=8 starts=2 and_failures=1 or_failures=0 intersect_failures=2 throughout_failures=2 not_failures=2 time_ns=80

tb.sv testbench
`timescale 1ns/1ps// Expected before execution: a/c and start at1/5,b at2/6,d at3 only,e at4,hold_ok false at2.// and1/or0/intersect2/throughout2/not2 failures, eight samples, two starts, end80ns.module tb_sva_operators;  bit clk=0,start=0,a=0,b=0,c=0,d=0,e=0,hold_ok=0;  int samples=0,starts=0,and_fail=0,or_fail=0,intersect_fail=0,throughout_fail=0,not_fail=0;  always #5 clk=~clk;  always @(posedge clk)begin samples++;if(start)starts++;end  default clocking cb @(posedge clk);endclocking  A_and:assert property(start |-> ((a ##1 b) and (c ##2 d)))else and_fail++;  A_or:assert property(start |-> ((a ##1 b) or (c ##2 e)))else or_fail++;  A_intersect:assert property(start |-> ((a ##1 b) intersect (c ##2 d)))else intersect_fail++;  A_throughout:assert property(start |-> (hold_ok throughout (a ##1 b ##1 d)))else throughout_fail++;  A_not:assert property(not (start && a))else not_fail++;  initial begin    for(int cycle=1;cycle<=8;cycle++)begin      if(cycle>1)@(negedge clk);      start=cycle==1||cycle==5;a=start;b=cycle==2||cycle==6;c=start;d=cycle==3;e=cycle==4;hold_ok=cycle!=2;    end    @(negedge clk);    if($time!=80||samples!=8||starts!=2||and_fail!=1||or_fail!=0||intersect_fail!=2||throughout_fail!=2||not_fail!=2)      $fatal(1,"SVA operator distinction oracle");    $display("SVA OPERATOR CHECK samples=8 starts=2 and_failures=1 or_failures=0 intersect_failures=2 throughout_failures=2 not_failures=2 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 OPERATOR CHECK samples=8 starts=2 and_failures=1 or_failures=0 intersect_failures=2 throughout_failures=2 not_failures=2 time_ns=80

Verilator 2 state, finite main subset:sequence and/or/intersect/throughout and Boolean property not. Not a proof for all sequence/property operators.

Within buildunsupported; or-continuation and first_match-range runtime oracles remain unmet, retained separately. No simulated-PASS claim for those probes.

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.

Sáu mutant giữ oracle để bắt and→or, and→intersect, or→and, intersect→and, bỏ điều kiện giữ span và bỏ not. Chúng phải parse/build qua rồi bị bắt tại runtime. Các failure counter khác 0 có chủ đích cũng giúp phát hiện checker bị tắt.

Ba probe chưa đạt gồm within build unsupported, or-continuation runtime chưa khớp expected và first_match-range runtime chưa khớp expected. Exit 0 của runner phân loại không biến ba construct ấy thành main PASS. Bằng chứng main chỉ thuộc source/trace năm construct đã thực sự chạy.

Giữ ba trường hợp chưa đạt: within có range được pyslang chấp nhận nhưng Verilator báo Unsupported: within with ranged cycle-delay operand; or nối temporal còn lệch yêu cầu; first_match với range cần any_failures=0, first_failures=1, first_mask=8 nhưng quan sát any=0, first=0, mask=0. Không đổi các kỳ vọng này để gắn nhãn supported. Những nguồn training có cách mô tả or/endpoint không nhất quán được giữ để đối chiếu, không dùng thay LRM. Sáu mutant của năm construct trong ví dụ chạy đều bị bắt ở runtime. Những counter vi phạm khác 0 có chủ đích giúp phát hiện checker bị tắt.

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

Bài liên quan

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

  1. IEEE 1800-2023 SystemVerilog LRM, Sequence combination, first_match and property negation — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. or operator (Disjunction) — bản chụp resources.zip, or operator (Disjunction); Example for OR of two sequences; Example for OR of two sequences including a time range. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. SystemVerilog Assertions Combining Sequences — bản chụp resources.zip, and: Both Must Match, Different Lengths Allowed; intersect: Both Must Match, and End at the Same Time; or: Matches as Soon as Either One Does; within: One Sequence Fully Contained in Another; throughout: A Boolean That Must Hold for the Whole Span. Trích dẫn; nguồn đã đọc các mục liên quan.
  4. within Operator — bản chụp resources.zip, within Operator; within operator example; not Operator in an assertion; not operator example. Trích dẫn; nguồn đã đọc các mục liên quan.
  5. first\_match Operator — bản chụp resources.zip, first_match Operator; first_match operator example. Trích dẫn; nguồn đã đọc các mục liên quan.
  6. Thí nghiệm nguyên bản B8.operators, Two-start operator distinctions, six runtime mutants and three retained capability failures. Trích dẫn; nguồn đã đọc toàn văn.
  7. IEEE 1800-2023 SystemVerilog LRM, Sequence operators and assertion local variables — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).