This course covers major formal specification and verification approaches used in the automation of digital design. Topics include the use of logic-based formalisms, formal verification of combinatorial circuit designs, symbolic model checking, specification and verification of synchronous and asynchronous sequential circuits, compositional verification, verification of complex hardware systems.