Functional coverage, stimulus generation, and run management are the three major interrelated tasks of functional verification today. Among these, functional coverage arguably looms as the most important, largely because coverage closure is the main criteria for tapeout. Measures of coverage provide critical feedback, such as the existence of gaps. As shown in figure 1, a comprehensive coverage model should consist of end-to-end functional coverage, transaction coverage on major interfaces, structural coverage of critical RTL structures and basic code coverage.
Figure 1: A comprehensive coverage model
An assertion-based methodology helps catch bugs, audit the quality of the regression environment and guard against illegal module use. Such a methodology need not be developed by the verification team alone. Designers can provide significant value by capturing their intimate knowledge about the internal operations of the design in the form of assertions.
Assertions and functional coverage are really two sides of the same coin . Both provide detailed observation points within a register transfer level (RTL) design. And while assertions’ design checking attributes are well known, the additional benefit -- supplementing functional coverage measurement -- is frequently overlooked by design teams. It turns out that the task of placing assertions in a design is similar to the task of finding interesting and relevant functional coverage points. Accordingly, it often makes sense to add assertions and coverage points concurrently.
Following a small handful of guidelines can make it easier to instrument a design. First, put the assertions in the RTL code so that they can be managed, updated and re-used along with the RTL code. Next, separate the assertions from the RTL through proper annotation; some companies recommend putting ifdef/endif around the assertions so that they can be excluded from tools in the implementation flow. Finally, stay with a language subset so that the assertions are good for simulation, formal model checking, hardware acceleration and FPGA prototyping.
Assertions need not be complex. In fact, based on my experience, simple assertions are often as useful as complex assertions, including in catching complex bugs. In the following sections, I will explore how to tack SystemVerilog  assertion properties and coverage properties onto several elements of a design, including:
1. Variable declarations
2. Conditional statements
3. Internal interfaces
4. Design elements
5. Finite state machines
Some readers would like to learn more about Assertion Based Verification. I would recommend the free Verification Academy (verification-academy.com) organized by Harry Foster. There is a module focusing on Assertion Based Verification.
Excellent article, Dr. Yeung. The examples you show are very practical and commonly encountered (and even more commonly overlooked, but that's another story). This is a very good foundation to start with in planning verification.
In addition, I find your writing to be wonderfully clear and concise. No fluff, very precise, and no ambiguity in message and intent. Great work!