V članku predstavljamo algoritme za avtomatsko generiranje testnih vzorcev, s pomočjo katerih pri sekvenčnih digitalnih vezjih odkrivamo zatične napake oziroma pokažemo, da zatičnih napak v danem primerku vezja ni. Vezje predstavimo kot končni avtomat. Za zatične napake generiramo lastnosti v obliki formul CTL, ki so veljavne v vezju z zatičnimi napakami in praviloma neveljavne v dobrem vezju. S simboličnim preverjanjem modelov preverimo veljavnost formul in za neveljavne formule skonstruiramo protiprimere, s katerimi vezje pripeljemo v stanja, ki dokažejo odsotnost zatičnih napak. Testni vzorci so sestavljeni tako, da izvajanje vezja vodijo po poti protiprimerov. Teoretične raziskave so podkrepljene z eksperimentalnimi rezultati. Prikazana je tudi analiza časovne in prostorske zahtevnosti.

Pravice

URN

URN:NBN:SI:DOC-DH1QX1KZ

COBISSID

7703318

Objavljeno

18.12.2015

Metapodatki

Citiranje

APA:

Časar, Aleš, Brezočnik, Zmago, Kapus, Tatjana (2002). Exploiting symbolic model checking for sensing stuck-at faults in digital circuits. Informacije MIDEM, letnik 32, številka 3, str. 171-180. URN:NBN:SI:DOC-DH1QX1KZ from http://www.dlib.si

MLA:

Časar, Aleš, Brezočnik, Zmago, Kapus, Tatjana. "Exploiting symbolic model checking for sensing stuck-at faults in digital circuits." Informacije MIDEM letnik 32. številka 3 (2002) str. 171-180.
<http://www.dlib.si/?URN=URN:NBN:SI:DOC-DH1QX1KZ>

Informacije MIDEM
1986-
(Zbirni zapis)

Exploiting symbolic model checking for sensing stuck-at faults in digital circuitsUporaba simboličnega preverjanja modelov pri zaznavanju zatičnih napak v digitalnih vezjih

Exploiting symbolic model checking for sensing stuck-at faults in digital circuits
Uporaba simboličnega preverjanja modelov pri zaznavanju zatičnih napak v digitalnih vezjih