937 KB44 KB198520252002Brezočnik, ZmagoČasar, AlešKapus, Tatjanaštevilka:3letnik:32str. 171-180ISSN:0352-9045COBISSID:7703318URN:URN:NBN:SI:doc-DH1QX1KZenStrokovno društvo za mikroelektroniko, elektronske sestavne dele in materialeInformacije MIDEMdigitalna vezjatestiranjezatične napakeExploiting symbolic model checking for sensing stuck-at faults in digital circuits| Uporaba simboličnega preverjanja modelov pri zaznavanju zatičnih napak v digitalnih vezjih|This paper presents algorithms for automatic test pattern generation for discovering stuck-at faults in sequential digital circuits or proving that there are no stuck-at faults in the given circuit. A circuit is represented as a finite state machine. Properties for stuck-at faults expressed with CTL formulas which are valid in the circuit with stuck-at faults and generally not valid in the good circuit are generated. Validity of the formulas is checked by symbolic model checking, and for invalid formulas counterexamples are constructed which guide the circuit to the states which prove the absence of stuck-at faults. Test patterns guide the circuits exactly as the counterexamples. Experimental results for a set of benchmark circuits togetherwith the time and space complexity analysis of the algorithms are also givenV č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 zahtevnostiTEXTznanstveno časopisjejournalsSlovenian National E-content AggregatorNational and University Library of SloveniaStrokovno društvo za mikroelektroniko, elektronske sestavne dele in materiale