· selgitada verifitseerimise põhimõtteid ja vajalikkust;
· anda ülevaade digitaalsüsteemide verifitseerimise meetoditest;
· õpetada ekvivalentsuskontrolli läbiviimist otsustusdiagrammidel ja SAT-ülesandena;
· anda ülevaade koodikatte mõõtudest, parameetrite ja funktsionaalsest kattest;
· õpetada sümbolsimuleerimise aluseid ja selgitada selle rakendusi verifitseerimisel;
· anda ülevaade väidetest ja nende kasutamisest;
· õpetada mudelikontrolli tehnikat;
· anda ülevaade verifitseerimiskeeltest SystemVerilog ja PSL.

· to explain the basic principles of verification and provide motivation;
· to provide an overview about digital systems verification methods;
· to teach equivalence-checking techniques using decision diagrams and SAT-solving;
· to provide an overview about code coverage metrics, parameter and functional coverage;
· to teach the basics of symbolic simulation and explain its application in verification;
· to provide an overview about assertions and their use in verification;
· to teach model-checking techniques;
· to provide an overview of verification languages SystemVerilog and PSL;

Aine läbinud üliõpilane:
· oskab kodeerida verifitseeritavalt riistvarakirjelduskeeles;
· oskab rakendada erinevaid koodikatte mõõte;
· oskab kirjutada väiteid staatilise ja dünaamilise kontrolli tarvis;
· oskab rakendada ekvivalentsuskontrolli digitaalsüsteemidele.

Having finished the study of the subject a student :
· knows how to code hardware description languages for verifiability;
· knows how to apply different code coverage metrics in simulation-based verification;
· knows how to write assertions in static and dynamic verification;
· know show to apply equivalence-checking in digital systems verification.

Verifitseerimise põhimõtted, liigid. Ekvivalentsuskontroll, mudelikontroll, simuleerimine. Verifitseerimismeetodid. Simuleerimine versus formaalne verifitseerimine. Otsustusdiagrammid. Kehtestatavus e. SAT. Väited ja omaduste kontroll. Verifitseerimine koodikatte mõõte kasutades. Parameetrite kate ja funktsionaalne kate. Verifitseerimiskeeled: SystemVerilog, PSL. Kodeerimine verifitseeritavust silmas pidades. Probleemid riistvarakirjelduskeeltega.

The basic verification principle, types of verification. Equivalence-checking, model-checking, simulation. Verification methods. Simulation versus formal verification. Decision diagrams. Satisfiability (SAT). Assertions and property-checking. Verification using code coverage metrics, parameter coverage and functional coverage. Verification languages: SystemVerilog, PSL. Coding for verification. Problems with hardware description languages.

Teadmiste kontroll toimub suulisel arvestusel. Üliõpilasel peab arvestusele pääsemiseks olema seminaril esitatud referaat. Arvestusel vastab üliõpilane 2-3 teoreetilisele lühiküsimusele kogu kursuse temaatika piires.

The course ends with an oral evaluation. A written summary must be presented by the student at a seminar before the evaluation. At the evaluation, the student will answer to 2-3 short theoretical questions about topics of the entire course.

Iseseisev töö seisneb teoreetiliste materjalide läbitöötamises ja referaadi koostamises. Töö maht ca 50 tundi.

The independent work consists of reading scientific literature and preparing a written summary. The amount of work is approximately 50 hours.

Põhiõpik:
William K. Lam, Hardware Design Verification: Simulation and Formal Method-Based Approaches, Prentice Hall PTR, March 03, 2005, ISBN: 0-13-143347-4, Pages: 624.

-