25 / 37 · Konsep
Rencana verifikasi, cakupan, dan model acuan independen
Bedakan tes lolos dari kontrak terpenuhi dan masukkan batas, persilangan, serta contoh minimum.
Pelajaran dapat dibaca gratis. Daftar untuk menyimpan progres.
Mengubah spesifikasi menjadi klaim yang dapat diuji
Ganti “berfungsi baik” dengan keadaan setelah reset, keluaran normal, penahanan saat berhenti, penanganan masukan terlarang, atau waktu selesai. Hubungkan minimal satu tes dan titik pengamatan ke setiap klaim untuk menemukan kelalaian.
| Klaim | Stimulus | Pengamatan |
|---|---|---|
| Reset diprioritaskan | reset=enable=1 | Keadaan berikutnya nilai awal |
| Urutan terjaga | Pola asimetris kontinu | Nilai dan valid seluruh keluaran |
| Perputaran tepat | Sekitar maksimum | M−1→0, tanpa nilai di luar rentang |
| Bertahan saat berhenti | Masukan berubah, accept=0 | Keadaan tetap |
| Pola bertumpang tindih | 10101 | Deteksi pada masukan diterima ke-3 dan ke-5 |
Mengapa acuan independen?
Menyalin sliceSlice Pemilihan rentang bit berurutan pada vektor. Rentang pilihan menentukan lebar dan urutan bit hasil. Selengkapnya RTL geser yang sama dapat menyalin kesalahan indeks. Formulasi berbeda seperti perkalian/modulo atau pembandingan sufiks string membantu pemeriksaan silang. Bentuk berbeda tidak otomatis membuktikan independensi; periksa kasus kecil secara manual.
Cakupan bukan jumlah tes yang lolos
Semua baris kode dieksekusi tidak berarti semua kondisi fungsi diuji. Persilangan reset×enable, state×input, atau full×push×pop dapat mengungkap kesalahan. Lengkapi tes acak dengan tes terarah untuk kombinasi langka dan penting.
Rangkaian kombinasional N masukan memiliki kasus, tetapi rangkaian sekuensial juga memiliki urutan waktu. Analisis keterjangkauan keadaan dan invarianInvarian Kondisi yang harus selalu benar pada setiap eksekusi yang diizinkan. Misalnya, okupansi FIFO kedalaman 4 selalu berada antara 0 dan 4. setiap transisi. Simulasi terbatas yang lolos bukan bukti matematis untuk waktu tak terbatas.
Hitung harapan secara independen dari kontrak. Ketika gagal, simpan masukan dan keadaan sebelumnya juga, bukan hanya keluaran nyata.
- Spesifikasi dan stimulus: Pilih batas dan kombinasi kondisi
- Model acuan independen: Hitung nilai harapan dan saat validnya
- Bandingkan dengan DUT: Bandingkan pada saat pengamatan yang sama
- Catat ketidakcocokan pertama: Simpan contoh tandingan minimal dan seed
Perkecil dan catat kegagalan
Simpan keadaan lama, masukan, harapan, dan hasil nyata pada mismatch pertama. Hapus stimulus yang tidak perlu sampai diperoleh contoh minimum, lalu perbaiki. Jalankan kembali pemeriksaan batas dan resetReset Kontrol yang mengembalikan keadaan ke nilai awal tertentu. Sifat sinkron/asinkron dan prioritas terhadap kontrol lain harus ditetapkan. Selengkapnya lama juga, bukan hanya tes yang diubah.
Coba sendiri
Cakupan RTL 100% dan 10.000 tes acak lolos, tetapi reset dan enable tidak pernah 1 bersamaan. Apa yang harus ditambahkan?
Baca penjelasan
Periksa kombinasi itu dalam kontrak dan tambahkan tes terarah dari keadaan bukan nol untuk memperlihatkan prioritas. Cakupan kode dan jumlah tes tidak menggantikan verifikasi kondisi fungsi tertentu.