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.