Formal verification: from dreams to reality (Kiểm thử chính quy: từ giấc mơ tới hiện thực)

It seems to me now that mathematics is capable of an artistic excellence as great as that of any music, perhaps greater; not because the pleasure it gives (although very pure) is comparable, either in intensity or in the number of people who feel it, to that of music, but because it gives in absolute perfection that combination, characteristic of great art, of godlike freedom, with the sense of inevitable destiny; because, in fact, it constructs an ideal world where everything is perfect and yet true.

- Bertrand Russel.

Tạm dịch là: "Hiện giờ, đối với tôi, dường như toán học có năng lực của một nghệ thuật xuất sắc, nó tuyệt vời như bất cứ một loại hình âm nhạc nào, thậm chí còn hơn thế nữa; không phải vì điều thú vị nó mạng lại đối với loại hình âm nhạc đó là có thể so sánh được, hay là về cảm xúc mãnh liệt, hay là ở số lượng người cảm nhận nó (mặ dù rất thuần khiết), mà bởi vì nó mang lại sự hoàn hảo tuyệt đối, cái mà là sự tổ hợp của tự do tuyệt đối với sự cảm nhận về vận mệnh tất yếu - một đặc trưng của nghệ thuật sáng tạo; và bởi vì, trên thực tế, nó kiến tạo một thế giới lý tưởng mà ở đó mọi thứ là hoàn hảo và đúng đắn."

Bạn có phải là một kỹ sư đang thiết kế các con chips hay các SoC (system on chips) hiện đại và phức tạp ở mức RTL? Bạn đã từng ở trong những tình huống gây phiền nhiễu sau đây chưa?

• Thiết kế RTl của bạn đã ở trong trường hợp là một lỗi quan trọng (mất nhiều chi phí để sửa) bị bỏ sót bởi vì đã không test được hết các trường hợp quan trọng trong quá trình mô phỏng.
• Bạn tạo ra một module RTL mới, và muốn xem xem các hoạt động thực tế của nó diễn ra như thế nào bằng mô phỏng, nhưng bạn nhận ra rằng để làm được điều đó sẽ phải mất vài tuần để tạo ra testbench.
• Bạn chỉnh sửa một phần của RTl cho mục đích synthesis hay điều chỉnh timing, và bạn cần hàng tuần mô phỏng để đảm bảo bạn không thực sự thay đổi chức năng của nó.
• Bạn đang ở trong những giai đoạn sau của việc thẩm định một thiết kế, và các lỗi mới liên tục xuất hiện đã minh thị  các mô phỏng ngẫu nhiên của bạn chưa cung cấp các thông tin về coverage chính xác.
• Bạn điều chỉnh đặc tả kĩ thuật về thanh ghi điều khiển (control register specification) cho thiết kế của bạn và cần dành nhiều thời gian để mô phỏng nhằm đảm bảo những sự thay đổi ở RTL của bạn thực thi chính xác những chức năng của các thanh ghi này. 

Nếu quả vậy, chúc mừng bạn: cuốn sách này dành cho bạn! Mỗi một trong số các tình huống trên có thể được giải quyết sử dụng kiểm thử chính quy (formal verification) để làm tăng đáng kể hiệu suất tổng thể và sự tự tin của bạn về thiết kế của bạn. Bạn sẽ làm được điều này (will achieve this) bằng cách sử dụng các công cụ toán học chính quy (formal mathematical tools) để tạo ra hiệu suất và năng suất ngày càng tăng mạnh, cũng như đưa tính chặt chẽ toán học vào trong các lĩnh vực mà trước đây phụ thuộc vào các việc kiểm tra không chính quy. 

Kiểm thử chính quy là gì

Chúng ta hãy bắt đầu với một định nghĩa đơn giản:

• Kiểm thử chính quy (Formal verification - FV) là việc sử dụng các công cụ mà nó phân tích bằng toán học tất cả các hành vi có thể có của một thiết kế thay vì tín toán các kết quả từ các giá trị cụ thể.

Điều này có nghĩa là gì? Về cơ bản, một công cụ FV sẽ nhìn vào toàn bộ các trường hợp mà việc mô phỏng có thể được thực hiện, thay vì chỉ thử các giá trị cụ thể. Tất nhiên nó không thật sự chạy tất cả các mô phỏng mà sẽ sử dụng các kĩ thuật toán học thông minh để đánh giá tất cả các hành vi có thể có. Hình 1.1 minh họa sự khác biệtgiữa mô phỏng và kiểm thử chính quy: mô phỏng nhìn vào các điểm riêng rẽ nằm trong số tổng thể không gian cần khảo sát, trong khi FV sẽ đánh giá toàn bộ không gian đó một lần.

Từ định nghĩa đơn giản này, bạn có thể đã cảm nhận được sức mạnh đáng ngạc nhiên mà chúng ta nhận được khi sử dụng kĩ thuật này. Trong nhiều lĩnh vực, sử dụng phương pháp mạnh mẽ này không còn được xem như là một lựa chọn nữa. Bạn có thể đã nghe về lỗi Pentium FDIV nổi tiếng từ những năm 1990s, trong đó các trường hợp hiếm gặp đã được phát hiện ra, mà ở đó, các bộ vi xử lý của Intel có thể thực hiện phép chia với kết quả không chính xác. Đây là trường hợp mà trong đó kiểm thử dựa trên mô phỏng, nói một cách đơn giản, không "phóng phi tiêu" trúng vào các trường hợp test ngẫu nhiên mà dẫn đến lỗi này trước khi sản phẩm được đưa ra thị trường tiêu thụ. Năm đó Intel mất 475 triệu đô la (khoảng 755 triệu đô la ở năm 2014) cho chi phí thay thế các bộ xử lý đó; khi bạn biết về sự phát triển của Intel kể từ ngày đó, một lỗi tương tự như vậy ngày nay có thể sẽ tốn đến hàng tỷ đô la. Do đó, trong các lĩnh vực cực kỳ quan trọng, kiểm thử chính quy được xem là bắt buộc để tránh bỏ sót những lỗi nguy hiểm.

Tuy nhiên, FV không còn chỉ được dùng để tìm các lỗi khó tìm nữa. Như chúng ta sẽ nhìn thấy khi chúng ta khám phá nhiều kĩ thuật mà đang phổ biến hiện nay, FV nên được thực sự coi là một công cụ đa năng để tương tác với, để kiểm thử và để hiểu rõ các thiết kế của chúng ta. Từ những ngày đầu phát triển đến quá trình tìm lỗi ở giai đoạn post-silicon, tận dụng các phương pháp chính quy một cách thích hợp ở mỗi giai đoạn thiết kế có thể tạo ra thông lượng lớn hơn, làm tăng mức độ tự tin về thiết kế và giảm thời gian đưa sản phẩm ra thị trường.

Tại sao lại cần cuốn sách này?

Mục đích của chúng tôi là để cung cấp những công cụ hữu ích cho các kỹ sư thiết kế và thẩm định VLSI. Trong quá khứ, có nhiều ấn phẩm về FV từ quan điểm học thuật, chẳng hạn như [Mcm93] và [Kro99]. Tuy nhiên, những cuốn sách này thường tập trung vào