Can anyone help me understand this SVA? This is in one of the CDC verification techniques by Matt Litterick.
property p_no_glitch;
logic data;
@(d_in)
(1, data = !d_in) |=>
@(posedge clk)
(d_in == data);
endproperty : p_no_glitch
What exactly does (1, data = !d_in) do?
In reply to kernalmode1:
One of the options of what a sequence is:
sequence_expr ::=
...
| (sequence_expr {, sequence_match_item}) [sequence_abbrev]
// for example,
(ack, v_data=data, v_ir=ir)[*2] // this is a sequence expression
sequence_match_item ::= operator_assignment | inc_or_dec_expression | subroutine_call
// for example
v_data=data // (write, v_data=data)
v_data += 1
v_data=f_convert(data)
BTW, the property as written is incorrect because the way the multiclocking is used is incorrect. From my SVA Handbook 4th Edition
The correct way to write this property is as shown below from a multiclocking point of view. Note that when d_in changes, as it may after a @(posedge clk), that assertion will trigger. If d_in goes to 1’b1, the sampled value is 1’b0 and data gets set to 1’b1, and at the next @(posedge clk) you check that d_in (with an expected value of 1’b1) is equal to 1’b1.
property p_no_glitch; // Note the change of name
logic data;
@(d_in) (1, data = !d_in) |-> // Note the " |-> " because of multiclocking
@(posedge clk) (d_in == data);
endproperty : p_no_glitch
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
In reply to ben@SystemVerilog.us:
Sorry, but I still do not understand… I am not worried about the correctness of the expression.
(1, data = !d_in)
Is this some sort of concatenation? Or some kind of a conditional statement for assertions? What does ‘1’ do here? data is being assigned !d_in which makes sense to me. But I dont see how ‘1’ fits in here…
In reply to kernalmode1:
sequence_expr ::=
...
| (sequence_expr {, sequence_match_item}) [sequence_abbrev]
This says every time the sequence_expr matches, execute the sequence_match_item.
In your case, the sequence_expr is 1, meaning always true, so match happens unconditionally every clock cycle. The sequence_match_item is the assignment data = !d_in
In reply to dave_59:
Thanks Dave and Ben.
Dave, Do you agree with Ben on the correctness/incorrectness of the expression? I just happened to comes across the paper and I believe it has been widely published at dvcons.
In reply to kernalmode1:
Dave will provide his own opinions; however, my rational for the use of |-> instead of |=> is to cover the case when d_in toggles in the SAME identical time as @(posedge clk).
Ben SystemVerilog.us