Một cách tiếp cận khác để xác minh chính thức các chức năng đường dẫn dữ liệu rất thách thức. Paul Cunningham (GM, Xác minh tại Cadence), Raúl Camposano (Silicon Catalyst, doanh nhân, cựu CTO Synopsys và bây giờ là Silvaco CTO) và tôi tiếp tục loạt bài về ý tưởng nghiên cứu. Như mọi khi, phản hồi hoan nghênh. Chúng tôi dự định sẽ bổ sung thêm một số nội dung vào quá trình khám phá xác minh của mình trong năm nay. Chi tiết để làm theo!

Sự đổi mới

Lựa chọn của tháng này là Xác minh chính thức đa thức của các bộ cộng dấu phẩy động. Bài viết này đã được xuất bản trong Hội nghị DATE năm 2023. Các tác giả đến từ Đại học Bremen, Đức.

Việc triển khai phần tử đường dữ liệu phải được chứng minh là hoàn toàn chính xác (hãy nhớ đến lỗi dấu phẩy động Pentium khét tiếng), đòi hỏi phải có bằng chứng chính thức. Tuy nhiên, biểu đồ trạng thái BDD cho các phần tử dấu phẩy động nhanh chóng bùng nổ, trong khi bằng chứng SAT thường bị giới hạn do đó không thực sự hoàn chỉnh.

Cách giải quyết phổ biến hiện nay là sử dụng tính năng kiểm tra tương đương bằng mô hình tham chiếu C/C++, hoạt động rất tốt nhưng tất nhiên phụ thuộc vào một tham chiếu đáng tin cậy. Tuy nhiên, một số tâm hồn dũng cảm vẫn đang cố gắng tìm ra con đường cùng BDD. Các tác giả này đề xuất các phương pháp sử dụng phân tách trường hợp để hạn chế bùng nổ đồ thị trạng thái, giảm độ phức tạp giới hạn theo cấp số nhân xuống đa thức. Hãy xem những người đánh giá của chúng tôi nghĩ gì!

Quan điểm của Paul

Bài viết nhỏ gọn, dễ đọc để khởi động năm 2024 và về một vấn đề kinh điển trong khoa học máy tính: quản lý sự bùng nổ kích thước BDD trong quá trình xác minh chính thức.

Đóng góp chính của bài báo là một phương pháp mới để “phân tách trường hợp” trong việc xác minh chính thức các bộ cộng dấu phẩy động. Theo truyền thống, phân tách trường hợp có nghĩa là chọn một biến boolean làm cho BDD tăng kích thước và chỉ chạy hai bằng chứng chính thức riêng biệt, một cho “trường hợp” trong đó biến đó là đúng và một cho trường hợp biến đó là sai. Nếu cả hai bằng chứng đều đạt, thì điều đó có nghĩa là bằng chứng tổng thể cho BDD đầy đủ bao gồm biến đó nhất thiết phải đạt. Tất nhiên, việc phân tách chữ hoa chữ thường cho n biến có nghĩa là 2^n trường hợp, vì vậy nếu bạn sử dụng nó ở mọi nơi thì bạn chỉ cần đổi một số mũ này lấy một số khác.

Bài viết này nhận thấy rằng việc phân tách trường hợp không chỉ cần dựa trên các biến Boolean riêng lẻ. Bất kỳ sự phân chia nhỏ đầy đủ nào của vấn đề đều hợp lệ. Ví dụ, trước khi chuẩn hóa số mũ cơ số, có thể thực hiện phân chia trường hợp số số 10 đứng đầu trong cơ số - tức là XNUMX số XNUMX đứng đầu trong cơ số, một số XNUMX đứng đầu trong cơ số, v.v. Sự lựa chọn phân tách cụ thể này kết hợp với một phân chia xảo quyệt khác trong bước dịch chuyển căn chỉnh đạt được một sự thỏa hiệp kỳ diệu sao cho bằng chứng tổng thể cho phép cộng dấu phẩy động chuyển từ cấp số nhân sang đa thức về độ phức tạp. Giờ đây, mạch cộng dấu phẩy động có độ chính xác gấp đôi có thể được chính thức chứng minh là chính xác trong XNUMX giây. Đẹp!

Quan điểm của Raúl

Bài viết ngắn này giới thiệu một cách tiếp cận mới để quản lý vấn đề bùng nổ kích thước trong việc xác minh chính thức các bộ cộng dấu phẩy động bằng cách sử dụng BDD, một vấn đề kinh điển trong kiểm tra tương đương. Theo truyền thống, điều này được giải quyết bằng cách phân tách trường hợp, tức là chia bài toán dựa trên giá trị của các biến Boolean riêng lẻ (0, 1), cũng dẫn đến sự tăng trưởng theo cấp số nhân về độ phức tạp với số lượng biến được phân chia. Dựa trên những quan sát về nơi xảy ra sự bùng nổ về kích thước khi xây dựng BDD, bài báo đề xuất ba phương pháp phân tách trường hợp sáng tạo. Chúng không dựa trên các biến Boolean riêng lẻ và dành riêng cho các bộ cộng dấu phẩy động (tất nhiên chúng không đơn giản hóa việc kiểm tra tương đương tổng quát đối với P).

1. Phân tách trường hợp dịch chuyển căn chỉnh: Bài báo đề xuất phân tách theo số lượng dịch chuyển hoặc chênh lệch số mũ, giảm đáng kể số lượng trường hợp cần thiết để xác minh.
2. Tách các trường hợp zero hàng đầu: Để giải quyết sự bùng nổ ở dịch chuyển chuẩn hóa, bài báo đề xuất tạo các trường hợp dựa trên số lượng các số 0 đứng đầu trong kết quả phép cộng.
3. Số bất thường và làm tròn: Các số bất thường được xử lý bằng cách thêm đơn giản hóa trong trường hợp chúng có thể xảy ra; làm tròn không gây ra vụ nổ ở kích thước BDD.

Bằng cách lựa chọn một cách chiến lược các phân tách trường hợp này, độ phức tạp của bằng chứng tổng thể cho phép cộng dấu phẩy động có thể giảm từ hàm mũ xuống đa thức. Kết quả là, việc xác minh chính thức các mạch thêm dấu phẩy động có độ chính xác gấp đôi và gấp bốn lần, mà trong mô phỏng biểu tượng cổ điển hết thời gian là hai giờ, giờ đây có thể hoàn thành sau 10-300 giây!

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

• Phân phối nội dung và PR được hỗ trợ bởi SEO. Được khuếch đại ngay hôm nay.
• PlatoData.Network Vertical Generative Ai. Trao quyền cho chính mình. Truy cập Tại đây.
• PlatoAiStream. Thông minh Web3. Kiến thức khuếch đại. Truy cập Tại đây.
• Trung tâmESG. Than đá, công nghệ sạch, Năng lượng, Môi trường Hệ mặt trời, Quản lý chất thải. Truy cập Tại đây.
• PlatoSức khỏe. Tình báo thử nghiệm lâm sàng và công nghệ sinh học. Truy cập Tại đây.
• nguồn: https://semiwiki.com/eda/342214-bdd-based-formal-for-floating-point-innovation-in-verification/