Ứng dụng và dịch vụ kiểm chứng hình thức Axiomise

Axiomise là công ty kiểm chứng hình thức thành lập năm 2017 tại Anh bởi TS. Ashish Darbari và TS. Vidya Chandran Darbari. Công ty hướng tới phổ biến kiểm chứng hình thức, để đội thiết kế chip chứng minh tính đúng của thiết kế một cách toàn diện thay vì chỉ dựa vào mô phỏng vốn có thể bỏ sót lỗi ở trường hợp biên.

Nền tảng axiomiser chứa các ứng dụng cấu hình được: formalISA kiểm chứng hình thức tự động cho bộ xử lý RISC-V, nocProve cho các triển khai mạng trên chip tùy biến, footprint phân tích diện tích silicon và floatrix. Ứng dụng kiểm tra thiết kế Verilog hoặc VHDL theo SystemVerilog Assertions, bộ máy trừu tượng CoreProve giúp các chứng minh có giới hạn hội tụ. Công ty còn cung cấp dịch vụ kiểm chứng hình thức cho sign-off SoC và lõi RISC-V, tư vấn và đào tạo, đã làm việc với hơn 20 khách hàng và Bluespec.

• formalISA: ứng dụng kiểm chứng hình thức tự động cho lõi bộ xử lý RISC-V.
• nocProve: sign-off hình thức cho thiết kế mạng trên chip tùy biến, cấu hình theo giao thức và quy tắc định tuyến.
• footprint: công cụ phân tích diện tích silicon ra mắt năm 2025.
• Bộ máy CoreProve: bộ máy chứng minh dựa trên trừu tượng hóa giúp chứng minh có giới hạn hội tụ.
• Dịch vụ kiểm chứng: sign-off SoC đầu cuối và kiểm chứng hình thức RISC-V.
• Đào tạo: khóa học kiểm chứng hình thức trực tuyến và có giảng viên.

Đội Việt Nam phát triển vi điều khiển RISC-V có thể dùng formalISA để kiểm tra tuân thủ tập lệnh trước tape-out. Startup chip AI có thể sign-off mạng trên chip tùy biến bằng nocProve. Trường đại học hoặc trung tâm thiết kế có thể tổ chức đào tạo kiểm chứng hình thức để nâng cao năng lực cho kỹ sư kiểm chứng mới.

Chứng minh hình thức toàn diện tìm ra lỗi ở trường hợp biên mà mô phỏng có thể bỏ sót trong bộ xử lý và mạng trên chip. Các ứng dụng dựng sẵn giảm yêu cầu chuyên môn khi bắt đầu kiểm chứng hình thức cho lõi RISC-V hoặc NoC. nocProve được công bố cho kết quả trong vài giờ. Chương trình đào tạo đã tiếp cận hơn 1.600 kỹ sư, giúp đội ngũ xây dựng năng lực kiểm chứng hình thức nội bộ.

Sự phổ biến của RISC-V cho phép nhiều công ty tự thiết kế bộ xử lý, làm tăng nhu cầu kiểm chứng kỹ lõi tùy biến. Chip tăng tốc AI dựa vào mạng trên chip phức tạp, nơi lỗi bế tắc và lỗi giao thức gây tổn thất lớn. Việt Nam và Đông Nam Á đang đầu tư vào RISC-V và đào tạo thiết kế chip, trong khi kỹ năng kiểm chứng hình thức vẫn còn khan hiếm trong khu vực.

Thành lập năm 2017, trụ sở tại London, Vương quốc Anh, bởi TS. Ashish Darbari (CEO) và TS. Vidya Chandran Darbari. Đối tác của Bluespec trong kiểm chứng lõi RISC-V. Nhà tài trợ các sự kiện DVCon tại Mỹ, châu Âu, Ấn Độ và Nhật Bản trong năm 2025 và 2026.