694 KB32 KB198520252000Brezočnik, ZmagoČasar, AlešKapus, Tatjanaštevilka:3letnik:30str. 153-160ISSN:0352-9045COBISSID:5935638URN:URN:NBN:SI:doc-6NVC8Q5SenStrokovno društvo za mikroelektroniko, elektronske sestavne dele in materialeInformacije MIDEMalgoritmidigitalna vezjaodločitveni grafipreverjanjeverifikacijaFormal verification of digital circuits using symbolic model checking| Formalna verifikacija digitalnih vezij s simboličnim preverjanjem modelov|This paper presents efficient algorithms for digital circuit verification. The algorithms are based on symbolic CTL (Computation Tree Logic) model checking. We also present an extension of ordinary CTL with fairness constraints. They enable verification of circuits with symbolic model checkingregarding only fair paths in the computaion tree. The model checking algorithms were implemented as part of a fully hime-made program package for manipulating finite machine descriptions of digital circuits, represented with Boolean functions. The package is also based on a fully home-made program package for manipulating Boolean functions, represented with binary decision diagramsV članku predstavljamo učinkovite algoritme za verifikacijo digitalnih vezij. Algoritmi temeljijo na simboličnem oreverjanju modelov z logiko drevesa izvajanj ("Computational Tree Logic" - CTL). Prav tako predstavljamo razširitev navadnega CTL s poštenostnimi omejitvami, ki omogočajo verifikacijo vezij samo vzdolž poštenih poti v drevesu izvajanj. Algoritmi za preverjanje modelov so implementirani kot del povsem domačega programskega paketa za obdelavo opisov digitalnih vezij s končnimi avtomati, predstavljenihz logičnimi funkcijami, ki temelji na prav tako povsem domačem paketu za obdelavo logičnih funkcij, predstavljenih z binarnimi odločitvenimi grafiTEXTznanstveno časopisjejournalsSlovenian National E-content AggregatorNational and University Library of SloveniaStrokovno društvo za mikroelektroniko, elektronske sestavne dele in materiale