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

Assertion: kiểm gì, kiểm lúc nào và thế nào mới là bằng chứng?

Khoảng 50 phútMức 1/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 immediate assertion khỏi một property có clock/sample
  • Đọc X/Z theo truth của expression, không theo sự có mặt của một ký tự
  • Phân biệt predicate, severity, cấu hình tool và phạm vi formal proof

Biến yêu cầu thiết kế thành câu hỏi có thể kiểm

“Khi có yêu cầu, bộ xử lý phải sẵn sàng” còn thiếu một chi tiết: sẵn sàng ngay bây giờ hay ở clock kế tiếp? Assertion giúp viết rõ cả điều kiện lẫn thời điểm cần kiểm.

Dùng immediate assertion khi cần kiểm tại một điểm trong luồng lệnh. Dùng concurrent assertion khi điều kiện gắn với clock hoặc trải qua nhiều tick. Hãy bắt đầu bằng một yêu cầu nhỏ, rồi đối chiếu từng mẫu tín hiệu.

Ví dụ nhỏ: kiểm một giá trị ngay lúc chạy

Giả sử flags rộng 2 bit và giá trị 00 không hợp lệ. Điều kiện flags != 0 cho bảng sau:

flags Điều kiện đúng? Ý nghĩa
00 Không Phải báo vi phạm
01 Có Hợp lệ
10 Có Hợp lệ
11 Có Hợp lệ

Immediate assertion đánh giá điều kiện khi luồng lệnh đi đến nó. Nếu thử cả bốn giá trị liên tiếp mà không có delay, cả bốn phép kiểm có thể xảy ra ở cùng một thời điểm mô phỏng. Assertion không tự tạo clock hay tự chờ dữ liệu ổn định.

[1]

X và Z được xét trong cả biểu thức

Một vector chứa X không tự động làm mọi điều kiện sai. Với assert(value), cần xét giá trị logic của cả vector. Chỉ một bit 1 đã biết cũng đủ xác định điều kiện là true.

value Điều kiện là true? Lý do
00 Không Không có bit 1
01 Có Có bit 1 đã biết
0x, 0z Không Chưa xác định được bit 1
1x Có Bit cao đã là 1
x0, xz, zz Không Không có bit 1 đã biết

Muốn cấm mọi unknown bit, hãy viết yêu cầu riêng bằng predicate phù hợp, chẳng hạn $isunknown. Đó là yêu cầu khác với “vector này có giá trị logic true”.

Ví dụ có clock: start và ready ở cùng tick

Xét property @(posedge clk) start |-> ready. Ở mỗi cạnh lên, nếu mẫu start bằng 1 thì mẫu ready tại chính tick ấy phải bằng 1.

Tick start ready Kết luận
1 0 0 Không phát sinh yêu cầu ready
2 1 0 Vi phạm
3 1 1 Đáp ứng yêu cầu
4 0 0 Không phát sinh yêu cầu ready

Bảng chỉ có một vi phạm, tại tick 2. Đừng xem hai tick start = 0 là hai lần xử lý yêu cầu thành công: ở đó chưa có yêu cầu nào để kiểm ready.

Chọn hành động khi điều kiện sai

Điều kiện và cách xử lý vi phạm là hai quyết định riêng. Action block có thể ghi thông tin, tăng bộ đếm hoặc dừng bằng $fatal, tùy mục tiêu testbench.

Đừng mặc định $error luôn dừng chương trình như $fatal. Hành vi quan sát được còn phụ thuộc simulator và cấu hình. Khi cần kết thúc bài kiểm, hãy chọn cách dừng rõ ràng và kiểm exit status.

[3]

Dùng assertion để mô tả bất biến tổ hợp

Với hai số unsigned rộng 2 bit, tổng giữ carry cần 3 bit. Hai điều kiện total >= a và total >= b là những bất biến đơn giản để phát hiện mất carry.

a b Tổng giữ carry Tổng bị cắt còn 2 bit
2 2 4 0

Formal có thể kiểm những điều kiện đã viết trên mô hình input được chọn. Hai bất biến này bắt được ví dụ mất carry trên, nhưng chưa mô tả mọi chức năng của một bộ cộng. Mô hình 2-state cũng chưa trả lời hành vi với X/Z.

Cùng số lỗi vẫn có thể sai thời điểm

Nếu đổi |-> thành |=> trong bảng bốn tick, yêu cầu ready chuyển sang tick kế tiếp. Lần bắt đầu ở tick 3 sẽ nhìn tick 4 và gặp vi phạm. Tổng số lỗi vẫn bằng một, nhưng thời điểm và nghĩa của property đã khác.

Khi debug, hãy ghi rõ tick bắt đầu, tick cần đáp ứng và tick vi phạm. Chỉ nhìn tổng số lỗi cuối bài có thể bỏ sót việc dùng nhầm toán tử thời gian.

Ba lỗi dễ gặp khi viết checker

  • Kiểm một giá trị mà chưa xác định thời điểm nó có ý nghĩa.
  • Đặt việc bắt buộc phải chạy, như randomize(), chỉ trong biểu thức assertion. Nên gọi trước, giữ kết quả rồi kiểm riêng để cấu hình tắt assertion không làm mất bước tạo stimulus.
  • Thấy không có lỗi rồi kết luận checker đang hoạt động. Hãy thêm một tình huống chắc chắn vi phạm để kiểm khả năng phát hiện lỗi.

Tình huống sai cố ý dùng để kiểm checker; nó không biến yêu cầu sai thành yêu cầu hợp lệ. Bản kiểm phải phát hiện cả việc bỏ lỡ vi phạm đã biết.

Thử suy luận trước khi chạy

Đọc lại bảng bốn tick và trả lời:

  1. Nếu ready ở tick 2 đổi thành 1, còn tick nào vi phạm property ban đầu?
  2. Nếu start luôn bằng 0, “không có lỗi” đã chứng minh bộ xử lý đáp ứng yêu cầu chưa?
  3. Vì sao 1x thỏa assert(value) nhưng vẫn không đáp ứng yêu cầu “không có unknown bit”?

Tự kiểm tra: why

  1. Với assert(value), vector nào sau đây làm điều kiện là true?
  2. Trong bảng bốn tick, property start |-> ready vi phạm ở tick nào?
  3. Hai bất biến total >= a và total >= b đã được chứng minh trong phạm vi nào?
  4. Quan sát Icarus và Verilator ở phần kiểm chứng cho thấy điều gì về $error?
  5. Với một lời gọi bắt buộc như randomize, cách tổ chức nào giữ intent rõ khi checker có thể bị tắt?

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

Hai ví dụ dưới giữ assertion sai có chủ đích và tự đối chiếu số lượng, vị trí vi phạm. Nếu tắt checker hoặc đổi loại implication, bộ kiểm phải từ chối kết quả. Không sửa kỳ vọng theo output mới để gọi là đạt.

Assertion: kiểm gì, kiểm lúc nào và thế nào mới là bằng chứng?

Expected tính trước chạy: ASSERTION WHY CHECK immediate_checks=4 immediate_failures=1 clock_samples=4 concurrent_failures=1 failure_mask=4 time_ns=40

tb.sv testbench
`timescale 1ns/1ps// Immediate checks at0ns:4cases,onefalse. Concurrent four ticks: start/ready00,10,11,00 ->onefailure.module tb_assertion_why; bit clk=0,start=0,ready=0; bit[1:0] flags; int immediate_checks=0,immediate_failures=0,concurrent_samples=0,concurrent_failures=0; int cycle_tag=1,failure_mask=0; always #5 clk=~clk; always @(posedge clk)concurrent_samples++; A_ready:assert property(@(posedge clk)start|->ready)else begin concurrent_failures++;failure_mask|=1<<cycle_tag;end initial begin  for(int k=0;k<4;k++)begin   flags=2'(k);assert(flags!=0)else immediate_failures++;immediate_checks++;  end  @(negedge clk);cycle_tag=2;start=1;  @(negedge clk);cycle_tag=3;ready=1;  @(negedge clk);cycle_tag=4;start=0;ready=0;  @(negedge clk);  if(immediate_checks!=4||immediate_failures!=1||concurrent_samples!=4||concurrent_failures!=1||failure_mask!=4||$time!=40)$fatal(1,"assertion modes accounting oracle");  $display("ASSERTION WHY CHECK immediate_checks=4 immediate_failures=1 clock_samples=4 concurrent_failures=1 failure_mask=4 time_ns=40");$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: ASSERTION WHY CHECK immediate_checks=4 immediate_failures=1 clock_samples=4 concurrent_failures=1 failure_mask=4 time_ns=40

Main counterexample/negativecases có failure dự kiến. WhyVerilator 2-state, X/Z dùng Icarus riêng; không claim formal bằng badgepipeline.

YosysSAT/severity/option là probe riêng; formal chỉ 2 invariant tổ hợp 2 state, không fulladdercorrectness/X/Z.

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.

Assertion: kiểm gì, kiểm lúc nào và thế nào mới là bằng chứng? — Icarus 4 state

Expected tính trước chạy: IMMEDIATE XZ CHECK cases=8 passed=2 failed=6 one_x_passes=1 time_ns=0

tb.sv testbench
`timescale 1ns/1ps// Cases00/01/0x/0z/1x/x0/xz/zz ->passes01/1x only,2pass6fail.module tb_immediate_xz; logic[1:0] value; bit actual,expected; int passed=0,failed=0; initial begin  for(int k=0;k<8;k++)begin   case(k)    0:value=2'b00;1:value=2'b01;2:value=2'b0x;3:value=2'b0z;    4:value=2'b1x;5:value=2'bx0;6:value=2'bxz;7:value=2'bzz;   endcase   expected=(k==1||k==4);   assert(value)begin actual=1;passed++;end else begin actual=0;failed++;end   if(actual!==expected)$fatal(1,"immediate four-state truth oracle");  end  if(passed!=2||failed!=6)$fatal(1,"immediate four-state accounting");  $display("IMMEDIATE XZ CHECK cases=8 passed=2 failed=6 one_x_passes=1 time_ns=0");$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 (Icarus Verilog 11.0, 4-state)

Output phải khớp: IMMEDIATE XZ CHECK cases=8 passed=2 failed=6 one_x_passes=1 time_ns=0

Main counterexample/negativecases có failure dự kiến. WhyVerilator 2-state, X/Z dùng Icarus riêng; không claim formal bằng badgepipeline.

YosysSAT/severity/option là probe riêng; formal chỉ 2 invariant tổ hợp 2 state, không fulladdercorrectness/X/Z.

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.

Verilator 5.050 chạy mô hình 2-state với bốn phép kiểm immediate và bốn mẫu clock. Icarus 11.0 chạy tám vector 4-state, gồm hai trường hợp true và sáu trường hợp còn lại. Các failure dự kiến là một phần của bài kiểm, không phải lỗi được bỏ qua.

Thí nghiệm riêng với Yosys 0.70 giữ hai assert cell và chứng minh hai bất biến tổ hợp trên 16 tổ hợp input 2-state. Biến thể cắt carry cho phản ví dụ a = 2, b = 2, total = 0 và làm lệnh chứng minh thất bại. Đây không phải chứng minh toàn bộ chức năng adder.

Trong thí nghiệm severity, Icarus tiếp tục sau $error, còn cấu hình Verilator đã chạy dừng tại đó. Kiểm thử tắt assertion bị từ chối. Những quan sát này gắn với công cụ và cấu hình đã ghi, không thay cho đối chiếu IEEE LRM.

[4] [5] [6]

Bài liên quan

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

  1. SystemVerilog Immediate Assertions — bản chụp resources.zip, SystemVerilog Immediate Assertions; Syntax; Common Beginner Mistakes. Trích dẫn; nguồn đã đọc các mục liên quan.
  2. 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ở).
  3. 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.
  4. Thí nghiệm nguyên bản B8.why, Source, failure mask và assertion-option/severity probes. Trích dẫn; nguồn đã đọc toàn văn.
  5. Thí nghiệm nguyên bản B8.immediate-xz, Bảng truth4-state và equality mutant. Trích dẫn; nguồn đã đọc toàn văn.
  6. Thí nghiệm nguyên bản B8.immediate-formal, Hai assert cell được giữ, SAT proof và carry counterexample. Trích dẫn; nguồn đã đọc toàn văn.