In this chapter we defined design verification as the process of ensuring that a design meets its specifications—the reverse of the design process. We discussed the general verification principle through redundancy, and simulation-based and formal verification methodologies, and then illustrated typical flows of these two methodologies. We then contrasted simulation and formal verification, and emphasized their input- and output-oriented nature. We viewed simulation-based verification as operating on a point basis whereas formal verification operates on a subspace basis. Next, we listed some limitations of formal verification—in particular, the inability to detect errors in the specification, incomplete functional coverage caused by verifying subcircuits, user errors, and software bugs in the verification tool. As a refresher of Verilog, we reviewed scheduling and execution semantics, during which we discussed the concurrent nature of the Verilog language and its inherent nondeterminism.