Bài phát biểu của Intel về chính thức A Mind-Stretcher

Được xuất bản lại bởi Plato

Người theo dõi: 0

Synopsys đã đăng trên trang SolvNet một bài nói chuyện hấp dẫn do Tiến sĩ Theo Drane của Intel Graphics trình bày. Chủ đề là kiểm tra tính tương đương của đường dẫn dữ liệu. Nghe có vẻ giống như một chứng thực DPV chính thức khác của Synopsys VC nhưng dù sao thì bạn cũng nên xem nó. Đây là một cuộc thảo luận mở rộng tư duy về việc sử dụng và cân nhắc một cách trang trọng, nó sẽ đưa bạn vượt ra ngoài kiểu quảng cáo chiêu hàng hướng dẫn sử dụng thông thường để tiến vào lĩnh vực hấp dẫn hơn.

Bài phát biểu chính thức của Intel

Hiểu biết trí tuệ so với thử nghiệm mẫu

Mô phỏng dựa trên thử nghiệm dưới mọi hình thức là tuyệt vời và thường không thể thay thế được trong việc xác minh tính chính xác của đặc tả hoặc triển khai thiết kế. Nó cũng dễ dàng để bắt đầu. Chỉ cần viết một chương trình thử nghiệm và bắt đầu mô phỏng. Nhưng mặt trái của sự đơn giản đó là chúng ta không cần đầy đủ hiểu những gì chúng tôi đang thử nghiệm để bắt đầu. Chúng tôi tự thuyết phục mình rằng chúng tôi đã đọc thông số kỹ thuật một cách cẩn thận và hiểu tất cả các trường hợp góc cạnh, nhưng sẽ không quá phức tạp để lấn át sự hiểu biết của chúng tôi.

Trang trọng khuyến khích bạn hiểu chức năng ở mức độ sâu (ít nhất là nếu bạn muốn mang lại kết quả có giá trị). Trong ví dụ trên, một câu hỏi đơn giản – liệu z có thể bằng 1 không – không thể chứng minh được một ví dụ trong một tỷ chu kỳ trên trình mô phỏng. Không có gì đáng ngạc nhiên vì đây là trường hợp góc cực đoan. Một bài kiểm tra chính thức cung cấp một ví dụ cụ thể và rất không rõ ràng trong 188 giây và có thể chứng minh đây là trường hợp duy nhất như vậy trong thời gian ngắn hơn một chút.

OK, formal đã làm được điều mà thử nghiệm động không thể làm được, nhưng quan trọng hơn là bạn đã học được điều gì đó mà trình mô phỏng có thể chưa bao giờ nói với bạn. Rằng chỉ có một trường hợp có thể xảy ra tình trạng đó. Chính thức đã giúp bạn hiểu rõ hơn về thiết kế ở cấp độ trí tuệ chứ không chỉ là bản tóm tắt xác suất trên một tập hợp các trường hợp thử nghiệm hữu hạn.

vấn đề về thông số kỹ thuật

Ví dụ tiếp theo của Theo dựa trên một máy bán lỗi tự động (được gọi như vậy vì khi bạn nhấn nút, bạn sẽ gặp lỗi). Đây có vẻ là một vấn đề kiểm tra tương đương C với RTL khá đơn giản, mô hình C ở bên trái, mô hình RTL ở bên phải. Một điều ngạc nhiên đối với Theo trong những ngày đầu làm việc chính thức là hành vi dịch chuyển phải trong mô hình C không được xác định hoàn toàn trong tiêu chuẩn C, mặc dù gcc sẽ hoạt động hợp lý. Tuy nhiên, DPV sẽ phàn nàn về sự không phù hợp khi so sánh với RTL. Hành vi không xác định là một điều nguy hiểm để dựa vào.

Chính thức như một máy bán lỗi

So sánh thông số kỹ thuật giữa C và RTL đi kèm với các mối nguy hiểm khác, đặc biệt là về độ rộng bit. Việc cắt bớt hoặc mất bit mang trong tín hiệu trung gian (#3 ở trên) là những ví dụ điển hình. Đây có phải là vấn đề về thông số kỹ thuật không? Có thể có một vùng màu xám giữa các lựa chọn thông số kỹ thuật và triển khai.

Ngoài việc kiểm tra sự tương đương

Có vẻ như mục đích chính của DPV là kiểm tra sự tương đương giữa tham chiếu C hoặc RTL và việc triển khai RTL. Nhưng nhu cầu đó tương đối không thường xuyên và có nhiều cách hữu ích khác mà công nghệ như vậy có thể được áp dụng, nếu có chút đột phá. Đầu tiên là một tác phẩm kinh điển trong thế giới triển khai – tôi đã thực hiện một thay đổi, sửa một lỗi – kết quả là tôi có đưa ra bất kỳ lỗi mới nào không? Giống như kiểm tra SEQ sau khi bạn thêm cổng đồng hồ. Phân tích khả năng tiếp cận trong đầu ra khối có thể là một ứng dụng hữu ích khác trong một số trường hợp.

Không chỉ kiểm tra sự tương đương

Theo thậm chí còn sáng tạo hơn khi yêu cầu học viên sử dụng các ví dụ phản biện để hiểu rõ hơn về thiết kế, giải Sudoku or phân tích số nguyên. Ông thừa nhận DPV là một cách kỳ quặc để tiếp cận những vấn đề như vậy nhưng chỉ ra rằng mục đích của ông là phá bỏ ảo tưởng rằng DPV chỉ dùng để kiểm tra tính tương đương. Ý tưởng thú vị và chắc chắn phải căng não để suy nghĩ vượt qua những thử thách như vậy. (Tôi thú nhận là tôi ngay lập tức bắt đầu nghĩ đến vấn đề Sudoku ngay khi anh ấy đề cập đến nó.)

Thúc

Theo kết thúc bằng cuộc thảo luận về các phương pháp quan trọng trong việc sử dụng sản xuất, xung quanh các ràng buộc, hồi quy và so sánh với các mô hình RTL cũ. Ngoài ra còn có những thách thức trong việc biết liệu những gì bạn đang kiểm tra có thực sự phù hợp với đặc tả ngôn ngữ tự nhiên cấp cao nhất hay không.

Cuộc nói chuyện rất tràn đầy năng lượng, rất đáng xem ở đây trên SolvNet!

Chia sẻ bài đăng này qua: