This course introduces the formal verification and testing methods for digital systems, which includes both software and digital hardware. In the first part of the course, formal testing based on finite state machine representation of digital systems is studied. Black box and white box testing methods are also covered. In the second part of the course, model checking is introduced as a formal approach for verification. The practical problems of model checking, and some complexity relief techniques are also discussed.