Let, Sequence and Property Declarations; Inference - SVA: The Power of Assertions in SystemVerilog - page 177

8.3 Disable Expression and Clock Inference

The default disable iff statement provides a default disable condition for
assertions where the disable condition is not explicitly specified. Similarly,
default clocking provides a clocking expression that can be inferred when not
explicitly specified. Both default statements can be specified only once in a module ,
interface , program , and checker , and their effect extends over the full scope
of the object. It does not extend, however, to any instances of such objects. For a
detailed discussion about clock and disable expression inference see Chaps. 12 - 14 .

Exercises

8.1. Write down a parameterized let definition that can be included in a package
for the following situation. Include means to make the let expression take some
useful default value when the argument rst is 1'b1 . Illustrate its use in some
assertion and assignment statement.

(a) Evaluate to 1'b1 only when the vector argument sig has at most one 1 or one
0 and the rest is either X or Z . Otherwise, return 1'b0 . Should the argument sig
be typed or untyped? Why?
(b) Is it possible in a single let definition to restrict the above definition to return
1'b1 only if there is at most one 1 or one 0 , and the rest are z (i.e., exclude x )?
8.2. Write down a simple module that has the variables clk , reset , a , and b of type
logic , and add a concurrent assertion that fails when a is 1 , and at the next clock
tick b is 0 , 1 ,or x . Let the clock and reset be inferred from the module context.
8.3. Provide a solution to Exercise 8.2 such that the property used in the assertion
is first defined outside the module, e.g., in a package.

8.4. What kind of actual arguments can be legally passed to the property that you
defined in Exercise 8.3 . Can you generalize the property to accept a wider range of
arguments? How should the specification of the property change?