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.