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ả khác cách, 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ã được chạy khác trường hợp chức năng đã kiểm. 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 mô tả hữu hạn lượt mô phỏng qua thành chứng minh toán học vô hạn thời gian.

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ũ.