Subject: Formal Methods for Hardware Verification (17 - EM405A)

Basic Information

Scientific or art field:Electronics
Course specification

Course is active from 12.10.2009..

Precondition courses

Course idMandatoryMandatory
Functional Hardware VerificationYesYes
This course aims to get students familiar with formal methods of specification and verification of hardware. Those are advanced skills needed for verification engineer.
After successful completion of this course, students will know theoretical fundamentals for specification and verification of hardware. They will be able to translate informal description of hardware to formal property specification. They will know to use EDA tools needed for formal verification of hardware.
Introduction to formal specification and verification of hardware: context, design of circuits, bugs and design cycle, formal verification vs simulation, test vectors, design-for-verification code style, assertion-based verification ABV, static (formal), semi-formal and dynamic (functional) verification approach, Languages for property specification (PSL, SVA), symbolic model checking, golden design, equivalence checking, verification base od Boolean functions, Binary Decision Diagrams (BDDs), verification based on Boolean satisfiability problem (SAT), bounded model checking, SAT solvers, SAT-BDD solvers, verification based on FSM, formal verification of hardware in higher-order logic (CTL, LTL), hardware description using temporal structures, logical formulas and specification, using formal EDA tools for verification of hardware.
Lectures. Computer labs. Consultations.
Thomas KropfIntroduction to Formal Hardware Verification1999SpringerEnglish
Christoph Meinel, Thorsten TheobaldAlgorithms and Data Structures in VLSI Design1998SpringerEnglish
Pallab DasguptaA Roadmap for Formal Property Verification2006SpringerEnglish
Eisner Cindy, Fisman DanaA Practical Introduction to PSL2006SpringerEnglish
Course activity Pre-examination ObligationsNumber of points
Complex exercisesYesYes20.00
Written part of the exam - tasks and theoryNoYes30.00
Project defenceYesYes50.00
Name and surnameForm of classes
Missing picture!

Vranjković Vuk
Associate Professor

Missing picture!

Dautović Staniša
Associate Professor

Missing picture!

Radovanović Boris
Assistant - Master

Laboratory classes