[System Verilog] Kiểm tra formal - phần 2: Tổng quan về mô tả thuộc tính

Bài này trình bày tại sao cần phải có ngôn ngữ đặc tả formal, một số khái niệm, thuật ngữ liên quan đến ngôn ngữ mô tả formal SVA và một số ví dụ cơ bản để hiểu tổng quan về mô tả thuộc tính với SVA.

1) Tại sao cần có ngôn ngữ đặc tả formal

Ngôn ngữ đặc tả formal được sử dụng để mô tả thuộc tính thiết kế một cách chính xác và rõ ràng. Thông thường, các thuộc tính được mô tả trong một phần của spec thiết kế trong các văn bản như một file word, excel,... nhưng việc mô tả thuộc tính bằng ngôn ngữ tự nhiên là không rõ ràng vì không có quy định chung, không thống nhất và có thể hiểu theo nhiều cách khác nhau bởi nhiều người khác nhau. Bên cạnh đó, khi các kỹ sư thuộc các quốc gia khác nhau cùng làm việc với nhau, việc mô tả thuộc tính bằng ngôn ngữ tự nhiên, ví dụ như tiếng Anh, không đảm bảo tất cả các kỹ sư đều hiểu đúng một ý tưởng.

Ví dụ, giao thức request-grant thường được sử dụng như một cặp giao tiếp bắt tay. Khi một yêu cầu được phát ra trên tín hiệu request nó sẽ đợi được chấp nhận bởi tín hiệu grant.

Hình 1: Minh họa một giao thức bắt tay request-grant

Chúng ta xét một câu mô tả thuộc tính tiêu biểu như sau "mỗi request phải được chấp nhận trong 4 chu kỳ xung clock" (nguyên văn câu tiếng Anh "Each request should be granted in four clock cycles"). Mô tả này là không rõ ràng vì:

• Bốn chu kỳ này bắt đầu được tính từ lúc nào? ngay từ khi request được phát hay từ chu kỳ kế tiếp sau khi request đã phát?

Hình 2: Thời điểm xác định grant là lúc nào?

• Việc chấp nhận một request sẽ được phát trong suốt 4 chu kỳ hay trong chu kỳ thứ 4?

Hình 2: grant sẽ kéo dài suốt 4 chu kỳ hay chỉ trong chu kỳ thứ 4?

• Nếu hai yêu cầu cùng xuất hiện, chúng sẽ được chấp nhận bởi cùng 1 grant hay hai grant khác nhau?

Hình 3: một grant sẽ xác nhận cho bao nhiêu request?

Nếu thuộc tính trên được mô tả bằng một ngôn ngữ mô tả formal, ví dụ như SVA, thì chỉ có một cách hiểu duy nhất và rõ ràng.

Ví dụ 1:

assert property( @( posedge clk ) request |-> ##4 grant ); 

Đây là một assertion đồng thời (concurrent assertion) được định nghĩa theo clock clk và thuộc tính sẽ được kiểm tra theo các sự kiện cạnh lên của clk. Nếu request=1 thì tại chu kỳ thứ 4 grant phải bằng "1". Sau đó, grant kéo dài bao nhiêu chu kỳ nữa thì không nằm trong phạm vi mô tả của thuộc tính này. Xem hình minh họa dưới đây.

Hình 4: Minh họa thuộc tính mong muốn của mô tả assertion

Bên cạnh đó, ngôn ngữ mô tả thuộc tính như SVA không chỉ được dịch và hiểu bởi các phần mềm kiểm tra, mô phỏng mà còn giúp các kỹ sư khác nhau cùng hiểu đúng một thuộc tính vì nó đã được chuẩn hóa.

2) Các cấp độ của mô tả formal

Như đã trình bày ở bài 1, kiểm tra formal định hướng theo đầu ra, mỗi mô tả formal sẽ định nghĩa "cái gì sẽ xảy ra?" và "xảy ra lúc nào?" chứ không định nghĩa hành vi đó "xảy ra như thế nào?", đây gọi là mô tả mức trừu tượng (abstract description). Xét lại ví dụ 1, assertion này không định nghĩ làm thế nào request=1 và làm thế nào grant=1 mà chỉ định nghĩa "tại cạnh lên clock clk, khi request=1 thì grant phải bằng 1 tại chu kỳ thứ 4 tính từ lúc bắt đầu phát hiện request=1".

Các mô tả trừu tượng sẽ được tập hợp thành các thuộc tính. Một nhóm các thuộc tính có thể là một mô hình hoàn chỉnh.

Hình 5: Các cấp độ mô tả formal

Trong SVA, các biểu thức logic cơ bản được tạo từ các toán tử boolean (&&, ||, !). Các biểu thức này kết nối với nhau theo thứ tự thời gian bằng các toán tử chuỗi (sequence operator) sẽ tạo thành các chuỗi tuần tự (sequence). Ở đây, các biểu thức cơ bản và các sequence là các mô tả trừu tượng. Các biểu thức logic hoặc các sequence sẽ dùng để xây dựng nên các thuộc tính bằng các toán tử thuộc tính (property operator) và từ khóa property. Các biểu thức logic, sequence và  thuộc tính sẽ dùng để xây dựng lên các chỉ dẫn (directive) với từ khóa như assert, cover và chúng còn được gọi là các assertion.
Các assertion tạo ra các khối dùng để xác thực hành vi của thiết kế. Trong nhiều trường hợp, để mô hình hoàn chỉnh việc xác minh một chức năng, chúng ta cần đóng gói nhiều assertion thành một khối lớn hơn. Các khối này còn có thể chứa thêm các code khác tính toán các giá trị trung gian hoặc các biến phụ để sử dụng cho assertion hoặc tích hợp thêm các covergroup. System Verilog hỗ trợ từ khóa checker/endchecker để thực hiện điều này. Mỗi checker còn được gọi là một đơn vị assertion (assertion unit).

Hình 6: Các cấp mô tả trong SVA

Xét lại ví dụ 1, request và grant là các biểu thức logic cơ bản được hiểu tương ứng là request=1 và grant=1. Chuỗi " request |-> ##4 grant" là một thuộc tính được hiểu là grant=1 sau 4 chu kỳ delay tính từ lúc request=1.

Cụm "property( @( posedge clk ) request |-> ##4 grant )" tạo thành một thuộc tính hoàn chỉnh và một thuộc tính này tạo thành một asertion (hay một chỉ dẫn) với từ khóa assert.

Hình 7: Ví dụ về các lớp mô tả của SVA

Sau đây là ví dụ về một đơn vị assertion (một checker):
Ví dụ 2:

checker my_check (logic a, b);
a1: assert #0 ($onehot0({a, b});
c1: cover #0 (a == 0 && b == 0);
c2: cover #0 (a == 1);
c3: cover #0 (b == 1);
endchecker : my_check

Trong ví dụ 2, đơn vị assertion my_check sẽ kiểm tra các hành vi sau của hai đầu vào a và b:

• (a1) Kiểm tra tại một thời điểm chỉ có a =1 hoặc b = 1 hoặc a=b=0
• (c1) Báo cáo kết quả coverage trường hợp a=b=0
• (c2) Báo cáo kết quả coverage trường hợp a=1
• (c3) báo cáo kết quả coverage trường hợp b=1