Checkers - SVA: The Power of Assertions in SystemVerilog - page 178

Chapter 9
Checkers
Contradictions do not exist. Whenever you think you are facing
a contradiction, check your premises. You will find that one of
them is wrong.
— Ayn Rand
In this chapter, we introduce checkers, units for packaging assertion-based
verification code. On the one hand, checkers are similar to modules and interfaces:
they define their own hierarchical scope and they may contain most constructs
allowed in modules and interfaces. On the other hand, checkers generalize properties
and sequences: they are instantiated “in place”, their arguments may be sequences,
properties, and edge-sensitive events. One can also say that checkers generalize
assertions, since they behave as one complex assertion. In the subsequent sections,
we elaborate the checker definition, instantiation and simulation semantics.
Using checkers makes the RTL cleaner: most instrumentation code in modules
may be moved to checkers, which improves the code modularity, makes module
code more readable and less error prone. Synthesis tools are normally supposed
to ignore checkers, thus there is no need in conditional compilation statements to
isolate the instrumentation code for the synthesis tools.
Although synthesis tools ignore checkers, most of the checker code is synthesi-
zable. Checkers may be synthesized for hardware emulation and even in silicon, if
so desired. Since the formal verification tools work on the synthesis model, checkers
are formal verification friendly.