Giới thiệu: Cuộc sống trong phòng DV
Là một kỹ sư xác minh làm việc trên các thiết kế bộ xử lý RISC-V, tôi nhận ra rằng không có hai dự án nào giống nhau. Với các phần mở rộng mới, các thông số kỹ thuật đang phát triển, áp lực tăng tốc chu kỳ và một luồng công cụ đổi mới liên tục, tôi luôn phải cân bằng giữa độ chính xác và tốc độ.
Sau khi tham gia buổi thuyết trình kỹ thuật của Synopsys về xác minh RISC-V tại Verification Futures 2025, tôi muốn chia sẻ quy trình làm việc này và cách các công cụ của Synopsys đã giúp tôi và đội ngũ của tôi tại Alpinum Consulting vượt qua sự phức tạp, giữ cho công việc được tổ chức và phát hiện các lỗi quan trọng sớm hơn.
Từ Thông Số Kỹ Thuật Đến Silicon: Quy Trình Hàng Ngày
Mỗi dự án RISC-V bắt đầu với một mê cung các bản cập nhật thông số kỹ thuật, các phần mở rộng kiến trúc và yêu cầu tích hợp. Tôi luôn bắt đầu bằng cách diễn giải các thông số kỹ thuật, trích xuất các tính năng và xác định những tính năng cần được bao phủ và tuân thủ.
Khi đã xác định được các tính năng, đã đến lúc phát triển bàn thử nghiệm, thiết lập một hạ tầng có thể tái sử dụng để xác minh nhiều kịch bản linh hoạt. Các cấp độ quyền hạn khác nhau, các tập con ISA, các phần mở rộng và các cấu hình phần cứng khác nhau khiến giai đoạn này trở nên vô cùng quan trọng. Thời gian đầu tư vào chuẩn bị ở giai đoạn này sẽ mang lại lợi ích sau này.
Tôi triển khai SystemVerilog Assertions (SVA) và các kiểm tra tùy chỉnh để phát hiện lỗi sớm. Những kiểm tra và khẳng định này được dệt vào các bàn thử nghiệm để đánh dấu các vấn đề như vi phạm thứ tự hoặc hành vi không đúng mức quyền hạn.
Tiếp theo là mô hình hóa độ bao phủ. Độ bao phủ chức năng là rất quan trọng, đặc biệt là cho các chuyển tiếp quyền hạn, hành vi ngắt và đồng bộ hóa đa lõi. Nếu không có độ bao phủ hoàn chỉnh, chúng tôi có thể bỏ lỡ các trường hợp góc.
Gỡ lỗi là một nhiệm vụ liên tục: theo dõi các lỗi khẳng định, sự không khớp theo chu kỳ và các điều kiện tranh chấp. Sau đó là báo cáo, nơi chúng tôi tóm tắt trạng thái bao phủ, tỷ lệ thất bại và các vấn đề mở trên bảng điều khiển xác minh của chúng tôi.
Chúng tôi cũng dựa vào xác minh chính thức sử dụng VC Formal song song với mô phỏng. Các công cụ chính thức giúp phát hiện các trường hợp góc mà mô phỏng có thể bỏ lỡ, chứng minh toán học về khả năng không thể đạt được, từ đó tiết kiệm thời gian cho những mô phỏng không hiệu quả sau này.
Quản lý quy trình này từ đầu đến cuối đòi hỏi phải xoay sở giữa các động cơ mô phỏng, công cụ chính thức, môi trường hồi quy và kiểm soát phiên bản. Các công cụ của Synopsys mang lại giá trị to lớn.
Cách Synopsys Giúp Tôi Hoàn Thành Công Việc
Tôi sử dụng Verdi® Verification Manager hàng ngày. Nó đơn giản hóa các phiên hồi quy và gỡ lỗi của tôi bằng cách cho phép tôi đi sâu vào các chế độ sóng, chéo tín hiệu và xem các kích hoạt khẳng định trong bối cảnh. Nó kết nối hoạt động của DUT với các lỗi khẳng định và kết quả hồi quy.
Sự đồng mô phỏng chính xác giữa DUT và mô hình tham chiếu là rất quan trọng. Dù xác minh các lệnh do người dùng định nghĩa hay tính nhất quán đa lõi, việc tích hợp mô hình đồng bộ giúp đảm bảo độ chính xác theo từng lệnh trong toàn bộ đường ống.
Một tài sản quan trọng khác là ImperasFPM, mô hình tham chiếu RISC-V có thể cấu hình cao. Nó vừa tuân thủ ISA vừa thích ứng. Tôi có thể sửa đổi nó cho các lệnh tùy chỉnh hoặc các phần mở rộng đặc quyền và xác minh nó với việc triển khai của chúng tôi trong thời gian thực.
Chúng tôi sử dụng mô phỏng để chạy các bài kiểm tra cấp OS hoặc một ngăn xếp firmware. Các công cụ của Synopsys có thể chạy các kịch bản phần mềm trên phần cứng để phát hiện các lỗi hệ thống không xuất hiện trong các bài kiểm tra đơn vị.
Sự Phức Tạp Thực Tế và Cách Chúng Tôi Xử Lý
Chúng tôi không chỉ xác minh các lõi — chúng tôi xác minh các trường hợp sử dụng. Trong dự án gần đây nhất, chúng tôi đã phải đối mặt với:
- Tương tác giữa các bộ xử lý đa lõi: đảm bảo tính nhất quán giữa các không gian bộ nhớ L1 và bộ nhớ chia sẻ
- Các phần mở rộng bảo mật: xác minh các chuyển tiếp vòng, quy trình khởi động an toàn và kiểm soát truy cập
- Các biến thể ISA: thử nghiệm các phần mở rộng tùy chọn với độ bao phủ vi kiến trúc mục tiêu
- Các lệnh tùy chỉnh: cách thêm các lệnh tùy chỉnh vào mô hình tham chiếu và độ bao phủ chức năng, và tạo ra các bài kiểm tra để xác minh các lệnh đó
- Chuyển tiếp chế độ quyền hạn: đảm bảo rằng các ngoại lệ và ngắt tuân thủ các cấp quyền đã cấu hình
- Giả lập phần mềm: thử nghiệm khởi động OS và các quy trình bare-metal với độ chính xác ở mức RTL
Các công cụ của Synopsys hỗ trợ tất cả các trường hợp này với khả năng mở rộng và độ hiển thị. Tôi có thể chuyển đổi giữa mô phỏng, chính thức và giả lập theo yêu cầu của dự án.
Sử Dụng RISC-V AIP Để Phát Hiện Nhiều Lỗi Hơn, Sớm Hơn
Một thành phần mà tôi đã trở nên phụ thuộc vào là RISC-V AIP. Nó bao gồm một tập hợp các khẳng định SVA có thể tái sử dụng và logic RTL có thể tổng hợp tích hợp trực tiếp với DUT của chúng tôi.
Trong một giai đoạn tích hợp gần đây, AIP đã phát hiện một điều kiện truy cập bất hợp pháp khi một tác vụ nền vô tình nâng cao quyền hạn trong quá trình trả lại ngắt. Vấn đề này có thể đã bị bỏ qua trong một mô phỏng cơ bản, nhưng khẳng định AIP đã phát hiện ra ngay lập tức.
Điều này đã tiết kiệm cho chúng tôi một chu kỳ gỡ lỗi hoàn toàn và tránh một lỗi phần mềm ở phía dưới mà sẽ mất hàng ngày để truy tìm.
Xác Minh Các Phần Mở Rộng ISA RISC-V Tùy Chỉnh
Một lợi thế của ISA RISC-V là khả năng thêm các lệnh tùy chỉnh. Tuy nhiên, khả năng này đi kèm với trách nhiệm xác minh phần mở rộng và đảm bảo rằng việc thêm nó không phá vỡ chức năng hiện có. Synopsys cung cấp một quy trình công việc cho điều này.
Kết Luận: Từ Áp Lực Đến Sự Tự Tin Với Các Công Cụ Đúng
Làm việc trong DV RISC-V không hề dễ dàng. Giữa những thay đổi trong thông số kỹ thuật, độ phức tạp của thiết kế và áp lực thời gian, các kỹ sư cần nhiều hơn chỉ là các kịch bản; họ cần một hệ sinh thái xác minh toàn diện.
Hệ sinh thái công cụ của Synopsys hoạt động liền mạch. Dù tôi đang chính thức hóa các điều kiện an toàn, so sánh kết quả mô hình với DUT, hay xem xét hồi quy đa lõi, tôi dành ít thời gian hơn cho việc theo đuổi các vấn đề thiết lập, gỡ lỗi và báo cáo, để lại cho tôi nhiều thời gian hơn để xác minh những gì quan trọng.
Dù bạn có tham dự hay bỏ lỡ phiên của Synopsys tại Verification Futures tại Đại học Reading vào ngày 1 tháng 7 năm 2025, tôi khuyên bạn nên xem bản ghi trực tuyến trên trang web hội nghị Verification Futures. Nếu quy trình làm việc của bạn giống như của tôi, bạn sẽ tìm thấy những ý tưởng thực tiễn để cải thiện độ bao phủ, tăng tốc độ gỡ lỗi và nâng cao sự tự tin trong thiết kế RISC-V tiếp theo của mình.
