Kế hoạch kiểm chứng, coverage và tham chiếu độc lập

Kế hoạch kiểm chứng biến đặc tả thành mệnh đề kiểm tra được

Thay “hoạt động tốt” bằng yêu cầu cụ thể: trạng thái sau reset, đầu ra với đầu vào bình thường, giữ khi dừng, xử lý đầu vào cấm, thời điểm hoàn tất. Gắn mỗi yêu cầu với ít nhất một kiểm tra và điểm quan sát giúp tìm thiếu sót.

Vì sao cần tham chiếu độc lập

Chép cùng slice^{iSlice Chọn dải bit liên tiếp trong vector. Phạm vi chọn quyết định độ rộng và thứ tự bit kết quả. Tìm hiểu thêm} của RTL dịch vào tham chiếu có thể chép luôn lỗi chỉ mục. Dùng mô hình nhân/modulo số nguyên hoặc so hậu tố chuỗi để thể hiện đặc tả theo cách khác, giúp kiểm chéo. Nhưng khác biểu diễn không tự chứng minh độc lập; kiểm ví dụ nhỏ bằng tay.

Coverage không phải số lượt qua

Coverage dòng mã đã chạy khác với coverage của các trường hợp chức năng đã kiểm tra. Tổ hợp chéo reset×enable, state×input, full×push×pop có thể lộ lỗi. Không chỉ giao cho ngẫu nhiên; thêm directed test cho tổ hợp hiếm, quan trọng.

Mạch tổ hợp N đầu vào có thể kiểm hết $2^N$ trường hợp, còn mạch tuần tự có cả chuỗi thời gian. Cần xét trạng thái có tới được và bất biến^{iBất biến Điều kiện phải luôn đúng trong mọi thực thi được phép. Ví dụ số phần tử FIFO sâu 4 luôn từ 0 đến 4.} có giữ ở mọi chuyển không. Không coi một số hữu hạn lượt mô phỏng thành công là chứng minh toán học cho hành vi trong thời gian vô hạn.

Tạo đáp án độc lập từ đặc tả thay vì chép cài đặt. Khi thất bại, ngoài thực tế còn ghi đầu vào và trạng thái ngay trước.

Thu nhỏ lỗi và ghi lại

Lưu trạng thái trước, đầu vào, kỳ vọng, thực tế của mismatch đầu. Bỏ kích thích không cần để có phản ví dụ nhỏ nhất còn lỗi, rồi sửa. Không chỉ chạy lại kiểm tra vừa sửa; hồi quy cả kiểm tra biên và reset^{iReset Điều khiển đưa trạng thái về giá trị đầu đã định. Phải quy định đồng bộ hay bất đồng bộ và ưu tiên so với các điều khiển khác. Tìm hiểu thêm} cũ.