Menguasai Verifikasi Formal Modul VHDL dengan PSL
Saat mendesain VHDL untuk aplikasi FPGA yang krusial keamanan, cukup menulis testbench tidak cukup. Insinyur harus membuktikan bahwa modul berperilaku tepat seperti yang ditentukan, bebas dari efek samping tersembunyi. Verifikasi formal memberikan jaminan matematis itu.
Verifikasi formal membatasi kesenjangan antara persyaratan dan implementasi dengan membuktikan bahwa setiap urutan input yang mungkin memenuhi properti desain. Ini tak tergantikan untuk mengsertifikasi perangkat medis, sistem penerbangan, atau domain manakah di mana sertifikasi DO‑254 diperlukan.
Dalam tulisan tamu ini, Michael Finn Jørgensen—praktisi verifikasi formal yang berpengalaman—membagikan wawasan praktis dan tips yang dapat ditindaklanjuti. Contoh di bawah ini membangun pada tutorial AXI FIFO yang familiar How to make an AXI FIFO in block RAM using the ready/valid handshake dan menunjukkan cara menerapkan PSL ke desain VHDL nyata.
Verifikasi formal (FV) adalah metode sistematis pra-sintesis yang menjamin kebenaran desain untuk semua kombinasi input. Berbeda dengan testbench konvensional yang bergantung pada stimulus yang dibuat secara manual, FV menentukan properti yang harus berlaku pada setiap siklus clock. Sebuah SAT solver kemudian secara ekslusif membuktikan bahwa properti-properti ini terpenuhi—atau mengidentifikasi contoh kontra jika tidak.
Dua teknik inti yang mendorong FV:
- Bounded Model Checking (BMC) – memeriksa sejumlah siklus terbatas, mulai dari reset.
- Induction Proof – memverifikasi bahwa jika suatu status valid, semua status berikutnya tetap valid. Ini memerlukan serangkaian properti yang lengkap tetapi menghasilkan jaminan untuk sejumlah siklus tak terbatas.
Karena BMC dapat dijalankan dengan hanya beberapa properti, seringkali menjadi garis pertahanan pertama. Induksi, sementara lebih menuntut, memberikan kepastian mutlak.
FV unggul dalam mengungkap bug yang sulit ditemukan karena menjelajahi seluruh ruang input secara otomatis. Ketika kesalahan ditemukan, alat menghasilkan gelombang ringkas yang menunjukkan siklus tepat tempat properti dilanggar—lebih mudah untuk di-debug daripada jejak simulasi yang panjang.
Meskipun FV adalah alat pengujian unit yang kuat, ini tidak menggantikan pengujian integrasi yang dibuat secara tangan. Saat ukuran modul bertambah, waktu runtime solver bisa menjadi menghalangi. Meskipun demikian, menginvestasikan waktu dalam FV mengurangi usaha debug keseluruhan dan mempercepat waktu ke pasar.
Menulis Properti dalam PSL
PSL (Property Specification Language) adalah bahasa franca verifikasi formal dalam VHDL. Properti biasanya disimpan dalam file terpisah .psl yang dibaca oleh solver selama fase verifikasi.
Tiga kata kunci PSL menggambarkan properti:
assert – menjamin bahwa suatu kondisi akan selalu berlaku.assume – menyatakan asumsi tentang input.cover – memeriksa apakah skenario tertentu dapat terjadi.
File PSL juga dapat berisi deklarasi dan proses VHDL biasa, yang memungkinkan Anda membuat sinyal tambahan untuk pernyataan kompleks.
Setiap file PSL dimulai dengan blok vunit yang mengaitkan file dengan entitas tertentu:
vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { } Diikuti oleh deklarasi clock default:
default clock is rising_edge(clk);
Sintaks properti terlihat seperti ini:
LABEL : assert always {PRECONDITION} |-> {POSTCONDITION} LABEL : assume always {PRECONDITION} |-> {POSTCONDITION} Gunakan |=> untuk pernyataan siklus berikutnya:
LABEL : assert always {PRECONDITION} |=> {POSTCONDITION} Di dalam kondisi, Anda dapat menggunakan stable untuk memberlakukan bahwa sinyal tidak berubah di antara siklus, dan Anda dapat merantai kondisi menggunakan {C1; C2} untuk mengekspresikan batasan berurutan.
Alat komersial terkemuka (misalnya, ModelSim) mendukung verifikasi formal, tetapi Edisi Gratis untuk Pelajar tidak memiliki fitur ini. Untungnya, stack open-source yang kuat tersedia untuk Linux (dan melalui WSL di Windows). Panduan berikut menggunakan Ubuntu 20.04 LTS tetapi berfungsi pada distribusi Debian‑based terbaru lainnya.
Prasyarat
sudo apt update && sudo apt upgrade
Instal pustaka pengembangan penting:
sudo apt install build-essential clang bison flex libreadline-dev \ gawk tcl-dev libffi-dev git mercurial graphviz \ xdot pkg-config python python3 libftdi-dev gperf \ libboost-program-options-dev autoconf libgmp-dev \ cmake gnat gtkwave
Yosys dan SymbiYosys
git clone https://github.com/YosysHQ/yosys cd yosys make sudo make install cd .. git clone https://github.com/YosysHQ/SymbiYosys cd SymbiYosys sudo make install cd .. git clone https://github.com/SRI-CSL/yices2 cd yices2 autoconf ./configure make sudo make install cd ..
GHDL dan Plugin Yosys
git clone https://github.com/ghdl/ghdl cd ghdl ./configure --prefix=/usr/local make sudo make install cd .. git clone https://github.com/ghdl/ghdl-yosys-plugin cd ghdl-yosys-plugin make sudo make install cd ..
Unduh Proyek Contoh
Isi formulir di bawah ini untuk menerima arsip ZIP yang berisi sumber AXI FIFO lengkap, file PSL, dan skrip verifikasi.
Di bawah ini kami merinci kategori properti utama untuk FIFO dan mengilustrasikan cara mengenkodekannya dalam PSL.
Penanganan Reset
f_reset : assume {rst}; Karena kata kunci always dihilangkan, asumsi ini hanya berlaku untuk siklus pertama setelah reset. Konvensi label (f_) membantu mengidentifikasi kegagalan.
f_after_reset_valid : assert always {rst} |=> {not out_valid}; f_after_reset_ready : assert always {rst} |=> {in_ready}; f_after_reset_head : assert always {rst} |=> {count = 0}; Perhatikan bahwa sinyal internal seperti count dapat dirujuk karena deklarasi vunit mencakup nama arsitektur.
Sinyal Penuh dan Kosong FIFO
f_empty : assert always {count = 0} |-> {not out_valid}; f_full : assert always {count = ram_depth-1} |-> {not in_ready}; Kepatuhan Protokol AXI
f_in_data_stable : assume always {in_valid and not in_ready and not rst} |=> {stable(in_valid) and stable(in_data)}; f_out_data_stable : assert always {out_valid and not out_ready and not rst} |=> {stable(out_valid) and stable(out_data)}; Untuk stabilitas sinyal ready:
f_out_ready_stable : assume always {out_ready and not out_valid and not rst} |=> {stable(out_ready)}; f_in_ready_stable : assert always {in_ready and not in_valid and not rst} |=> {stable(in_ready)}; Urutan FIFO
Jaminan urutan memastikan tulisan lebih awal keluar sebelum tulisan lebih akhir. Kami memodelkan ini dengan sinyal tambahan yang mengingat saat nilai data tertentu masuk atau keluar.
signal f_sampled_in_d1 : std_logic := '0'; signal f_sampled_in_d2 : std_logic := '0'; p_sampled : process (clk) begin if rising_edge(clk) then if in_valid then if in_data = f_value_d1 then f_sampled_in_d1 <= '1'; end if; if in_data = f_value_d2 then f_sampled_in_d2 <= '1'; end if; end if; if out_valid then if out_data = f_value_d1 then f_sampled_out_d1 <= '1'; end if; if out_data = f_value_d2 then f_sampled_out_d2 <= '1'; end if; end if; if rst = '1' then f_sampled_in_d1 <= '0'; f_sampled_in_d2 <= '0'; f_sampled_out_d1 <= '0'; f_sampled_out_d2 <= '0'; end if; end if; end process p_sampled;
Deklarasikan nilai data sebagai konstan tidak terbatas sehingga solver dapat memilih pola bit apa pun:
signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0); signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0); attribute anyconst : boolean; attribute anyconst of f_value_d1 : signal is true; attribute anyconst of f_value_d2 : signal is true;
Terakhir, enkode batasan urutan:
f_fifo_ordering_in : assume always {f_sampled_in_d2} |-> {f_sampled_in_d1}; f_fifo_ordering_out : assert always {f_sampled_out_d2} |-> {f_sampled_out_d1}; Buat skrip axi_fifo.sby untuk alat sby:
[tasks] bmc [options] bmc: mode bmc bmc: depth 10 [engines] smtbmc [script] ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo prep -top axi_fifo [files] axi_fifo.psl axi_fifo.vhd
Jalankan verifikasi:
sby --yosys ";yosys -m ghdl" -f axi_fifo.sby
Jalankan yang berhasil mencetak:
[axi_fifo_bmc] DONE (PASS, rc=0)
Menyesuaikan depth melebihi kedalaman FIFO memastikan solver menjelajahi skenario kapasitas penuh.
Pengujian Mutasi
Untuk mengukur kelengkapan serangkaian properti Anda, sengaja suntikkan bug kecil—seperti menghapus logika yang mendorong out_valid—dan jalankan kembali FV. Jika solver melaporkan kegagalan pernyataan, Anda telah memverifikasi bahwa properti Anda cukup ekspresif untuk menangkap kesalahan itu.
Contoh pesan kegagalan:
Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
Buka trace.vcd yang dihasilkan di GTKWave untuk menunjukkan siklus tepat tempat properti dilanggar.
Pernyataan Cover
Pernyataan cover berguna untuk menyatakan bahwa skenario tertentu dapat tercapai. Misalnya, untuk memverifikasi bahwa FIFO dapat diisi dan kemudian dikosongkan:
f_full_to_empty : cover { rst = '1'; rst = '0'[*]; rst = '0' and count = ram_depth-1; rst = '0'[*]; rst = '0' and count = 0}; Sesuaikan skrip sby untuk menyertakan tugas cover:
[tasks] bmc cover [options] bmc: mode bmc bmc: depth 10 cover: mode cover
Cakupan yang berhasil menghasilkan:
Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
Mengubah count = ram_depth-1 menjadi count = ram_depth akan membuat cover tidak tercapai, menunjukkan sensitivitas alat terhadap akurasi properti.
Langkah Selanjutnya
