Formal verification of digital circuits using symbolic model checking - Časar, Aleš (Informacije MIDEM, 2000)
V č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 grafi.
Keywords: algoritmi; digitalna vezja; odločitveni grafi; preverjanje; verifikacija