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
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…
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
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