12 / 37 · Konsep

Verifikasi MUX: pengujian menyeluruh dan properti

Periksa cakupan masukan kombinasional dan penyimpanan secara terpisah, lalu minimalkan contoh penyangkal.

Apa arti hasil yang benar?

Masukan satu bit a, b, dan sel memiliki delapan kombinasi; memeriksa semuanya efisien. Untuk MUX^{Multiplekser Rangkaian kombinasional yang menghubungkan satu dari beberapa masukan ke keluaran menurut seleksi. Hubungan bit seleksi dan nomor masukan harus ditetapkan. Selengkapnya} lebar W, seluruh masukan termasuk seleksi berjumlah $2^{2W+1}$ kasus, sehingga lebar yang sedikit lebih besar segera membutuhkan strategi lain.

Aturan pemilihan setiap bit keluaran lebar W adalah:

\forall i\in\{0,\ldots,W-1\},\quad y_i=\overline s a_i+s b_i

Pilih stimulus sesuai cacat yang dicari

Cacat	Masukan atau pengamatan berguna
a/b tertukar	Data berbeda, bandingkan sel=0 dan sel=1
Urutan bit terbalik	Pola walking-one dengan satu bit 1
Bit stuck-at	Semua 0, semua 1, bit berselang-seling
Tepi penyimpanan salah	Ubah masukan di antara tepi dan periksa q bertahan
Selisih satu siklus	Buat nilai harapan berbeda pada tepi berurutan

Banyaknya pengujian saja tidak cukup; jelaskan cacat yang ingin dideteksi.

Perbandingan berikut hanya memilih a≠b. Setiap kolom satu vektor; seleksi salah memberi nilai kebalikan expected pada keempat kasus.

Empat kombinasi untuk menemukan seleksi terbalik

Lihat data gelombang

Data gelombang: setiap karakter mewakili satu interval; titik mempertahankan keadaan sebelumnya; p adalah satu siklus clock.
Sinyal	Gelombang	Nilai bus
a	`0.1.`
b	`1.0.`
sel	`0101`
expected	`01.0`
cacat terbalik	`10.1`

Acuan independen dari implementasi

Menyalin kode DUT dapat menyalin kesalahannya. Bentuk nilai harapan dari tabel kebenaran^{Tabel kebenaran Tabel seluruh kombinasi masukan beserta keluarannya. Perubahan terhadap waktu diperiksa terpisah melalui gelombang. Selengkapnya} atau seleksi indeks, dan lacak keadaan tangkapan q sebelumnya secara terpisah. Jika terjadi mismatch, ringkas menjadi urutan terpendek yang tetap gagal lalu jelaskan penyebabnya.

Alih-alih hanya keadaan akhir, catat masukan, hasil nyata, dan harapan di setiap pengamatan. Bukti ini membedakan “simulasi berjalan” dari “spesifikasi terpenuhi”.

Coba sendiri

MUX delapan bit diuji pada kedua seleksi hanya dengan a=0x00 dan b=0xFF. Apakah ini mendeteksi pembalikan urutan bit keluaran?

Baca penjelasan

Tidak. Membalik urutan bit tidak mengubah 0x00 atau 0xFF. Gunakan pola yang menunjukkan posisi seperti 0x01 dan 0x02, lalu bandingkan setiap bit keluaran.