Ensuring functional correctness on RTL designs continues to pose one of the greatest challenges for today's ASIC and SoC design teams. Rooted in that challenge is the goal to shorten the verification cycle. This requires new design and verification techniques. In this book, we address the functional correctness challenge within a contemporary verification flow that relies on an assertion-based methodology and property checking techniques. The methodology we propose enables designers to meet today's aggressive time-to-market goals, while providing higher confidence in functional correctness. It benefits dynamic verification (that is, simulation), while providing a seamless path to static (formal) verification. This chapter provides a general introduction to property checking and assertion techniques. We present the benefits associated with assertion-based design and address the many fallacies associated with their use. Finally, we discuss the importance of a specification-driven methodology related to design and implementation.