Introduction - SVA: The Power of Assertions in SystemVerilog - page 27

PSL has an important mechanism of vunits (verification units) for encapsulating
verification code. One vunit may inherit another in order to modify a portion of the
verification environment. SVA has the checker construct and the bind statement.
Vunits and checkers implement two different approaches to verification environment
design: vunits are based on overriding and name matching, while checkers are based
on argument mapping.
In contrast to PSL, SVA provides immediate and deferred assertions. The use
and semantics of assertions in procedural code is undefined in PSL. Also, PSL lacks
any notion of properties being invoked recursively. Since SVA is an integral part of
SystemVerilog, its simulation semantics is well defined and SVA can be used much
more widely within the context of SystemVerilog than is possible with PSL. Some
examples of the benefits are:

￿ Sequences can be used outside the context of assertions.
￿ Integration with functional coverage features is powerful.
￿ Sampling of variables is precisely defined.
￿ Type compatibility and conversion is handled smoothly.

Exercises

1.1. What is the main difference between the assertion specification language in
SystemVerilog and the language subset used for RTL description?

1.2. Modify the RTL code in Figs. 1.2 and 1.4 to take reset signal rst into account:
when rst is asserted checking of active transactions should be stopped.
1.3. Implement the following assertion

assert property (@( posedge clk) req[ * 2] |=> grant[ * 2]);
in RTL: two consecutive requests should be followed by two consecutive grants.

1.4. What kinds of assertions exist in SVA? What is the difference between them?

1.5. Compare formal specification languages with natural languages. What are the
advantages of formal languages?

1.6. What are the main advantages and disadvantages of checking assertions in
(conventional) simulation?

1.7. Why is it useful to check assertions in emulation?

1.8. What are main advantages and disadvantages of checking assertions using
formal verification?

1.9. Why is assertion reuse important? Which constructs exist in SystemVerilog for
assertion reuse?

1.10. What is the intended use of checkers in SystemVerilog?