Hardware Reference
In-Depth Information
module decl_in_clocking_block ( logic a, b, c, clk);
clocking PCLK; @( posedge clk);
property p3; a |=> p4; endproperty
endclocking
property p4; b until c; endproperty
a19: assert property (PCLK.p3);
endmodule
Since p4 is declared without clocks, the instance of p4 within the declaration of p3
is legal. The clock of p3 is posedge clk , which flows into and clocks this instance
of p4 .
Exercises
12.1. Write an assertion to check that after an occurrence of event ev_start ,
there is no occurrence of event ev_wait until strictly after an occurrence of event
ev_enable (cf. Example 12.2 ).
12.2.
Without
using
the nexttime operator,
rewrite
assertion a14 from
Sect. 12.2.5.1 so that its behavior is identical to that of a13 .
12.3. Using the waveform in Fig. 12.12 , analyze the behavior of the following
assertion:
a1: assert property (
@( posedge clk1) a |=> @( posedge clk2) nexttime b
);
12.4. Using the waveform in Fig. 12.12 , analyze the behavior of the assertions in
the following module for the evaluation attempts beginning at times 20 and 60:
module m( logic a, b, clk1, clk2);
a1: assert property (
@( posedge clk1) a |->
(@( posedge clk2) a) until (@( posedge clk2) b)
);
a2: assert property (
@( posedge clk1) a |-> @( posedge clk2) a[ * ] ##1 b
);
endmodule
12.5. Consider the assertion
a1: assert property (
@( posedge clk1) a |-> @( posedge clk2) nexttime b
);
Create waveforms in which clk2 converges to clk1 from the right to explain why
the synchronizing behavior of nexttime must both align and advance to the next
tick in order for the multiply clocked semantics to converge to the singly clocked
semantics. What happens if clk2 converges to clk1 from the left?
Search WWH ::




Custom Search