AutoTrans: Terjemahan Otomatis Berbantuan AI untuk Security Assertion pada Prosesor RISC-V

Kerangka kerja yang menggabungkan ekstraksi sinyal berbasis regex, prompt LLM deterministik, dan verifikasi formal untuk mengotomatiskan terjemahan security assertion lintas target

Sharjeel Imtiaz; Uljana Reinsalu; Tara Ghasempouri· 2026· DOI 10.48550/arXiv.2609.10057

Masalah inti

Penggunaan kembali security assertion yang telah terverifikasi pada target prosesor RISC-V yang berbeda menjadi hambatan utama dalam verifikasi keamanan perangkat keras. Terjemahan assertion secara manual memakan waktu, sering kali membutuhkan berjam-jam per assertion. Meskipun large language model (LLM) dapat mempercepat proses ini, terjemahan LLM mentah mengalami signal hallucination—mengarang nama port yang tidak ada pada RTL target—dan menghasilkan keluaran yang bervariasi antar pembaruan model atau bahkan dalam versi model yang sama. Makalah ini memperkenalkan AutoTrans, kerangka kerja otomatis yang dirancang untuk mengatasi keterbatasan tersebut. AutoTrans mengintegrasikan tiga komponen utama: ekstraktor sinyal SystemVerilog ringan berbasis Regular Expression untuk mencegah signal hallucination, templat prompt deterministik dengan parameter inferensi yang dipatok untuk memastikan perakitan prompt identik byte antar eksekusi, dan proses verifikasi formal menggunakan JasperGold FPV untuk menjamin bahwa assertion yang dihasilkan benar-benar memverifikasi keamanan prosesor RISC-V. Kerangka kerja ini dievaluasi pada terjemahan security assertion dari RISC-V NS31A ke RISC-V IBEX me

Eksperimen terjemahan security assertion dari NS31A ke IBEX menggunakan Deepseek V4 menunjukkan bahwa AutoTrans mencapai 78% Auto Translation Acceptance Rate (TAR) secara otomatis, tanpa intervensi manusia. Setelah penyempurnaan oleh manusia, Final TAR mencapai 100%. Hal ini menunjukkan bahwa kerangka kerja ini secara signifikan mengurangi upaya manual sekaligus menjamin kebenaran. Prompting deterministik dan ekstraksi sinyal secara efektif memitigasi signal hallucination dan variabilitas model, sebagaimana dibuktikan oleh tingkat penerimaan otomatis yang tinggi. Langkah verifikasi formal memastikan bahwa semua assertion yang diterima valid untuk prosesor target.

Penggunaan kembali security assertion yang telah terverifikasi pada target prosesor RISC-V yang berbeda menjadi hambatan utama dalam verifikasi keamanan perangkat keras. Terjemahan assertion secara manual memakan waktu, sering kali membutuhkan berjam-jam per assertion. Meskipun large language model (LLM) dapat mempercepat proses ini, terjemahan LLM mentah mengalami signal hallucination—mengarang nama port yang tidak ada pada RTL target—dan menghasilkan keluaran yang bervariasi antar pembaruan model atau bahkan dalam versi model yang sama. Makalah ini memperkenalkan AutoTrans, kerangka kerja otomatis yang dirancang untuk mengatasi keterbatasan tersebut. AutoTrans mengintegrasikan tiga komponen utama: ekstraktor sinyal SystemVerilog ringan berbasis Regular Expression untuk mencegah signal hallucination, templat prompt deterministik dengan parameter inferensi yang dipatok untuk memastikan perakitan prompt identik byte antar eksekusi, dan proses verifikasi formal menggunakan JasperGold FPV untuk menjamin bahwa assertion yang dihasilkan benar-benar memverifikasi keamanan prosesor RISC-V. Kerangka kerja ini dievaluasi pada terjemahan security assertion dari RISC-V NS31A ke RISC-V IBEX menggunakan Deepseek V4.

AutoTrans terdiri atas tiga tahap utama:

AutoTrans mengatasi dua tantangan kritis dalam terjemahan assertion berbasis LLM: signal hallucination dan variabilitas keluaran. Ekstraktor sinyal berbasis regex menyediakan ground truth untuk nama sinyal, sehingga mencegah LLM mengarang port. Templat prompt deterministik dan parameter inferensi yang dipatok memastikan reproduktifitas, membuat pipeline tahan terhadap pembaruan model. Integrasi verifikasi formal berfungsi sebagai penyaring kebenaran, memastikan bahwa hanya assertion yang lolos pemeriksaan formal yang diterima. TAR otomatis sebesar 78% menunjukkan efektivitas langkah-langkah tersebut, sedangkan TAR akhir 100% setelah penyempurnaan oleh manusia menyoroti potensi otomatisasi lebih lanjut. Kerangka kerja ini dapat digeneralisasi ke target RISC-V dan deskripsi keamanan lainnya, meskipun kinerjanya dapat bergantung pada kualitas deskripsi berbahasa Inggris dan kemampuan LLM. Pekerjaan selanjutnya dapat mengeksplorasi perluasan AutoTrans ke bahasa deskripsi perangkat keras dan alat verifikasi lain.

Praktisi dan peneliti ilmu komputer

Membuka konten member…