Verifikasi formal dalam VHDL menggunakan PSL

Saat mendesain VHDL untuk aplikasi FPGA yang kritis terhadap keamanan, menulis testbenches dengan upaya terbaik saja tidak cukup. Anda harus menunjukkan bukti bahwa modul berfungsi sebagaimana mestinya dan tanpa efek samping yang tidak diinginkan.

Teknik verifikasi formal dapat membantu Anda memetakan persyaratan ke pengujian, membuktikan bahwa modul VHDL Anda sesuai dengan spesifikasi. Ini adalah alat penting untuk memverifikasi aplikasi perawatan kesehatan atau mendapatkan sertifikasi DO-254 untuk solusi FPGA udara.

Untuk mengungkap verifikasi formal, VHDLwhiz meminta bantuan Michael Finn Jørgensen untuk menulis posting tamu ini. Michael memiliki pengalaman substansial dalam topik tersebut dan membagikan banyak kiat di halaman GitHub-nya.

Perangkat yang diuji dalam contoh artikel yang dapat diunduh ini berasal dari tutorial yang ada:
Cara membuat FIFO AXI di RAM blok menggunakan handshake yang siap/valid

Saya akan membiarkan Michael mengambil alih dari sini dan menjelaskan verifikasi formal kepada Anda di sisa entri blog ini.

Apa itu verifikasi formal?

Tujuan verifikasi formal (FV) adalah untuk memastikan modul Anda berfungsi sebagaimana mestinya!

FV adalah sesuatu yang Anda lakukan sebagai bagian dari proses pengembangan Anda sebelum Anda mensintesis modul Anda. Kadang-kadang disebut “Pemeriksaan Properti”, yang menurut saya merupakan deskripsi yang lebih baik.

Di FV Anda menentukan properti modul Anda harus dimiliki, dan kemudian alat (disebut "Pemecah Kepuasan") akan membuktikan bahwa modul Anda memenuhi properti untuk semua kemungkinan urutan input .

Dengan kata lain, alat akan mencari transisi apa pun dari valid status (di mana semua properti terpenuhi) ke tidak valid negara (di mana satu atau lebih properti dilanggar). Jika tidak ada transisi seperti itu, yaitu tidak ada cara untuk beralih ke keadaan tidak valid, maka properti telah terbukti selalu terpenuhi.

Tantangan dalam FV adalah mengekspresikan properti modul Anda dalam bahasa yang dapat dipahami oleh alat ini.

Verifikasi formal adalah alternatif untuk testbenches yang ditulis secara manual. Tujuan dari verifikasi formal dan testbenches manual adalah untuk menghilangkan bug dari desain, tetapi verifikasi formal melakukan ini dengan memeriksa properti dan menghasilkan banyak testbenches yang berbeda secara otomatis.

Alat ini menggunakan dua metode berbeda:

Pemeriksaan Model Terikat (BMC) . Mulai dari reset dan memeriksa jumlah siklus clock yang tetap.
Bukti induksi . Mulai dari status valid yang berubah-ubah dan memverifikasi bahwa status berikutnya juga valid.

Bukti induksi lebih sulit untuk dipenuhi karena membutuhkan semua properti yang akan dinyatakan, sedangkan BMC dapat dijalankan hanya dengan beberapa properti dan tetap memberikan hasil yang bermanfaat.

Mengapa menggunakan verifikasi formal?

Verifikasi formal sangat bagus dalam menangkap bug yang sulit ditemukan! Itu karena verifikasi formal secara otomatis menelusuri seluruh ruang dari kemungkinan masukan.

Ini berbeda dengan penulisan testbench tradisional yang membutuhkan kerajinan tangan dari rangsangan. Praktis tidak mungkin untuk menjelajahi seluruh ruang keadaan menggunakan testbenches yang ditulis secara manual.

Selain itu, ketika verifikasi formal menemukan bug, itu akan menghasilkan bentuk gelombang yang sangat pendek yang menunjukkan bug dan melakukan ini jauh lebih cepat daripada saat menjalankan simulasi berdasarkan testbench yang ditulis secara manual. Bentuk gelombang pendek ini jauh lebih mudah untuk di-debug daripada bentuk gelombang yang sangat panjang yang biasanya muncul dari simulasi.

Namun, verifikasi formal bukanlah pengganti penulisan testbench. Menurut pengalaman saya, verifikasi formal sangat cocok untuk pengujian unit, sedangkan lebih baik melakukan pengujian integrasi menggunakan bangku tes yang dibuat dengan tangan. Itu karena waktu proses verifikasi formal meningkat secara eksponensial dengan ukuran modul.

Memang ada kurva belajar yang terkait dengan verifikasi formal, tetapi ini sepadan dengan waktu, dan saya harap posting blog ini membantu Anda mengatasi kurva belajar ini. Anda akan menyelesaikan desain Anda lebih cepat, dan akan ada lebih sedikit bug!

Cara menulis properti di PSL

Saat melakukan verifikasi formal, Anda harus mengekspresikan properti modul Anda menggunakan Bahasa Spesifikasi Properti (PSL). Properti biasanya terletak di file terpisah dengan akhiran .psl , dan file ini hanya digunakan selama verifikasi formal.

Di bagian ini, saya akan menjelaskan fitur utama bahasa PSL secara umum, dan di bagian selanjutnya, saya akan memberi Anda contoh spesifik.

Ada tiga pernyataan dalam PSL:

assert
assume
cover

Anda mungkin sudah familiar dengan kata kunci assert saat menulis bangku tes. Kata kunci yang sama ini juga digunakan di PSL, tetapi dengan sintaks yang sedikit berbeda. assert kata kunci digunakan untuk menjelaskan properti yang dijanjikan modul ini untuk selalu dipenuhi. Secara khusus, assert kata kunci diterapkan ke output dari modul, atau mungkin juga ke status internal.

assume kata kunci digunakan untuk menjelaskan persyaratan apa pun yang diterapkan modul ini pada input. Dengan kata lain, assume kata kunci diterapkan ke input ke dalam modul.

cover kata kunci digunakan untuk menggambarkan properti yang harus mungkin dicapai dalam beberapa cara.

Anda juga dapat menulis kode VHDL biasa dalam file PSL, termasuk deklarasi dan proses sinyal (baik sinkron maupun kombinatorial).

Baris pertama file PSL harus

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

Di sini ENTITY_NAME dan ARCHITECTURE_NAME lihat modul yang Anda verifikasi. INSTANCE_NAME bisa apa saja yang kamu suka. File harus diakhiri dengan kurung kurawal:} .

Baris berikutnya di .psl file harus:

default clock is rising_edge(clk);

Ini menghindari keharusan merujuk ke sinyal clock di setiap pernyataan properti.

Sintaks untuk assert dan assume pernyataannya adalah:

LABEL : assert always {PRECONDITION} |-&gt; {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-&gt; {POSTCONDITION}

Pernyataan ini berbunyi sebagai berikut:Jika PRECONDITION memegang (dalam setiap siklus jam) maka POSTCONDITION harus puas dalam sama siklus jam.

Ada bentuk lain yang umum digunakan:

LABEL : assert always {PRECONDITION} |=&gt; {POSTCONDITION}

Pernyataan ini berbunyi sebagai berikut:Jika PRECONDITION memegang (dalam setiap siklus jam) maka POSTCONDITION harus puas di berikutnya siklus jam.

Kedua bentuk tersebut digunakan secara ekstensif.

Di dalam PRE- dan POST-CONDITIONS , Anda dapat menggunakan kata kunci stable . Kata kunci ini berarti:Nilai dalam ini siklus jam sama dengan nilai di sebelumnya siklus jam.

Di dalam PRE- dan POST-CONDITIONS , Anda dapat menggunakan urutan juga, dengan menulis sebagai berikut:

{CONDITION_1 ; CONDITION_2}

Artinya CONDITION_1 harus puas dalam ini siklus jam dan CONDITION_2 harus puas pada berikutnya siklus jam.

Pernyataan sampul memiliki sintaks berikut:

LABEL : cover {CONDITION}

Kita akan melihat banyak contoh dari semua pernyataan ini dalam contoh yang berhasil nanti di blog ini.

Memasang alat yang diperlukan

Verifikasi formal didukung oleh vendor alat terkemuka, termasuk ModelSim. Sayangnya, ModelSim Edisi Pelajar TIDAK mendukung verifikasi formal. Memang, Anda mendapatkan kesalahan berikut:

Jadi untuk menggunakan ModelSim untuk verifikasi formal memerlukan lisensi berbayar.

Sebagai gantinya, ada alat sumber terbuka (gratis) yang memungkinkan Anda melakukan verifikasi formal. Di bagian ini, saya akan memandu Anda melalui proses penginstalan alat ini.

Panduan ini mengasumsikan Anda menjalankan platform Linux. Jika Anda menggunakan platform Windows, saya sarankan menggunakan Windows Subsystem for Linux (WSL). Panduan berikut diverifikasi menggunakan Ubuntu 20.04 LTS.

Prasyarat

Pertama, kita harus memperbarui sistem untuk mendapatkan patch terbaru:

sudo apt update
sudo apt upgrade

Kemudian kita harus menginstal beberapa paket pengembangan tambahan:

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 dkk.

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 dkk.

Ada binari pra-paket untuk GHDL, tetapi saya sarankan untuk mengunduh file sumber terbaru dan mengompilasinya sebagai berikut:

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

Bagian selanjutnya dari artikel ini memandu Anda dalam menerapkan verifikasi formal untuk proyek VHDL yang ada. Anda dapat mengunduh kode lengkap dengan memasukkan alamat email Anda pada formulir di bawah ini.

Contoh yang berhasil dengan verifikasi formal

Bagian berikut akan menjelaskan cara memverifikasi secara formal modul axi_fifo yang ditulis sebelumnya di blog ini.

Untuk memulai verifikasi formal, kita perlu bertanya pada diri sendiri, properti apa yang dimiliki FIFO? Saya telah mengidentifikasi empat kategori properti:

Penanganan reset:Bahwa modul bangun dalam keadaan terdefinisi dengan baik setelah reset.
Pensinyalan penuh dan kosong FIFO:Ini memverifikasi bahwa FIFO dengan benar menunjukkan kondisi penuh dan kosong.
Protokol AXI:Bahwa modul memenuhi persyaratan jabat tangan valid/siap AXI.
Pemesanan FIFO:Agar FIFO tidak menjatuhkan/menggandakan/mengurutkan ulang elemen yang melewatinya.

Saya akan membahas masing-masing properti berikut ini.

Setel ulang penanganan

Pertama, kami mendeklarasikan bahwa modul mengharapkan reset ditegaskan untuk satu siklus clock:

f_reset : assume {rst};

Perhatikan di sini tidak adanya kata kunci always . Tanpa always kata kunci, pernyataan hanya berlaku untuk siklus jam pertama.

Merupakan kebiasaan (dan sangat berguna) untuk memberi label pada setiap pernyataan formal. Saat menjalankan verifikasi formal, alat akan merujuk kembali ke label ini saat melaporkan kegagalan apa pun. Saya menggunakan konvensi sebelum semua label tersebut dengan f_ .

Kemudian kami menyatakan bahwa FIFO harus kosong setelah reset:

f_after_reset_valid : assert always {rst} |=&gt; {not out_valid};
f_after_reset_ready : assert always {rst} |=&gt; {in_ready};
f_after_reset_head  : assert always {rst} |=&gt; {count = 0};

Perhatikan bahwa dimungkinkan untuk merujuk internal sinyal dalam modul dan bukan hanya port. Di sini kami mereferensikan count , yang merupakan tingkat pengisian saat ini, yaitu jumlah elemen yang saat ini ada di FIFO. Itu mungkin karena kita mengacu pada nama arsitektur di baris pertama file PSL.

Sebagai alternatif, kami dapat memiliki proses terpisah dalam file PSL yang menghitung jumlah elemen yang masuk dan keluar dari FIFO. Meskipun itu lebih disukai, saya akan menggunakan sinyal hitungan internal untuk membuat posting blog ini singkat dan langsung ke intinya.

Pensinyalan penuh dan kosong FIFO

Cara sinyal AXI FIFO penuh dan kosong adalah dengan out_valid dan in_ready sinyal. out_valid sinyal ditegaskan setiap kali FIFO tidak kosong, dan in_ready sinyal ditegaskan setiap kali FIFO tidak penuh. Mari kita periksa properti ini:

f_empty : assert always {count = 0} |-&gt; {not out_valid};
f_full : assert always {count = ram_depth-1} |-&gt; {not in_ready};

Protokol AXI

Jabat tangan AXI yang valid/siap menyatakan bahwa transfer data hanya terjadi ketika keduanya valid dan ready ditegaskan secara bersamaan. Salah satu kesalahan umum saat bekerja dengan protokol ini adalah menyatakan valid (dan data yang menyertainya) dan tidak memeriksa siap. Dengan kata lain, jika valid ditegaskan dan ready tidak, maka valid harus tetap ditegaskan pada siklus jam berikutnya, dan data harus tetap tidak berubah. Itu berlaku untuk data yang masuk ke FIFO dan data yang keluar dari FIFO. Untuk data yang masuk ke FIFO, kami menggunakan assume kata kunci, dan untuk data yang keluar dari FIFO, kami menggunakan assert kata kunci.

f_in_data_stable : assume always
   {in_valid and not in_ready and not rst} |=&gt;
   {stable(in_valid) and stable(in_data)};

f_out_data_stable : assert always
   {out_valid and not out_ready and not rst} |=&gt;
   {stable(out_valid) and stable(out_data)};

Perhatikan di sini penggunaan stable kata kunci yang dikombinasikan dengan |=> operator. Pernyataan-pernyataan ini merujuk pada dua siklus clock yang berurutan. Pada siklus jam pertama, ia memeriksa apakah valid ditegaskan dan ready tidak ditegaskan. Kemudian pada siklus jam (detik) berikutnya (ditunjukkan dengan |=> operator), nilai valid dan data harus sama dengan siklus clock sebelumnya (yaitu yang pertama).

Kedua, untuk protokol AXI kami mengharuskan ready sinyal stabil. Artinya jika FIFO dapat menerima data (ready ditegaskan) tetapi tidak ada data yang dimasukkan (valid tidak ditegaskan), maka pada siklus jam berikutnya ready harus tetap ditegaskan.

f_out_ready_stable : assume always
   {out_ready and not out_valid and not rst} |=&gt;
   {stable(out_ready)};

f_in_ready_stable : assert always
   {in_ready and not in_valid and not rst} |=&gt;
   {stable(in_ready)};

Pemesanan FIFO

Properti penting lainnya dari FIFO adalah bahwa data tidak diduplikasi/dihapus/ditukar. Mengekspresikan properti ini di PSL cukup rumit, dan ini adalah bagian tersulit dari verifikasi formal ini. Mari kita telusuri properti ini selangkah demi selangkah dengan cermat.

Kita dapat mengatakan secara umum bahwa jika ada data D1 yang masuk ke FIFO sebelum data lain D2, maka pada sisi keluaran data yang sama D1 harus meninggalkan FIFO sebelum D2 masuk.

Untuk mengekspresikan ini dalam PSL kita memerlukan beberapa sinyal tambahan:f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 , dan f_sampled_out_d2 . Sinyal-sinyal ini dihapus saat reset dan ditegaskan setiap kali D1 atau D2 masuk atau keluar dari FIFO. Setelah ditegaskan, sinyal-sinyal ini tetap ditegaskan.

Jadi kami menyatakan properti pemesanan FIFO dalam dua bagian:Pertama asumsi bahwa sekali D2 masuk ke FIFO, maka D1 sudah masuk sebelumnya:

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |-&gt;
   {f_sampled_in_d1};

Dan kedua pernyataan bahwa sekali D2 meninggalkan FIFO, maka D1 sudah pergi sebelumnya:

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |-&gt;
   {f_sampled_out_d1};

Kita masih perlu mendeklarasikan dan mengisi sinyal sampling yang dirujuk di atas. Kami melakukan ini sebagai berikut untuk sinyal pengambilan sampel input:

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 &lt;= '1';
         end if;
         if in_data = f_value_d2 then
            f_sampled_in_d2 &lt;= '1';
         end if;
      end if;

      if out_valid then
         if out_data = f_value_d1 then
            f_sampled_out_d1 &lt;= '1';
         end if;
         if out_data = f_value_d2 then
            f_sampled_out_d2 &lt;= '1';
         end if;
      end if;

      if rst = '1' then
         f_sampled_in_d1  &lt;= '0';
         f_sampled_in_d2  &lt;= '0';
         f_sampled_out_d1 &lt;= '0';
         f_sampled_out_d2 &lt;= '0';
      end if;
   end if;
end process p_sampled;

Di sini kami merujuk dua sinyal lain, f_value_d1 dan f_value_d2 . Mereka berisi nilai data D1 dan D2. Sinyal ini dapat berisi sewenang-wenang nilai, dan ada cara khusus untuk menunjukkan ini ke alat verifikasi formal:

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;

anyconst atribut dikenali oleh alat verifikasi formal. Ini menunjukkan bahwa alat dapat memasukkan nilai konstan apa pun sebagai gantinya.

Dengan di atas, kami telah menentukan properti FIFO.

Menjalankan verifikasi formal

Sebelum kita benar-benar dapat menjalankan alat verifikasi formal, kita perlu menulis skrip kecil axi_fifo.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

Bagian [tasks] menyatakan bahwa kita ingin Bounded Model Checking. Bagian [options] menentukan bahwa BMC harus dijalankan selama 10 siklus clock. Standarnya adalah 20. Bagian [engines] memilih yang mana dari beberapa pemecah yang berbeda untuk digunakan. Mungkin ada perbedaan dalam kecepatan eksekusi mesin yang berbeda, tergantung pada desain khusus Anda. Untuk saat ini, biarkan nilai ini tidak berubah.

[script] bagian adalah bagian yang menarik. Di sini kami menentukan standar VHDL (2008), nilai generik, file yang akan diproses, dan nama entitas tingkat atas. Terakhir, [files] bagian berisi nama file lagi.

Dengan skrip ini siap, kita dapat menjalankan verifikasi formal yang sebenarnya menggunakan perintah ini:

sby --yosys &quot;;yosys -m ghdl&quot;; -f axi_fifo.sby

Menjalankan alat verifikasi formal diakhiri dengan pernyataan sederhana:

[axi_fifo_bmc] DONE (PASS, rc=0)

Dan itu hanya berarti bahwa semua properti yang telah kami tentukan dipenuhi dengan semua input arbitrer hingga 10 siklus clock. Meningkatkan kedalaman menyebabkan waktu eksekusi yang lebih lama untuk pemecah. Namun, perhatikan bahwa kedalaman lebih besar dari kedalaman FIFO, yang berarti bahwa BMC akan menghadapi situasi penuh FIFO untuk beberapa urutan input. Jika kami hanya memilih, katakanlah, 5 siklus clock, verifikasi formal tidak akan pernah menemukan FIFO penuh, dan tidak akan menangkap bug apa pun yang terkait dengan itu.

Dimungkinkan untuk membuktikan bahwa properti terpenuhi untuk semua siklus clock menggunakan Bukti Induksi. Namun, itu membutuhkan lebih banyak pekerjaan menulis properti. Tantangannya adalah sejauh ini, kami baru saja menulis beberapa properti. Tapi untuk induksi, kita perlu menentukan semua properti (atau setidaknya cukup banyak). Itu akan cukup memakan waktu, jadi sebagai gantinya, saya akan membahas strategi alternatif untuk meningkatkan kepercayaan diri kita.

Mutasi

Jadi sekarang kami telah menjelaskan beberapa properti yang axi_fifo modul harus memenuhi, dan alat kami dengan cepat mengonfirmasi properti tersebut, yaitu membuktikan bahwa mereka puas. Tapi kita mungkin masih memiliki perasaan tidak enak ini:Apakah kita yakin tidak ada bug? Sudahkah kita benar-benar menyatakan semua properti axi_fifo modul?

Untuk membantu menjawab pertanyaan-pertanyaan ini dan untuk lebih percaya diri dalam kelengkapan properti yang ditentukan, kita dapat menerapkan teknik yang disebut mutasi :Kami sengaja membuat perubahan kecil dalam implementasinya, yaitu dengan sengaja memperkenalkan bug, dan kemudian melihat apakah verifikasi formal akan menangkap bug tersebut!

Salah satu perubahan tersebut adalah dengan menghapus beberapa logika yang mengendalikan out_valid sinyal. Misalnya, kita dapat mengomentari tiga baris ini:

if count = 1 and read_while_write_p1 = '1' then
  out_valid_i &lt;= '0';
end if;

Saat kami menjalankan verifikasi formal, sekarang kami mendapatkan pesan yang gagal

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
Writing trace to VCD file: engine_0/trace.vcd

Menggunakan alat GTKwave kita dapat melihat bentuk gelombang yang menyertainya, dan tampilannya sebagai berikut:

Di sini kita melihat bahwa pada 40 ns, out_valid sinyal harus pergi ke nol, tapi tidak. Pernyataan yang gagal adalah pada 50 ns, di mana out_valid tetap tinggi, tetapi out_data perubahan sinyal, menunjukkan data duplikat. Data duplikat sebenarnya tidak dikirimkan dalam jejak khusus ini karena out_ready rendah pada 40 ns, tetapi verifikasi formal tetap mendeteksi bug.

Pernyataan sampul

Akhirnya, mari kita beralih ke aplikasi lain dari alat verifikasi formal:Pernyataan sampul. Tujuan dari pernyataan penutup adalah untuk memeriksa apakah ada urutan input yang memenuhi properti tertentu. Karena kita berurusan dengan FIFO, mari kita lihat apakah kita dapat mengisinya sepenuhnya dan kemudian mengosongkannya lagi. Hal ini dapat diungkapkan dalam satu pernyataan sampul:

f_full_to_empty : cover {
   rst = '1';
   rst = '0'[*];
   rst = '0' and count = ram_depth-1;
   rst = '0'[*];
   rst = '0' and count = 0};

Itu cukup membuat mulut penuh! Perhatikan titik koma di dalam {} . Untuk keterbacaan, saya telah menempatkan setiap bagian pada baris terpisah. Pernyataan penutup ini berbunyi sebagai berikut:Cari urutan input yang memenuhi:

Reset dinyatakan untuk satu siklus clock.
Sejumlah siklus clock (di mana reset tidak dinyatakan) kemudian dapat berlalu.
Satu siklus clock di mana reset tidak dilakukan dan FIFO penuh.
Sejumlah siklus clock (di mana reset tidak dinyatakan) kemudian dapat berlalu.
Satu siklus clock di mana reset tidak dilakukan dan FIFO kosong.

Jadi sintaks [*] berarti mengulang (nol kali atau lebih) kondisi sebelumnya. Pada baris 3, kita bisa saja menghilangkan kondisi rst = '0' di depan [*] . Hasilnya akan sama. Alasannya adalah pemeriksa formal akan mencoba menemukan terpendek urutan yang memenuhi pernyataan sampul, dan menyatakan reset saat mengisi FIFO hanya akan menunda itu. Namun, saat mengosongkan FIFO di baris 5, reset tidak perlu dilakukan.

Untuk menjalankan verifier formal sekarang, kita harus membuat sedikit modifikasi pada script axi_fifo.sby . Ganti bagian atas dengan yang berikut:

[tasks]
bmc
cover

[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover

Sekarang solver akan menjalankan BMC dan kemudian menjalankan analisis penutup. Di output Anda akan melihat dua baris ini:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
Writing trace to VCD file: engine_0/trace5.vcd

Ini berarti bahwa pernyataan penutup memang dapat dipenuhi dengan urutan 15 siklus clock, dan pemecah telah menghasilkan bentuk gelombang khusus untuk pernyataan penutup ini:

Di sini kita melihat pada 80 ns FIFO penuh dan in_ready ditegaskan kembali. Dan pada 150 ns FIFO kosong dan out_valid ditegaskan kembali. Perhatikan bagaimana selama periode 30 ns sampai 80 ns itu out_ready dipertahankan rendah. Itu diperlukan untuk memastikan FIFO terisi.

Jika kita mengganti kondisi count = ram_depth-1 dengan count = ram_depth , pernyataan penutup tidak dapat dipenuhi. Alat tersebut kemudian melaporkan kesalahan.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

Jadi pesan kesalahan berisi label pernyataan sampul yang gagal. Itulah salah satu alasan mengapa label sangat berguna! Kami menafsirkan kesalahan di atas sebagai menyatakan bahwa FIFO tidak pernah dapat menampung ram_depth jumlah elemen. Ini persis seperti yang dinyatakan dalam posting blog AXI FIFO asli.

Ke mana harus pergi dari sini

Pendahulu bahasa PSL
Pengantar Verifikasi Formal
Serangkaian video kecil untuk memulai verifikasi formal
Blog yang terkait dengan verifikasi formal
Serangkaian artikel dengan topik lebih lanjut dalam verifikasi formal
Kumpulan contoh kecil menggunakan verifikasi formal

Memulai dengan VUnit Menggunakan Integrated Logic Analyzer (ILA) dan Virtual Input/Output (VIO)

VHDL