Checkers in Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 537

23.2. Define the formal semantics of a conditional free variable assignment con-
trolled by a clocking event of the form of @( edge clk) and of each of the forms
listed in Exercise 23.1 .

23.3. Implement the checker from Example 23.18 using local variables instead of
free variables.

23.4. What is the difference between the behavior of checkers check1 and check2
(dotted parts are the same and do not assign v in both checkers)?
checker check1(...);
bit [3:0] v = ...;
// ...
endchecker : check1

checker check2(...);
rand bit [3:0] v = ...;
// ...
endchecker : check2
How should the checker check2 be modified to have the same behavior as the
checker check1 ? The variable v should remain free in check2 .
23.5. Rewrite the following fragment of a checker always_ff procedure to
eliminate all conditional statements.

if (c1)
if (c2) begin
a<=x;b<=y;a<=z;
end
else a<=x;
else begin
a<=y;
if (c2); else a<=x;
end

23.6. Implement checker data_consistency from Example 23.29 without using
local, free, or rigid variables. Assume that the transactions do not overlap.

23.7. The output data out_data at the end of transaction ( end_t asserted) has the
same value as the input data in_data at the beginning of the transaction ( start_t
asserted). With each transaction is associated a tag: the tag at the beginning of the
transaction is contained in stag , and the tag at the end of the transaction is contained
in etag . For the same transaction, stag and etag have the same values.
Implement this specification as a checker

(a) using rigid variables, and

(b) as an assertion with local variables.

23.8. What is the problem with the following definition of simulation semantics of
a continuous assignment to a free variable: Continuous assignment to a free variable
executes in the Active region? Consider both the case when the right-hand side is