Introduction to the formal specification and verification of hardware: the context, design of circuits, errors and cycle of design. Formal verification, simulations, test vectors, test-benches, design-for-test and design-for-verification styles of writing code and verification based on assertion (assertion-based verification, ABV). Formal (static), semi-formal and informal (dynamic, functional) approach to verification. Hardware verification languages (HVLs). Properties specification languages (PSLs). Formal properties of hardware description languages (FPLs). Symbolic model checking, golden design, logical equivalence. Approaches to verification based on Boolean functions. Representations of Boolean functions using binary decision diagrams (BDD). Extensions and variants of BDDs. Approaches to verification based on the satisfiability problem (SAT), limited model checking (BMC), symbolic trajectory estimation (STE), solvers of SAT problems, combined SAT-BDD checkers. Approaches to verification based on finite state machines (FSM). The formal verification of hardware in higher order logic (PTL, CTL, LTL). Descriptions of hardware using temporal structures, logical formulas and specifications. Probabilistic model checking.