Bài viết này trình bày tổng quan về SVA (System Verilog Assertion), phân loại SVA và sự khác nhau giữa các loại SVA.
1) Các loại phát biểu assertion
Một assertion mô tả một hành vi hệ thống. Mục đích chính của assertion là xác thực tính hợp lệ của hành vi của một thiết kế, nghĩa là trả lời câu hỏi “thiết kế có làm việc chính xác hay không?”. Assertion còn được dùng để cung cấp thông tin về coverage chức năng, nghĩa là trả lời câu hỏi “các test có tốt hay không?”.
Assertion có thể được kiểm tra động (dynamic) bằng mô phỏng hoặc kiểm tra tĩnh (static) bằng phần mềm kiểm tra thuộc tính, ví dụ như phần mềm kiểm tra forrmal xác minh thiết kế có đáp ứng theo đúng spec hay không. Các phần mềm này yêu cầu các mô tả về thuộc tính, hành vi thiết kế để làm cơ sở so sánh với thiết kế thực.
Để mô tả một assertion chúng ta có thể sử dụng một trong các phát biểu assertion sau đây:
- assert dùng đểđặc tả thuộc tính bắt buộc của thiết kế sẽ được kiểm tra để xác minh thuộc tính đó có được giữ hay không.
- assume dùng để đặc tả thuộc tính giả định của môi trường. Trình mô phỏng sẽ kiểm tra thuộc tính này được giữ hay không còn phần mềm formal sẽ sử dụng thông tin này để tạo các kích thích đầu vào.
- cover dùng để giám sát sự ước lượng thuộc tính cho việc coverage.
- restrict dùng để đặc tả thuộc tính ràng buộc sự tính toán kiểm tra forrmal. Trình mô phỏng không kiểm tra thuộc tính này.
Như vậy, các phát biểu sử dụng một trong bốn từ khóa trên gọi là một assertion.
Ví dụ 1:
module event_sim;
//
//Design example
//
reg in_a, in_b;
reg in_c;
wire f;
assign f = in_a & in_b | in_c;
//
//Create input stimulus
//
initial begin in_a = 0;
in_b = 0;
in_c = 0;
#2
in_a = 1;
#2
in_b = 1;
end
reg clk = 0;
always #1 clk = !clk;
//
//Assertions
//
always @ (posedge clk) begin assert_f: assert (f)
$info("assert: PASSED");
else $error("assert: FAIL");
assume_inputs: assume (in_a || in_b)
$info("assumption holds");
else $error("assumption does not hold");
cover_a_and_b: cover (in_a && in_b)
$info("in_a=1 and in_b=1 are covered");
end
endmodule
Ví dụ 1 mô tả 3 assertion được kiểm tra tại mỗi cạnh lên của clock clk. Khi thực hiện mô phỏng động bằng trình mô phỏng (simulator):
- assert_f sẽ được kiểm tra điều kiện f=1, nếu đúng sẽ báo “assert: PASSED”, nếu sai sẽ báo lỗi “assert: FAIL”. $info và $error là các task hệ thống được hỗ trợ bởi System Verilog để in thông tin cảnh báo theo cấp độ.
- assume_inputs được kiểm tra điều kiện “in_a || in_b” và cảnh báo “assumption holds” nếu in_a hoặc in_b luôn bằng 1. Nguộc lại, nếu in_a=in_b=0 thì trình mô phỏng sẽ báo lỗi “assumption does not hold”
- cover_a_and_b được sử dụng để giám sát trường hợp in_a=in_b=1 có xảy ra hay không. Nếu có xảy ra, ta nói trường hợp này được bao phủ (đã cover) và thông tin “in_a=1 and in_b=1 are covered” được trình mô phỏng in ra. Nếu không thì sẽ không có thông báo nào được in ra.
Khi thực hiện mô phỏng tĩnh bằng phần mềm kiểm tra formal, ví dụ như Incisive Formal Verifier (IFV) của Cadence, assert_f sẽ được kiểm tra điều kiện f=1 với ràng buộc giả định được mô tả trong assume_inputs, in_a và in_b không bao giờ cùng bằng 0. Phần mềm kiểm tra formal sử dụng giả định assume_inputs để tạo ra tất cả các tổ hợp giá trị cho in_a và in_b để kiểm tra assert_f nhưng sẽ không tạo ra tổ hợp in_a=in_b=0. cover_a_and_b dùng để phát hiện đã có trường hợp in_a=in_b=1 hay chưa. Khi sử dụng phần mềm kiểm tra formal, chúng ta không cần đoạn code initial để tạo các kích thích đầu vào cho in_a, in_b và in_c vì chúng sẽ được tạo tự động bởi phần mềm kiểm tra formal.
2) Kết quả chạy mô phỏng động với QuestaSim
Sau khi biên dịch và chạy mô phỏng với QuestaSim trong 6ns, chúng ta có thể quan sát được các kết quả như sau:
- Waveform
- Report trên Transcript (command line của QuestaSim)
- Assertion report
- Coverage assertion report
 |
| Hình 1: Waveform của ví dụ 1 trong 6ns |
Vì các assertion được kiểm tra và giám sát tại các cạnh lên xung clock clk nên chúng ta sẽ chỉ phân tích kết quả tại các thời gian 1ns, 3ns và 5ns.
- Tại 1ns, in_a=in_b=0, assert_f và assume_inputs đều fail
- Tại 3ns, ina=1 và in_b=0, assert_f bị fail nhưng assume_inputs là pass
- Tại 5ns, in_a=in_b=1, assert_f và assume_inputs đều pass và trường hợp được giám sát bởi cover_a_and_b được bao phủ.
Các kết quả trên sẽ thể hiện trên command line hoặc terminal khi chạy mô phỏng.
 |
| Hình 2: Báo cáo (report) của các assertion |
Chúng ta cũng có thể xem các báo cáo về assertion và coverage của assertion trên trình mô phỏng. Đối với Questa Sim, chúng ta có thể xem ở View/Coverage/Assertions và View/Coverage/Cover Directives.
 |
| Hình 3: Xem các báo cáo về assertion trên Questa Sim |
So sánh với các cảnh báo trên cửa sổ transcript, chúng ta thấy số lần fail của assert_f là 2, của assume_inputs là 1 và trường hợp được giám sát bởi cover_a_and_b đã bao phủ 100%. Bên cạnh đó, chúng ta cũng có thể xuất ra file báo cáo các kết quả của assertion và assertion coverage bằng cách bấm chuột phải vào cửa sổ Assertions hoặc “Cover Directives” chọn report.
 |
| Hình 4: Xuất file báo cáo về assertion |
2) Phân loại assertion
Assertion được chia làm 2 loại chính là assertion trực tiếp (immediate assertion) và assertion đồng thời (concurrent assertion).
Assertion trực tiếp đi theo ngữ cảnh của sự kiện mô phỏng. Assertion trực tiếp là các phát biểu thủ tục được sử dụng cho mô phỏng. Phát biểu restrict không được sử dụng cho assertion trực tiếp. Trong đó assertion trực tiếp được chia thành các loại sau:
- Assertion trực tiếp đơn giản (simple immediate assertion) chỉ dùng các từ khóa assert, assume và cover để mô tả một assertion. Assertion này báo cáo trực tiếp khi có bất cứ thay đổi nào của biểu thức mà nó mô tả.
- Assertion trực tiếp bị trì hoãn (deferred immediate assertion) cũng được mô tả bằng các từ khóa assert, assume và cover nhưng thêm mô tả về sự “trì hoãn” là #0 hoặc final với mục đích ngăn chặn các báo cáo sai của assertion trực tiếp khi xuất hiện các glitch.
- Assertion trực tiếp bị trì hoãn dùng để giám sát (deferred immediate assertion assertion) là loại sử dụng #0, nó sẽ báo cáo kết quả “trễ” hơn chứ không báo cáo trực tiếp, trễ hơn ở đây không có nghĩa là là một khoảng thời gian trễ đo đếm cụ thể mà được hiểu là báo cáo khi giá trị ước lượng đã ổn định, tránh báo cáo sai khi xuất hiện glitch. Điều này có được vì việc thực thi báo cáo của assertion được thực thi trong vùng Reactive.
- Assertion trực tiếp bị trì hoãn final (final deferred immediate assertion) là loại chỉ báo cáo một lần tại vùng Postponed nên cũng giúp tránh được việc báo cáo sai do glitch xuấy hiện.
Assertion đồng thời dựa trên ngữ cảnh của clock và dùng các giá trị được lấy mẫu từ các biểu thức mà nó mô tả. Assertion đồng thời mô tả hành vi kéo dài theo thời gian. Không như assertion trực tiếp, mô hình ước lượng của assertion đồng thời dựa trên một clock. Nghĩa là assertion đồng thời chỉ được đánh giá khi xảy ra một clock tick. clock tick ở đây có thể hiểu là cạnh lên hoặc cạnh xuống của sự kiện clock được định nghĩa bởi người sử dụng. Assertion đồng thời sử dụng bốn phát biểu assert, assume, cover và restrict kết hợp với hai từ khóa property và sequence để mô tả.
 |
| Hình 5: Phân loại assertion trong SVA |
