What Do RTL Repair Benchmarks Actually Measure?

{"tags": ["RTL Repair", "Hardware Verification", "LLM Benchmark", "Formal Equivalence", "EDA", "Simulation Semantics", "Semiconductor AI"], "risks": ["Nguy cơ ngộ nhận năng lực LLM: điểm số sửa lỗi cao có thể chỉ do mô hình tự sinh lại từ đặc tả thay vì thực sự phân tích và sửa mã lỗi.", "Sai lệch kết quả giữa mô phỏng và kiểm chứng hình thức nếu không xử lý nhất quán ngữ nghĩa reset và trạng thái chưa khởi tạo (unknown-value).", "Độ phức tạp tính toán và nguy cơ timeout/undecided khi chạy kiểm chứng formal equivalence trên các khối RTL quy mô lớn."], "category": "Research", "entities": ["RTLRepairBench", "RTLRepairDataset", "GitHub (Evaaaz/RTLRepairBench)"], "summary_vi": "Nghiên cứu phân tích tính xác thực của các benchmark sửa lỗi RTL (Register-Transfer Level) cho LLM, chỉ ra hai sai lệch đo lường lớn: (1) kết quả giữa mô phỏng (simulation) và kiểm chứng hình thức (formal equivalence) có thể trái ngược nhau do ngữ nghĩa reset và so sánh chu kỳ đầu tiên; (2) điểm số sửa lỗi truyền thống không phân lập được việc mô hình thực sự sửa RTL lỗi hay chỉ đang sinh mã mới từ đặc tả (độ lệch từ -8,5 đến +18,3 điểm phần trăm qua 6 mô hình). Nhóm tác giả công bố tập dữ liệu RTLRepairDataset (5.784 cặp), bộ benchmark RTLRepairBench (459 ca kiểm thử) cùng bộ quy chuẩn đánh giá nghiêm ngặt nhằm chẩn đoán chính xác năng lực thực tế của mô hình.", "key_changes": ["Xây dựng RTLRepairDataset gồm 5.784 cặp (broken, fixed) để huấn luyện và RTLRepairBench gồm 459 trường hợp kiểm thử (374 đột biến cú pháp, 85 đột biến hành vi).", "Phát triển harness đánh giá hỗ trợ đồng thời cả mô phỏng (simulation) và kiểm chứng tương đương hình thức (formal equivalence).", "Phát hiện sai lệch thứ nhất: simulation và formal scoring đưa ra kết quả trái ngược nhau do ngữ nghĩa của tín hiệu reset và chu kỳ đầu tiên (first-cycle comparison).", "Phát hiện sai lệch thứ hai: trên 274 ca lỗi của mô hình, chênh lệch phục hồi giữa chỉ dùng đặc tả (spec-only) so với có kèm mã RTL lỗi dao động từ -8,5 đến +18,3 điểm phần trăm trên 6 mô hình, cho thấy điểm số benchmark truyền thống không chứng minh được mô hình có thực sự tận dụng mã lỗi hay không.", "Đưa ra các quy chuẩn kiểm soát đánh giá mới: báo cáo ngữ nghĩa khởi tạo/reset/chu kỳ đầu/giá trị unknown (X), minh bạch độ bao phủ của oracle/trường hợp undecided, và bắt buộc kèm baseline chỉ dùng đặc tả.", "Mã nguồn mở toàn bộ benchmark, tập huấn luyện, mã tạo dữ liệu và công cụ tái hiện tại https://github.com/Evaaaz/RTLRepairBench."], "sub_category": "RTL Hardware Verification & LLM Evaluation", "novelty_score": 82, "business_score": 70, "research_score": 88, "why_it_matters": "Trong thiết kế vi mạch, lỗi phần cứng ở mức RTL có thể dẫn đến thiệt hại hàng triệu USD nếu bị lọt vào khâu sản xuất (tape-out). Nghiên cứu này chứng minh các phương pháp đánh giá AI sửa lỗi phần cứng hiện tại có nhiều kẽ hở đo lường, khiến điểm số bị thổi phồng hoặc đánh giá sai bản chất. Việc chuẩn hóa quy trình đánh giá với nhận thức reset và baseline spec-only giúp các doanh nghiệp bán dẫn và nhóm nghiên cứu EDA định lượng chính xác năng lực thực sự của mô hình trước khi ứng dụng vào dây chuyền phát triển chip thực tế.", "developer_score": 82, "importance_score": 80, "possible_use_cases": ["Đánh giá và kiểm chuẩn khách quan năng lực sửa lỗi RTL của các mô hình LLM trong thiết kế vi mạch (ASIC/FPGA).", "Tích hợp bộ kiểm tra formal equivalence có nhận thức reset (reset-aware) vào pipeline CI/CD kiểm thử phần cứng bán dẫn.", "Sử dụng tập dữ liệu RTLRepairDataset để fine-tune các mô hình AI chuyên trách hỗ trợ kỹ sư EDA.", "Thiết lập chuẩn so sánh (baseline) tách biệt giữa khả năng tổng hợp mã mới từ đặc tả và năng lực debug mã lỗi có sẵn."], "actionability_score": 78}