Apakah Anda Tahu Pasti RTL RISC-V Anda Tidak Mengandung Kejutan?

Mengingat kebaruan relatif dan kompleksitas desain RISC-V RTL, apakah Anda membeli inti yang didukung secara komersial atau mengunduh penawaran sumber terbuka yang populer, ada risiko kecil namun tidak nol dari kejutan yang tidak diinginkan yang lolos tanpa terdeteksi ke produk akhir Anda. Dalam urutan probabilitas tinggi ke rendah, pertimbangkan:

• Kehadiran bug kasus sudut yang aneh namun sepenuhnya mungkin
• Bug “di dalam” instruksi khusus yang Anda atau vendor Anda buat untuk aplikasi Anda
• Bug "di tepi" dari instruksi khusus — misalnya, instruksi dijalankan dengan benar, tetapi entah bagaimana meninggalkan mesin dalam keadaan rusak
• Terkait: fitur baru yang tidak terdokumentasi dan/atau tidak ditentukan dengan baik yang tanpa disadari membuka lubang pada desain
• Logika Trojan jahat diam-diam dimasukkan melalui serangan rantai pasokan

Pendekatan mitigasi umum

Secara alami, garis pertahanan pertama adalah pemeriksaan ahli terhadap kode RTL yang masuk atau berkembang. Jelas, ini harus dilakukan; tetapi harus sama jelasnya bahwa teknik ini - seperti yang mereka katakan di dunia matematika - "diperlukan tetapi tidak cukup" (bahkan jika Anda meminta Profesor Patterson sendiri meninjau kode Anda).

Garis pertahanan berikutnya menerapkan pendekatan berbasis simulasi: Instruction Set Simulation (ISS), perbandingan otomatis DUT Anda dengan model emas dewasa, testbench UVM acak terbatas untuk simulasi DUT RTL, dan bahkan menyalurkan stimulus dunia nyata ke emulasi yang dibantu perangkat keras dari DUT. Sekali lagi, semua pendekatan ini berharga dan harus dilakukan; tetapi mereka semua menderita kelemahan yang sama: mereka secara inheren tidak lengkap karena bergantung pada pembangkitan stimulus. Misalnya, dalam kasus serangan rantai pasokan yang ekstrem tetapi mungkin terjadi, pengembang logika Trojan telah dengan sengaja membuat urutan pemicu sinyal dan data yang kemungkinan besar akan lolos dari deteksi bahkan oleh peretas topi putih yang paling kreatif sekalipun. Dan tentu saja, bug fungsional memiliki caranya sendiri dalam menggunakan entropi alami untuk tetap tersembunyi.

Intinya adalah bahwa satu-satunya cara untuk benar-benar yakin bahwa RTL RISC-V Anda bebas dari kejutan alami atau berbahaya adalah dengan menerapkan metode formal yang lengkap untuk memverifikasi desain.

Lebih mudah diucapkan daripada dilakukan, bukan?

Ya dan tidak: 14 tahun yang lalu, analisis semacam ini hanya dapat dilakukan oleh peneliti tingkat PhD dengan menggunakan program buatan tangan mereka sendiri. Namun sejak 2008, alat dan teknik telah diproduksi sedemikian rupa sehingga siapa pun yang terbiasa dengan dasar-dasar verifikasi formal dan penulisan System Verilog Assertions (SVA) standar IEEE dapat dengan cepat menerapkan dan berhasil di sini.

Proses berbasis formal tiga tahap

Alur berbasis formal yang direkomendasikan terungkap sebagai berikut:

1. Buat testbench formal yang "memodelkan" spesifikasi DUT
2. Tentukan kendala input dan periksa untuk dijalankan terhadap DUT
3. Jalankan analisis

Langkah 1 – Buat testbench formal yang “memodelkan” spesifikasi DUT

Fondasi dari metodologi ini adalah menulis satu set properti yang mewakili perilaku setiap instruksi dalam desain RISC-V Anda. Tugasnya adalah untuk menangkap efek dari instruksi yang diberikan pada output IP dan status arsitektur internal (di dunia RISC-V, ini adalah penghitung program (PC) dan file register (RF)) untuk setiap urutan input panjang yang sewenang-wenang. Ini dilakukan dengan menggunakan ekstensi yang dibuat khusus untuk IEEE SVA yang disebut Operational SVA. Singkatnya, ini adalah perpustakaan yang dikirimkan dengan alat verifikasi prosesor berbasis formal; dan dari sudut pandang teknisi verifikasi, ini terlihat seperti subset intuitif dari kode SVA yang sudah dikenal. Gambar 1 menunjukkan struktur generik:

instruksi properti_A; // status konseptual t ##0 ready_to_issue() dan // memicu t ##0 opcode==instr_A_opc menyiratkan // status konseptual t ##0 ready_to_issue() dan // keluaran antarmuka memori // membaca instruksi selanjutnya t ##0 imem_access(instr_A_opc) dan // memuat/menyimpan data t ##1 dmem_access(instr_A_opc) dan // register arsitektur t ##1 RF_update(instr_A_opc) dan t ##1 PC_update(instr_A_opc) endproperty 

Gambar 1: Struktur kode SVA Operasional menangkap spesifikasi instruksi prosesor. [1]

Mengacu pada gambar 1, sisi kiri dari implikasi (bagian dari kode atas kata kunci menyiratkan) mengidentifikasi kapan mesin siap mengeluarkan instruksi baru, dan instruksi dikeluarkan. Penegasan menangkap nilai-nilai saat ini dari keadaan arsitektur dan, di sisi kanan implikasi (bagian dari kode di bawah kata kunci menyiratkan), membuktikan nilai selanjutnya.

Selain itu, keluaran prosesor harus terbukti benar — dalam hal ini untuk memastikan bahwa instruksi mengakses data yang diharapkan dan lokasi memori instruksi. Penegasan tersebut juga membuktikan bahwa mesin siap mengeluarkan instruksi baru pada siklus berikutnya. Ini sangat penting untuk memisahkan verifikasi instruksi dari urutan instruksi yang bisa menjadi bagiannya. Misalnya, instruksi A dapat dijalankan dengan benar, tetapi membiarkan mesin dalam keadaan rusak. Keadaan yang salah ini dapat menyebabkan instruksi B berikutnya menghasilkan hasil yang salah bukan karena kesalahannya sendiri. Oleh karena itu, dengan pendekatan Operasional SVA, instruksi B yang memverifikasi pernyataan akan lulus, sementara instruksi A yang memverifikasi pernyataan akan gagal (di mana operasi memori baca dan tulis dapat bertahan beberapa siklus).

Intinya: fungsi yang mewakili keadaan arsitektur dalam kode Operasional SVA harus dipetakan ke sinyal implementasi dan harus mencerminkan mikroarsitektur prosesor. Status RF, misalnya, mungkin bergantung pada aktivasi jalur penerusan. [1]

[Catatan: Bagi Anda yang akrab dengan simulasi atau cakupan fungsional formal, gagasan kelengkapan ini tidak bergantung pada metrik cakupan struktural, atau pada pembuatan dan pengumpulan metrik untuk model cakupan fungsional. Alih-alih (dan sedikit lebih maju dari langkah dan hasil yang tersisa), hasil analisis di sini adalah tentang mendapatkan bukti lengkap untuk semua properti. Bukti lengkap juga secara implisit menunjukkan bahwa tidak ada fungsi lain — yang tidak ditentukan atau tidak terduga (bug spesifikasi atau kode), atau disisipkan dengan jahat — yang tidak ditangkap oleh kumpulan properti ini. Mengulangi, metodologi ini adalah tentang mencapai 100% "cakupan rencana pengujian" sebagaimana diverifikasi oleh hasil analisis formal yang lengkap — di mana tidak ada yang lebih "lengkap" daripada bukti matematis!]

Langkah 2 – Tentukan kendala input dan pemeriksaan yang akan dijalankan terhadap DUT

Untuk melengkapi properti spesifikasi untuk setiap instruksi, langkah selanjutnya adalah menentukan batasan input dan pemeriksaan output tambahan. Sekali lagi, SVA Operasional digunakan, di mana pengguna sekarang menentukan "rencana kelengkapan" untuk menentukan input legal dan pensinyalan ilegal yang harus diabaikan oleh DUT. Per contoh yang ditunjukkan pada gambar 2, ada tiga bagian: asumsi penentuan, persyaratan penentuan, dan grafik properti.

kelengkapan pengolah; determinasi_asumsi: // INPUT ditentukan(imem_data_i); ditentukan(dmem_valid_i); if (dmem_valid_i) defined(dmem_data_i) endif; determinasi_persyaratan: // OUTPUT ditentukan(imem_read_o), jika (imem_read_o) ditentukan(imem_addr_o) endif; ditentukan(dmem_enable_o); jika (dmem_enable_o) ditentukan(dmem_rd_wr_o), ditentukan(dmem_addr_o) endif; // NEGARA ARSITEKTUR ditentukan(PC); ditentukan(RF); property_graph: all_instructions := instruction_not_a, instruction_add_a, instruction_sub_a, [...] all_instructions -> all_instructions; kelengkapan akhir; 

Gambar 2: Contoh rencana kelengkapan dengan asumsi dan persyaratan penentuan kondisional.

Untuk menguraikan:

• "determination_assumptions" hanyalah nama keren untuk batasan nilai input
• "determination_requirements" adalah definisi dari sinyal yang harus diverifikasi (baik sinyal keluaran prosesor maupun status arsitektural)
• Bagian "property_graph" hanyalah pengikatan file ini ke semua properti yang dibuat pada Langkah 1

Merangkum di mana kita berada pada titik ini: pada Langkah 1 Anda membuat model DUT yang akurat secara siklus yang harus dibuktikan benar untuk semua waktu dan semua input; pada Langkah 2 Anda menetapkan batasan dan perilaku khusus apa pun yang harus diwaspadai. Tambahkan ini bersama-sama, dan efeknya Anda memiliki testbench formal yang siap dijalankan!

Langkah 3 – Jalankan analisis

Tujuan dari semua alat formal adalah untuk membuktikan secara mendalam bahwa semua properti benar untuk semua waktu dan semua masukan. Dalam kasus verifikasi prosesor RISC-V, alat ini berfungsi untuk membuktikan bahwa urutan masukan yang panjang dapat disesuaikan dengan urutan unik dari Operasional SVA yang ditentukan yang memprediksi nilai keluaran dan keadaan arsitektur.

Dan inilah yang sebenarnya terjadi. Jika ada perbedaan dalam perilaku yang terdeteksi antara spesifikasi dan DUT, alat formal memberikan bentuk gelombang "contoh tandingan" yang menunjukkan dengan tepat rangkaian sinyal input dan data yang dapat membuat pelanggaran terhadap spesifikasi. Seperti disinggung di atas, kegagalan tersebut dapat ditemukan di bagian dalam logika RTL instruksi atau dalam "logika handoff" yang mengatur cabang/instruksi legal berikutnya.

Either way, ketika masalah ini diperbaiki dan alat membuktikan semua properti, hasilnya benar-benar "lengkap" - yaitu, Anda dapat yakin secara matematis bahwa tidak ada kesalahan pengkodean RTL - analisis formal benar-benar membuktikan tidak adanya bug !

Hasil

Pertama, seperti disebutkan di atas, selama bertahun-tahun banyak pengembang prosesor telah mendapat manfaat dari aliran ini [2], [3], [4].

Menguji metodologi ini dengan RISC-V, rekan saya melakukan studi kasus menggunakan inti sumber terbuka Rocket Chip yang populer. Secara khusus, konfigurasi RV64IMAFDC – sv39 vm diperiksa. Ini adalah inti prosesor 64-bit dengan sistem memori virtual 39-bit [5] dan ekstensi, seperti instruksi terkompresi dan atom [6]. Implementasi RISC-V ISA open-source ini menggunakan pipeline lima tahap, single-issue, in-order dengan penyelesaian out-of-order untuk instruksi latensi panjang, seperti pembagian atau cache yang hilang. Inti juga mendukung prediksi cabang dan modifikasi runtime dari register "misa", memungkinkannya untuk mematikan ekstensi set instruksi tertentu.

Meskipun snapshot dari Rocket Chip ini telah diverifikasi secara ekstensif dan direkam beberapa kali, empat perilaku mencurigakan yang sebelumnya tidak diketahui, kasus sudut, diidentifikasi dan dilaporkan ke pengembang Rocket Core RTL. Isu-isu ini ([7], [8], [9], dan [10]) ditemukan semata-mata melalui penerapan sistematis dari pendekatan verifikasi formal lengkap yang diuraikan dalam artikel ini.

Menguraikan [10] secara khusus - penemuan instruksi non-standar CEASE (Opcode 0x30500073) di RTL: jelas tim Rocket Chip tertinggal dalam dokumentasi mereka (dan mereka memperbaikinya segera setelah mengajukan permintaan tarik GitHub). Poin yang lebih besar adalah bahwa ini menunjukkan bahwa logika yang diperlukan untuk mengimplementasikan seluruh instruksi - lusinan baris kode dan banyak gerbang logika yang disintesis, ditempatkan, dan diarahkan - dapat lolos dari deteksi dengan inspeksi visual, simulasi RTL, simulasi level gerbang, keseluruhan proses implementasi back-end, dan prototipe perangkat keras di lab!

Tapi bagaimana dengan kinerja aliran ini?

Pertama, mari kita bahas arti "kinerja" yang lebih luas. Karena sifat baru dari desain Rocket Chip, untuk studi kasus ini diperlukan sekitar 20 minggu teknik bagi praktisi verifikasi formal kami untuk mengembangkan seluruh testbench dan batasan. Namun, aplikasi sebelumnya dari aliran ini pada IP komersial yang lebih terstruktur biasanya menghabiskan sebagian kecil dari waktu ini. Secara alami, seluruh proses peningkatan akan berjalan jauh lebih cepat, semakin stabil dan matang spesifikasinya, seberapa baik didokumentasikan dan dapat dibaca kode DUT RTL, dan seberapa banyak akses yang Anda miliki ke insinyur desain untuk Tanya Jawab.

Setelah lingkungan disiapkan, waktu kerja jam dinding hanya 2 jam — yaitu, jauh lebih sedikit daripada yang dapat Anda harapkan dari simulasi RTL acak terbatas dan bahkan verifikasi dengan bantuan perangkat keras. Selain itu, ingatlah bahwa hasil analisis ini berlaku untuk semua input dan sepanjang waktu — singkatnya, hasil tersebut lengkap [11].

Kesimpulan

Pendekatan verifikasi prosesor berbasis formal lengkap yang disajikan dalam artikel ini menggunakan ekstensi ke IEEE SVA, Operational SVA, untuk memverifikasi secara formal bahwa RISC-V ISA bebas dari celah dan ketidakkonsistenan. Tidak seperti testbench simulasi acak terbatas, emulasi, atau pembuatan prototipe fisik, rangkaian lengkap properti dan batasan secara mendalam mendeteksi banyak jenis kesalahan RTL, serta adanya kode yang tidak terdokumentasi atau tidak ditentukan dengan baik dan Trojan berbahaya.

Referensi

1 – Konferensi GOMACTech 2019, Albuquerque, NM, 28 Maret 2019: Verifikasi Formal Lengkap IP Prosesor RISC-V untuk IC Tepercaya Bebas Trojan, David Landoll, et.al.

2 – DVCon 2007: Verifikasi Formal Lengkap TriCore2 dan Prosesor Lainnya, Infineon Gmbh.

3 - 51^st Design Automation Conference (DAC): Verifikasi Formal Diterapkan pada Platform Desain MCU Renesas Menggunakan Alat OneSpin

4 – DVCon Eropa 2019: Verifikasi Formal Lengkap Keluarga DSP Otomotif, Bosch Gmbh.

5 – Manual Set Instruksi RISC-V, Volume II: Arsitektur Istimewa, Versi Dokumen 1.10.

6 - https://github.com/freechipsproject/rocket-chip [diakses 20 Desember 2018]

7 – Hasil Instruksi DIV tidak Ditulis ke File Registrasi
https://github.com/freechipsproject/rocket-chip/issues/1752

8 – Instruksi JAL dan JALR Menyimpan PC Pengembalian yang Berbeda
https://github.com/freechipsproject/rocket-chip/issues/1757

9 – Opcode Ilegal Diputar Ulang dan Menyebabkan Efek Samping Tak Terduga
https://github.com/freechipsproject/rocket-chip/issues/1861

10 – Instruksi Non-standar CEASE (Opcode 0x30500073) Ditemukan di RTL, https://github.com/freechipsproject/rocket-chip/issues/1868

11 – Blog Verifikasi Cakrawala, Bagaimana Anda Dapat Mengatakan Bahwa Verifikasi Formal Lengkap?, Joe Hupcey III
https://blogs.sw.siemens.com/verificationhorizons/2021/09/16/how-can-you-say-that-formal-verification-is-exhaustive/

Sumber: https://semiengineering.com/do-you-know-for-sure-your-risc-v-rtl-doesnt-contain-any-surprises/