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

Exercises
9.1. Assertion a_initial_no_complete from Fig. 9.4 does not behave correctly
in the general case when rst is initially low. For what actual arguments corre-
sponding to rst the assertion behaves always correctly? Consider the use cases
of simulation and formal verification. Hint: Consider cases when the corresponding
actual argument is of type logic and bit , and when it is explicitly initialized or
not.
9.2. Fix assertion a_initial_no_complete from Fig. 9.4 to handle the case when
the reset is initially low. Hint: consult Sect. 11.2.1.1 .
9.3. In assertion a_initial_no_complete from Fig. 9.4 rst is used both in the
implicit disable iff clause and in the body of the assertion. Which problem
does this cause? How to solve it? Hint: Consider variable sampling in concurrent
assertions.
9.4. Write a checker verifying that each request is followed by a grant, and that the
request happens at least once.
9.5. Example 9.11 introduces a checker simple_reset to verify that the reset
signal is initially high then it eventually goes low and remains low forever.
(a) Modify this checker to make it generic. The new checker should accept the
assertion clock as an optional argument. This argument should default to
$global_clock .
(b) If the reset remains always high, the checker assertion does not fail in simu-
lation. How should the checker be modified to ensure that a more meaningful
scenario is exercised in simulation?
(c) What would the checker verify if followed-by (suffix conjunction) #=# is
replaced with suffix implication |=> ?
9.6. Implement the checker check_window borrowed from OVL [ 10 ] (with minor
modifications).
This checker ensures that the condition cond is true in a specified window
between a start and complete .
The checker should have the following arguments:
￿ cond —expression that should be true in the event window
￿ start —sequence whose completion opens the event window
￿ complete —sequence whose completion closes the event window
￿ clk —clock event for the checker. Should be inferred from the context by default
￿ rst —checker reset signal. Should be inferred from the context by default
￿ msg —message to be issued in case of the check failure. Default is “Violation”
￿ collect_cov —elaboration time constant indicating that the coverage about
window should be collected. Default is yes. The following coverage information
is collected.