Geekly articles weekly

Verifikasi sirkuit digital. Ulasan

gambar


Saya akan mencoba berbicara secara umum tentang verifikasi sirkuit digital.


Verifikasi di bidang ini adalah proses penting yang membutuhkan keterlibatan insinyur berpengalaman. Misalnya, spesialis verifikasi yang bekerja pada sistem dengan CPU, sebagai aturan, harus memiliki bahasa scripting dan bahasa shell perintah (Tcl, bash, Makefile, dll.), Bahasa pemrograman (C, C ++, assembler), HDL / HDVL (SystemVerilog [10, Lampiran C - Sejarah Bahasa] [11], Verilog, VHDL), metodologi dan kerangka kerja modern (UVM).


Proporsi waktu yang dihabiskan untuk verifikasi mencapai 70-80% dari total waktu proyek. Salah satu alasan utama untuk perhatian tersebut adalah bahwa Anda tidak dapat melepaskan "tambalan" ke chip setelah dimasukkan ke dalam produksi, Anda hanya dapat melepaskan "silikon errata" (ini tidak berlaku untuk proyek FPGA / FPGA).


Dengan sirkuit digital, maksud saya:


  • blok fungsional kompleks / properti intelektual (SFB / IP);
  • Chip khusus sirkuit khusus aplikasi (ASIC) khusus aplikasi
  • logika yang dapat diprogram sirkuit terpadu / field-programmable gate array (FPGA);
  • sistem pada chip / sistem pada kristal (SoC / SoC);
  • dll.

Masalah verifikasi aktual


Keadaan saat ini dan tren di bidang verifikasi dapat dinilai dengan tantangan dan masalah berikut yang dihadapinya [6]:


  • Ukuran objek verifikasi (OB) terus bertambah. Bahkan tipe IC mikrokontroler kecil adalah sekumpulan puluhan submodul, sangat sering dengan fungsi yang kompleks. IC besar adalah kompleks di mana mungkin ada hingga miliaran transistor, dan skema manajemen daya saja dapat melebihi beberapa prosesor dalam kompleksitas [8];
  • tidak mungkin untuk membuat spesifikasi untuk IMS pada awal proyek dan hanya mengikutinya di masa depan, itu terus berubah sepanjang proses pengembangan (pelanggan mengubah persyaratan, masalah teknis atau penemuan solusi yang lebih optimal memaksa kita untuk mempertimbangkan kembali pendekatan, dll). Berdasarkan hal ini, semua proses harus memahami dinamika perubahan spesifikasi dan dimodifikasi sesuai dengan persyaratan;
  • seringkali, beberapa tim yang terpisah satu sama lain mengerjakan verifikasi proyek, yang jumlahnya dapat mencapai puluhan orang;
  • jumlah tes individu dan jenisnya mencapai jumlah yang sangat besar, hasilnya harus dikumpulkan dan dianalisis;
  • pemodelan bahkan sistem digital memerlukan banyak waktu komputer;
  • kelengkapan target kesiapan yang ditetapkan untuk proyek sangat tergantung pada kompetensi dan intuisi spesialis verifikasi;
  • Terlepas dari adanya indikator cakupan proyek dengan tes (metrik), satu-satunya cara untuk menyelesaikan verifikasi adalah memutuskan untuk menangguhkannya, terutama berdasarkan pada kesimpulan berikut: uang atau waktu yang dihabiskan pada tahap proyek harus dimasukkan ke dalam produksi, sepertinya mereka mencapai cakupan kode 100 %, kami telah menguji selama seminggu dan belum menemukan kesalahan, dll.

Jenis Verifikasi


Verifikasi sirkuit digital dapat dibagi menjadi beberapa tipe utama berikut:


  1. fungsional (verifikasi fungsional) - nama berbicara sendiri, Anda memeriksa apakah sistem Anda menjalankan fungsinya dengan benar;
  2. verifikasi formal - dengan verifikasi ini, kesetaraan representasi sistem Anda pada berbagai tahapan rute desain atau pemenuhan pernyataan yang ditempatkan dalam kode sumber ditetapkan:
    • Pemeriksaan Kesetaraan (mis. RTL-ke-RTL, RTL-ke-Gerbang, Gerbang-ke-Gerbang);
    • Pemeriksaan Properti (Pemeriksaan Model) (memeriksa properti (pernyataan) yang ditentukan dalam kode menggunakan SVA (misalnya)).
  3. analisis kode statis - memeriksa kode sumber sesuai dengan kriteria formal untuk kepatuhan dengan aturan untuk menggunakan bahasa dan konstruksinya. Sangat sering, aturan verifikasi yang dikonfigurasi dikirim ke RMM [4]. Program untuk verifikasi semacam itu biasanya disebut dengan lint atau linter;
  4. verifikasi fisik - pada dasarnya menyiratkan pemeriksaan DRC, LVS, PERC, dll., representasi fisik sistem diperiksa untuk kesesuaian dengan standar teknologi dan kesesuaian representasi fisik dan logis, dll. Komposisi cek sangat bergantung pada teknologi. Biasanya, verifikasi fisik dilakukan oleh insinyur atau tim desain topologi.
  5. prototyping - penggunaan FPGA untuk verifikasi fungsional [18].

Verifikasi fungsional dalam lingkup semua pekerjaan paling signifikan dan membutuhkan keterlibatan manusia secara langsung.


Analisis kode statis hanya memerlukan konfigurasi awal alat, yang sesuai dengan aturan desain internal yang diadopsi oleh perusahaan, maka alat tersebut terlibat dalam fakta bahwa alat ini menyediakan "panduan berharga" bagi pengembang dan tidak memerlukan pengawasan terus-menerus.


Alat verifikasi formal seringkali juga sangat independen, hanya memerlukan analisis yang cermat atas laporan yang dihasilkannya. Mereka juga cocok untuk rekayasa terbalik, ketika karena alasan tertentu Anda tahu Anda harus mengembalikan kode dari daftar sirkuit.


Contoh Alat Verifikasi


Contoh alat verifikasi sirkuit digital (rute digital-on-top):


  • alat manajemen verifikasi
    • Grafik Mentor - Manajemen Verifikasi Questa
    • Irama - vManager
    • Sinopsis - Verdi, Manajer Eksekusi VC (“ExecMan”)
  • fungsional - biasanya simulator
    • Mentor Graphics - ModelSim, QuestaSim
    • Cadence - Incisive, Xcelium
    • Sinopsis - VCS
    • Perangkat lunak bebas dari pengembang independen - simulator Verilator, Icarus [5]
  • formal
    • Grafik Mentor - Pro Resmi, Verifikasi Formal Questa
    • Cadence - JasperGold, LEC Konformal, Platform Verifikasi Formal yang Tajam
    • Sinopsis - Formalitas, VC Formal
  • analisis kode statis
    • Mentor Graphics - Questa AutoCheck
    • Cadence - HAL, JasperGold
    • Synopsys - SpyGlass Lint
  • verifikasi fisik
    • Mentor Graphics - Calibre
    • Cadence - Pegasus, Sistem Verifikasi Fisik,
    • Sinopsis - Hercules, IC Validator

Metode Verifikasi Fungsional


Verifikasi fungsional - adalah serangkaian tes, saya akan secara kondisional membiarkan diri saya dibagi menjadi tiga kelompok (ini bukan dogma, ini dari pengalaman pribadi):


  1. Cabang positif - verifikasi perilaku dalam situasi normal, diatur oleh spesifikasi untuk perangkat atau standar, dll. Yaitu Kami memeriksa situasi ketika semuanya berjalan dengan baik.
  2. Cabang negatif - memeriksa penyimpangan dari situasi standar, tetapi dalam kerangka spesifikasi atau standar, misalnya - ketidakcocokan checksum, jumlah data yang diterima, dll. Yaitu ketika ada yang tidak beres, tetapi kami tahu bahwa ini bisa terjadi dan kami tahu cara bekerja dalam situasi ini.
  3. Situasi non-standar - segala situasi acak mulai dari pelanggaran protokol komunikasi, urutan data, hingga benturan fisik di antarmuka, perubahan acak dalam keadaan elemen logika, dll. Yaitu ini adalah saat apa pun bisa terjadi dan Anda perlu memastikan bahwa OB akan keluar setelah ini dalam kondisi kerja.

Dua tahap pertama dapat diotomatisasi menggunakan UVC / VIP (Komponen Verifikasi Universal / Verifikasi IP) dan cukup cepat di sana Anda dapat meningkatkan volume berbagai tes, termasuk yang dihasilkan secara otomatis. Tahap ketiga adalah "karya besar" dalam verifikasi, tahap ini membutuhkan pendekatan dan pengalaman yang luar biasa, sangat sulit untuk diotomatisasi, karena kebanyakan situasi adalah algoritma yang terpisah, mungkin skrip untuk CAD atau instruksi untuk pemeriksaan "manual".


Jenis metrik verifikasi fungsional


Metrik adalah indikator dari cakupan uji proyek. Mereka diperlukan untuk memahami tes lain apa yang perlu dikembangkan untuk memverifikasi situasi yang mungkin dan berapa banyak waktu yang diperlukan verifikasi [16].


Sayangnya, hanya satu jenis metrik yang dievaluasi berdasarkan kode sumber proyek, definisi kriteria untuk jenis yang tersisa adalah hasil karya intelektual.


Selain itu, harus diingat bahwa pencapaian indikator yang diinginkan oleh satu jenis metrik tidak berarti kemampuan kerja secara umum, selalu diperlukan untuk mengevaluasi kompleks.


Jenis metrik [3]:


  • lapisan fungsional . Menunjukkan seberapa banyak fungsi OB telah diuji. Kriteria untuk cakupan ini dapat ditentukan oleh rencana pengujian dan pengenalan konstruksi khusus (covergroup [1]) di lingkungan pengujian dan / atau OM, yang memantau apakah fungsi / tindakan ini atau itu dilakukan atau tidak, apakah data diubah dengan cara tertentu, dll. Informasi dari desain yang disematkan dalam kode sumber dapat dikumpulkan secara otomatis oleh CAD.
  • cakupan kode - mengubah status konstruksi kode sumber selama pengujian. Ia dikumpulkan secara otomatis oleh CAD, tidak memerlukan pengenalan struktur apa pun dalam kode sumber. Sebagai contoh:
    • switching register (Toggle Coverage);
    • aktivitas setiap baris kode (Line Coverage);
    • aktivitas ekspresi (Pernyataan Cakupan), pada kenyataannya - ini adalah Cakupan Line, tetapi dapat melacak ekspresi yang lebih dari satu baris di editor;
    • aktivitas segmen kode di dalam pernyataan atau prosedur bersyarat (Cakupan Blok), variasi dari Cakupan Pernyataan;
    • aktivitas semua cabang pernyataan bersyarat seperti jika, kasus, sementara, ulangi, selamanya, untuk, loop (Branch Coverage);
    • perubahan semua status (benar, salah) dari ekspresi logis komponen (Cakupan Ekspresi);
    • keadaan mesin negara (Cakupan Mesin Hingga-Status).
  • klaim menutupi . Pernyataan adalah konstruksi bahasa khusus yang melacak berbagai peristiwa dan urutan, dan menurut kriteria yang ditentukan menentukan legalitas kejadiannya.

Metode Verifikasi Fungsional


Metode Tes Langsung (DTM)


Tes langsung dan bermakna. Jika metode ini diadopsi dalam proyek, maka rencana verifikasi terdiri dari tes yang bertujuan untuk memeriksa perilaku bahan organik di tempat-tempat menarik tertentu (negara bagian). Memeriksa semua situasi yang mungkin terjadi, terutama dalam proyek yang kompleks, hampir tidak mungkin.
Pada saat yang sama, masalah yang mungkin timbul dalam situasi yang tidak tercakup oleh pengujian tidak terdeteksi sebelum perangkat mulai digunakan dalam kondisi nyata. Biasanya, tes ini menggunakan metrik cakupan fungsional.


Verifikasi Berbasis Drive, Verifikasi Berbasis Metrik (CDV, MDV) [17]


Konsep membuat tes yang bertujuan untuk mencapai "cakupan uji" tertentu dari zat organik. Mereka mengandalkan metrik untuk memahami tes apa yang perlu ditambahkan ke rencana verifikasi untuk mencapai target kesiapan proyek.
Anda perlu menggunakan alat analisis cakupan untuk melihat apa lagi yang akan ditambahkan ke rencana verifikasi. Bahkan, jika kita mulai menyesuaikan rencana verifikasi dalam DTM, dengan mengandalkan setidaknya pada "cakupan kode", maka kita sudah dapat berasumsi bahwa kita dengan lancar beralih dari DTM ke CDV.


Verifikasi Acak Terkendali (CRV)


Verifikasi dengan mengirimkan pengaruh acak. Ini adalah tes yang benar-benar otomatis dengan generasi efek acak pada OM, tetapi sulit membayangkannya tanpa simbiosis dengan ABV.
Metode ini sangat mahal pada awalnya, karena Butuh waktu lama untuk menyiapkan alat. Setelah tahap persiapan awal selesai, pengujian dapat dimulai secara otomatis, berulang kali dengan data awal yang berbeda. Jika ketidakcocokan pernyataan terdeteksi, tim pengembangan dan verifikasi mulai menganalisis kesalahan yang terdeteksi.
Dalam proyek nyata, seseorang tidak dapat membatasi diri hanya untuk metode ini, karena Dengan menggunakan metode ini, Anda dapat mengumpulkan cakupan kode dan cakupan pernyataan, dan mereka tidak dapat mengatakan apa-apa tentang operasi OS yang benar, yaitu. kesesuaian dengan spesifikasi. Itu harus dilengkapi dengan tes fungsional.
Untuk mengimplementasikan metodologi ini dibutuhkan:


  1. menerapkan "pernyataan" di semua poin penting dari kode sumber OB dan lingkungan pengujian;
  2. untuk mengembangkan generator dari efek dan skenario acak dari pekerjaan mereka, yaitu dampaknya acak, tetapi memiliki batasan jangkauan (kami tidak punya waktu untuk memilah-milah semuanya), urutan pengarsipan, dll.

Verifikasi Berbasis Pernyataan [9] (ABV)


Verifikasi dengan pernyataan. Mungkin, ini bahkan bukan metode independen, tetapi beberapa komponen atau komponen dasar di atas.


Masalah penting dengan ABV adalah bagaimana mendistribusikan pernyataan, mana yang paling baik ditempatkan dalam kode sumber OB, mana yang harus di lingkungan pengujian.


Harus segera dicatat bahwa bahasa Verilog tidak memiliki asersi dalam standarnya (mereka dapat dibuat menggunakan konstruksi bahasa dasar, tetapi arahan diperlukan untuk synthesizer sehingga tidak berurusan dengan konversi mereka). Pernyataan hanya muncul dalam standar SystemVerilog, dan mereka juga awalnya dalam standar bahasa VHDL dan e.


Saya menyarankan agar Anda membiasakan diri dengan rekomendasi para spesialis, termasuk Clifford Cummings [12, artikel tentang SVA] tentang distribusi karya pada tulisan mereka, serta materi tentang ABV di situs web Verification Academy [13].


Referensi


  1. IEEE Std 1800TM-2012. Standar IEEE untuk SystemVerilog - Desain Perangkat Keras, Spesifikasi, dan Bahasa Verifikasi
  2. Clive Maxfield. Desain FPGA. Arsitektur, alat dan metode. Kursus pejuang muda. ISBN 978-5-94120-147-1 (RUS), ISBN 0-7506-7604-3 (ENG)
  3. Akademi Verifikasi. Cakupan Cookbook. Cakupan uji pro
  4. Michael Keating, Pierre Bricaud. Gunakan kembali manual metodologi untuk desain sistem-pada-chip. Cetak ISBN 1-4020-7141-8, eBuku ISBN 0-306-47640-1
  5. Daftar CAD berlisensi dan didistribusikan secara gratis
  6. Grafik Mentor. Contoh statistik tentang kondisi saat ini dan ruang lingkup verifikasi
  7. WikiChip. Keripik Wikipedia
  8. Wikipedia Data umum tentang jumlah transistor di IC
  9. Harry Foster, Adam Krolnik, David Lacey. Desain berbasis pernyataan. Cetak ISBN 1-4020-8027-1, eBuku ISBN 1-4020-8028-X
  10. Stuart Sutherland, Simon Davidmann, Peter Flake. SystemVerilog untuk Desain. Cetak ISBN-10: 0-387-33399-1, eBuku ISBN-10: 0-387-36495-1
  11. Chris Spear, Greg Tumbush. SystemVerilog untuk Verifikasi. Cetak ISBN: 978-1-4614-0714-0, eBuku ISBN: 978-1-4614-0715-7
  12. Desain Sunburst. Makalah
  13. Akademi Verifikasi. Tentu saja ABV
  14. Doulos. Materi yang berguna on-line dan buku referensi
  15. Prakash Rashinkar, Peter Paterson, Leena Singh. Verifikasi chip sistem-on-a. metodologi dan teknik. Cetak ISBN: 0-792-37279-4, ISBN eBuku: 0-306-46995-2
  16. Akademi Verifikasi. Metrik dalam Verifikasi SoC
  17. Doulos. Metodologi verifikasi berdasarkan cakupan
  18. Doug Amos, Austin Lesea, Rene Richter. Manual Metodologi Prototip Berbasis FPGA: Praktik terbaik dalam Desain-untuk-Prototipe (FPMM). Cetak ISBN: 978-1617300042. Unduh secara gratis dari situs web Synopsys

Source: https://habr.com/ru/post/id481542/

More articles:


All Articles