Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 329

always @( posedge clk) begin
if (load) begin
sh[0] <= d_in;
for ( int i=1; i<D; i++)
sh[i] <= sh[i-1];
d_out <= sh[D-1];

end

end

1. Write a procedural concurrent assertion to check that if load is true, then the
current value in position j of the shift register is the next value in position j+1 ,
where j ranges from 0 to D-2 .
2. Write a procedural concurrent assertion to check that after D+1 occurrences of
load , d_out holds the value that was originally in d_in .[Hint:Use const cast
to capture the value of d_in when your assertion is invoked.]
14.4. In Example 14.18 , what assertion evaluation results in a time step in which
c1_long changes value from true to false? Be sure to consider that the change in
c1_long may be neither the first nor the last event in the time step that triggers
procedural block B2 .
14.5. Consider the following variant of Example 14.21 :
always @( * ) begin :B1
a <= a_in;
a_1: assert property (@( posedge clk) a == const '(a_in));
@( edge clk) b <= b_in;
a_2: assert property (@( posedge clk) b == const '(b_in));
end
Describe scenarios in which triggering B1 causes:
1. An instance of a_1 that gets purged and an instance of a_2 that matures.
2. An instance of a_1 that matures and an instance of a_2 that gets purged.
3. Instances of a_1 and a_2 that both mature.
4. Instances of a_1 and a_2 that both get purged.
14.6. Consider the following checker declaration:
checker chk(a, b, event ev = $inferred_clock);
a1: assert property (@ev a);
always_ff @ev begin
a2: assert property (b);

end
endchecker : chk
For each of the following instances of checker chk , either give a rewrite that is
conceptually equivalent and eliminates the checker instance or explain why the
checker instance is illegal.

1.

always @( posedge clk) begin
A <= A_in;