In reply to hisingh:
@(posedge r_clk) disable iff (!w_rst_n || !r_rst_n)
(r_valid && r_ready, p_rbaddr=r_baddr, p_rdata=r_data) ##0
@(posedge w_clk) (w_valid && w_ready, p_wbaddr=w_baddr, p_wdata=w_data) |=>
(w_memory[p_wbaddr] === p_wdata) && (r_memory[p_rbaddr] === p_rdata);
For the multiclocked property ::
(a) If both @(posedge r_clk) and @(posedge w_clk) are True at T0 then
p_rbaddr , p_rdata , p_wbaddr and p_wdata are all assigned at T0.
(b) If @(posedge r_clk) is True at T1 whereas @(posedge w_clk) is False at T1 ,
then p_rbaddr and p_rdata are assigned at T1 and p_wbaddr and p_wdata are assigned at nearest @(posedge w_clk) .
[Q1] Is my understanding correct for (a) and (b) ?
[Ben] Yes, you are correct
[Q2] When is the consequent evaluated ? i.e which clock is used
Is it at the next @(posedge r_clk) OR next @(posedge w_clk) ?
[Ben]The last defined clockflows through the implication operator.
THus, next @(posedge w_clk) is used.
** [my book] 4.3.3 Clock Flow Rule: Flow through |->, |=> :
When no explicit clock event is specified in an implication operator,
the clock from the end point of the antecedent is understood to flow across the operator.
Thus, the following to property expressions are identical:
@(posedge clk0) a0 |-> @(posedge clk0) a1 ##1 @(posedge clk2) a2;
** Rule: [1] A clocking event in the declaration of a sequence or property
does not flow out of an instance of that sequence or property.
owever, the clock flows across elements of same sequence.
For example, assuming no default clocking:
sequence q_ef; @ (posedge clk) e ##[1:5] f; endsequence : q_ef
ap_q_ef_a: assert property (q_ef ##1 a); // Illegal, clk does not flow into “a”
** Rule: Clocking event is trapped in parenthesized sequence: [1]
The scope of a clocking event flows into parenthesized subexpressions and,
if the subexpression is a sequence, also flows left-toright across the
parenthesized subexpression.
However, the scope of a clocking event does not flow out of enclosing parentheses.
The standard also states that when sequence instances are flattened,
the resulting expression that is returned is enclosed in parenthesis;
therefore clocks do not flow out of sequence instances either.
In the following example, the parentheses are within a sequence:
@(posedge clk1) w ##1 (r ##1 @(posedge clk2) y ) |=> m;
//Is equivalent to:
@(posedge clk1) w ##1
(@(posedge clk1) r ##1 @(posedge clk2) y |=>
@(posedge clk1) m;
w, r, m are clocked at posedge clk1 and y is clocked at posedge clk2.
Clock posedge clk1 flows across ##1, over the parenthesized subsequence
(r ##1 @( posedge clk2) y), and across the nonoverlapping implication |=> operator.
Clock posedge clk1 also flows into the parenthesized subsequence,
but it does not flow through @(posedge clk2).
Clock posedge clk2 does not flow out of its enclosing parentheses;
thus it does not flow into m.
SO what does that mean your
@(posedge r_clk) disable iff (!w_rst_n || !r_rst_n)
(r_valid && r_ready, p_rbaddr=r_baddr, p_rdata=r_data) ##0
@(posedge w_clk) (w_valid && w_ready, p_wbaddr=w_baddr, p_wdata=w_data) |=>
(w_memory[p_wbaddr] === p_wdata) && (r_memory[p_rbaddr] === p_rdata);
In this case, the consequent is clocked with w_clk. However, if you wrote it this way:
// NOTE THE ()
@(posedge r_clk) disable iff (!w_rst_n || !r_rst_n)
(r_valid && r_ready, p_rbaddr=r_baddr, p_rdata=r_data) ##0
(@(posedge w_clk) (w_valid && w_ready, p_wbaddr=w_baddr, p_wdata=w_data)) |=>// **new ()**
(w_memory[p_wbaddr] === p_wdata) && (r_memory[p_rbaddr] === p_rdata);
The consequent will be clocked with the r_clk because the write sequence (expression in this case)
is enclosed with its clocking event in parentheses.
Trivial, isn’t it?
:)
Ben
