Trung tâm đào tạo thiết kế vi mạch Semicon

Assertion được sử dụng để hỗ trợ trong quá trình kiểm tra thiết kế. Kiểm tra thiết kế dựa vào assertion (assertion-based verification) sử dụng hiệu quả trong quá trong quá trình kiểm tra thiết kế ở mức block và ở mức hệ thống (chip).

Thông qua phương thức này, các logic, tín hiệu, trạng thái bên trong thiết kế có thể được quan sát và kiểm tra, bất cứ khi nào có lỗi xảy ra dựa vào các ràng buộc được thiết đặt trước. Thêm vào đó, assertion dùng cho việc kiểm tra thiết kế cũng được sử dụng cho cả quá trình thực hiện việc kiểm tra tính ngang bằng của 2 thiết kế (formal verification). Một vài ví dụ về phương thức mô tả assertion:

- Khi thiết kế FIFO: Khi FIFO đang trong trạng thái FULL, việc thực hiện một chức năng để ghi vào FIFO là không được phép. Thông qua đặc tính này, người kĩ sư thiết kế có thể viết assertion, kiểm tra điều kiện này và báo sai cho trường hợp này.

- Khi thiết kế một tín hiệu là one-hot, được sử dụng để mô tả trạng thái của các state machine, người kĩ sư thiết kế có thể viết assertion để kiểm tra điều kiện one-hot và báo sai nếu tín hiệu không thỏa điều kiện này trong quá trình mô phỏng thiết kế.

-Khi thiết kế cặp tín hiệu request và response, điều kiện ràng buộc là tín hiệu response phải tích cực sau 1 chu kỳ khi có tín hiệu request. Thông qua ràng buộc này, kĩ sư thiết kế có thể dễ dàng viết assertion để kiểm tra điều kiện trên và báo sai nếu không thỏa.

Hầu hết các assertion đều có thể được diễn tả bởi ngôn ngữ Verilog HDL. Ví dụ sử dụng Verilog HDL để mô kiểm tra one-hot như trong file attach sau:

Tuy nhiên, cách viết này dài dòng và phức tạp, đôi khi sẽ đánh mất ý nghĩa ban đầu của assertion (do bản thân assertion code cũng có lỗi). Thay vào đó, các phương pháp sau được sử dụng:

- Open Verification Library (OVL)

- Formal Property Language Sugar

- SystemVerilog Assertions