[System Verilog] Kiểm tra formal - phần 1: Các phương pháp kiểm tra thiết kế

Đây là bài thứ nhất trong loạt bài trao đổi về phương pháp kiểm tra formal (formal verification) sử dụng System Verilog. Trước khi đi sâu về việc làm thế nào sử dụng System Verilog để kiểm tra formal. Bài này trình bày tổng quan về các phương pháp kiểm tra (xác minh) tính đúng đắn của một thiết kế để bạn đọc có thể hình dung cơ bản về vài trò của các phương pháp và phạm vi áp dụng trong một quy trình thiết kế vi mạch.

1) Các phương pháp kiểm tra (xác minh) thiết kế

Việc kiểm tra thiết kế được chia thành 3 nhóm phương pháp:

1. Kiểm tra dựa trên mô phỏng (simulation-based verification), gọi tắt là mô phỏng
2. Kiểm tra formal (formal verification)
3. Kiểm tra bán formal (semi-formal verification)

Chú ý, ban đầu bài viết dịch từ "formal" là "hình thức" nhưng tác giả cảm thấy không thể hiện được bản chất của phương pháp này nên chuyển qua từ "thuộc tính". Tuy nhiên, phương pháp này lại được chia thành 2 nhóm nhỏ là kiểm tra tương đương và kiểm tra thuộc tính (property) nên tác giả quyết định giữ nguyên từ formal để tranh gây hiểu lầm.
Để phân biệt các phương pháp này, chúng ta căn cứ vào các đặc điểm sau:

1. Mô phỏng dựa trên các vector, phương pháp này cần Stimulus để cung cấp các vector (giá trị) đầu vào và cần có một tập các vector (giá trị) đầu ra để so sánh, kiểm tra so với kết quả của thiết kế. Kiểm tra formal  không dựa trên các vector.
2. Mô phỏng định hướng theo đầu vào (input) vì người kiểm tra sẽ cung cấp các giá trị đầu vào mong muốn để tạo ra trường hợp cần kiểm tra. Trong khi đó, kiểm tra formal định hướng theo đầu ra, người thiết kế sẽ cung cấp các thuộc tính của các đầu ra để kiểm tra. Chú ý, kiểm tra formal sẽ kiểm tra thuộc tính đầu ra chứ không phải kiểm tra giá trị đầu ra.
3. Kiểm tra bán formal là một phương pháp kết hợp giữa mô phỏng và kiểm tra formal. Nó vừa dựa trên các vector đầu vào vừa thực hiện kiểm tra thuộc tính lân cận các vector.

2) Mô phỏng

Phương pháp mô phỏng đặt thiết kế trong một testbench, thiết kế lúc này gọi là DUT (Design Under Test). Các kích thích ngõ vào (các test vector) được đưa đến testbench. Ngõ ra thiết kế được so sánh với các giá trị ngõ ra tham khảo.

Hình 1: Phương pháp kiểm tra dựa trên mô phỏng

Phạm vi áp dụng:

• Mức RTL code
• Mức gate netlist sau tổng hợp
• Mức Layout sau layout

Phần mềm sử dụng: là các trình mô phỏng (simulator)

• Incisive Enterprise Simulator - Cadence
• ModelSim and Questa - Mentor Graphic
• VCS - Synopsys

Ưu điểm:

• Kiểm tra được các chức năng và hoạt động như thực tế vì các test vector dựa theo các trường hợp sử dụng thực tế của thiết kế.
• Các phần mềm mô phỏng thường trực quan và dễ debug

Nhược điểm:

• Số lượng test vector là có giới hạn và được tạo theo những kịch bản (mục đích) kiểm tra nhất định. Ở điểm này, tuy ngôn ngữ mô phỏng như System Verilog có hỗ trợ tạo các test vector ngẫu nhiên nhưng người kiểm tra vẫn phải ràng buộc (constraint) để giá trị ngẫu nhiên nằm trong phạm vi sử dụng thực tế.
• Thời gian để kiểm tra toàn bộ thiết kế có thể lâu hơn (tốc độ coverage).

Hình 2: Phạm vi áp dụng phương pháp mô phỏng

3) Kiểm tra formal

Khác với mô phỏng, kiểm tra formal không yêu cầu tạo ra các test vector. Nó có thể được chia làm hai loại là:

• Kiểm tra tương đương (equivalence checking)
• Kiểm tra thuộc tính (property verification)

3.1) Kiểm tra tương đương

Kiểm tra tương đương là xác định xem giữa hai mô hình có tương đương về chức năng hay không, ví dụ như giữa thiết kế và một mô hình tham khảo. Kiểm tra tương đương không thể thực hiện với phương pháp mô phỏng với trình mô phỏng thông thường vì số lượng test vector cần đến là quá lớn. Nếu dùng phương pháp mô phỏng để kiểm tra tương đương chúng ta cần có số lượng test vector bao phủ toàn bộ các tổ hợp giá trị có thể của ngõ vào, ví dụ số bit ngõ vào là 32 bit thì số lượng test vector cần là (2^32 - 1) = 4.294.967.295, hơn 4 tỷ.

Kiểm tra tương đương được thực hiện với các phần mềm chuyên dụng. Việc kiểm tra tương đương được thực hiện dựa trên hai phương pháp.

Phương pháp thứ nhất, các phần mềm sẽ dựa trên thiết lập (cấu hình) của người dùng để giới hạn phạm vi ngõ vào, tự động tạo ra các test vector phù hợp để xác định sự tương đương của 2 mạch. phương pháp này cũng giống như mô phỏng, cung cấp các vector đầu vào để kiểm tra và cùng đối mặt với vấn đề số lượng vector quá nhiều khi số ngõ vào lớn nhưng thông qua phần mềm các vector được tạo tự động có giới hạn đủ để phân kiểm tra 2 mạch.

Phương pháp thứ hai, 2 mạch cùng được biến đổi về một dạng tiêu chuẩn chứa các thuộc tích đặc trưng để so sánh, ví dụ như "Sơ đồ quyết định nhị phân theo thứ tự tối giản" (Reduced Ordered Binary Decision Diagram).

Hình 3: Phương pháp kiểm tra tương đương

Phạm vi áp dụng:

• RTL và Gate netlist
• Gate netlist trước và sau khi chèn các mạch DFT
• Gate netlist trước và sau Place&Route

Phần mềm sử dụng:

• Formality - Synopsys
• Conformal - Cadence
• JasperGold - Cadence
• Formal Pro - Mentor Graphic

Hình 4: Phạm vi kiểm tra tương đương

Chú ý, kiểm tra tương đương sẽ không phải là mục tiêu phân tích của loạt bài này, mục tiêu chính của loạt bài này là về kiểm tra thuộc tính trong phương pháp kiểm tra formal.

3.2) Kiểm tra thuộc tính

Kiểm tra thuộc tính là kiểm tra hoạt động, hành vi của thiết kế có phù hợp với thuộc tính đã được quy định trong spec hay không. Một thuộc tính là một phần của spec, nó là một hành vi, đặc điểm mà thiết kế được yêu cầu phải có. Một thiết kế có nhiều thuộc tính khác nhau, các thuộc tính này có thể được mô hình hóa bằng ngôn ngữ kiểm tra như System Verilog. Các mô hình dùng để kiểm tra này có thể được gọi là các "model checker".

Hình 5: Phương pháp kiểm tra thuộc tính

Việc mô tả một thuộc tính giống như việc mô tả một chức năng thiết kế nhưng theo một cách khác. Ví dụ, chức năng của thiết kế được mô tả bằng Verilog khả tổng hợp còn thuộc tính tương ứng được mô tả bằng System Verilog Assertion. Ví dụ, chúng ta có spec sau đây: 

Hình 6: Yêu cầu của spec

Chức năng trên được mô tả trong thiết kế như sau:

always @ (posedge clk) begin
  if (rst) syn0 <= 1'b0;
  else     syn0 <= ctrl;
end

Một thuộc tính của chức năng này là nếu tín hiệu reset rst=0 và ctrl=1 thì syn0 sẽ bằng 1 ở chu kỳ sau. Thuộc tính này được mô hình như sau:

chk_syn0: assert property (@ (posedge clk) (~rst & ~syn0 & ctrl) |-> ##1 syn0)
  else  $display("[%d] Assertion FAIL", $time);

Trong quá trình kiểm tra nếu thiết kế không đảm bảo thuộc tính này "Assertion FAIL" sẽ được hiển thị.

4) So sánh giữa mô phỏng và kiểm tra formal
Một vector mô phỏng được xem như một điểm của không gian đầu vào (input space). Không gian đầu vào được hiểu là tập chưa toàn bộ các giá trị ngõ vào có thể có của thiết kế. Việc mô phỏng là lấy mẫu không gian đầu vào nên thiết kế chỉ đảm bảo không tồn tại lỗi nếu tất cả các điểm đầu vào đều được lấy mẫu. Khác với mô phỏng, kiểm tra formal làm việc ở mức thuộc tính. Với một thuộc tính, việc kiểm tra thực hiện trên tất cả các điều kiện ngõ vào có thể.
Nếu nhìn ở đầu ra, mô phỏng kiểm tra chỉ kiểm tra một điểm ngõ ra tại mỗi thời điểm. Trong khi đó, kiểm tra formal là kiểm tra thuộc tính mà một thuộc tính có thể là một nhóm điểm ngõ ra.

Hình 7: Minh họa không gian đầu ra của mô phỏng (trái) và kiểm tra formal (phải)

Có thể thấy, sử dụng kiểm tra formal có thể giúp chúng ta xác minh được toàn bộ thiết kế nhanh hơn mô phỏng. Tuy nhiên để đảm bảo toàn bộ thiết kế đã được kiểm tra thì tập các thuộc tính phải được xây dựng đầy đủ.
Một điểm bất lợi chính của phần mềm kiểm tra formal là tốn nhiều dung lượng bộ nhớ khi thực thi. Bên cạnh đó, do tính chát kiểm tra thuộc tính (nhóm điểm) nên phần mềm có thể ít trực quan và khó sử dụng.