Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 57

Chapter 4
Assertion Statements
Language is a mixture of statement and evocation.
— Elizabeth Bowen
In this chapter, we describe SVA assertion statements: 1
￿ Assert statements
￿ Assume statements
￿ Restrict statements
￿ Cover statements
The term assertion is overloaded in SVA; in a narrower sense it means an assert
statement, and in a broader sense it means any assertion statement listed above.
In this chapter, we use the term assertion in its narrow meaning. We indicate the
meaning explicitly when it is not clear from the context.
Assertion, assumption, and cover statements may be of the following kinds:
immediate and concurrent. Immediate assertions are further subdivided into simple
immediate and deferred. The deferred ones are of two kinds—observed and final.
They are used when filtering of 0-width glitches is needed in simulation. Restrict
statements may only be concurrent.
For convenience, we briefly recapitulate main results of Sect. 1.4 , how different
kinds of assertion statements are checked in simulation and in formal verification.
We then describe basic simulation semantics for different kinds of assertion
statements. Their understanding is important to correctly choose the kind of
assertions in each particular case. Knowing principles of assertion simulation is also
1 In SVA, there is also expect statement used mostly in testbenches, but we do not describe it in
this topic.