Hi ,
Question :
bit[3:0]fifo_lvl,fifo_lvl2;
Collect the value fifo_lvl, when valid is high @clk1.
when en = 1@(clk2) & after one clk cycle of (@clk2) Compare with fifo_lvl == fifo_lvl2.
Please let me know above scenario using assertions ?
Thank you.
In reply to gani:
bit[3:0]fifo_lvl,fifo_lvl2;
bit valid, en;
//Collect the value fifo_lvl, when valid is high @clk1.
//when en = 1@(clk2) & after one clk cycle of (@clk2) Compare with fifo_lvl == fifo_lvl2.
property p_fifo;
bit[3:0] v;
@(posedge clk1) (valid, v=fifo_lvl) |->
@(posedge clk2) en[->1] ##1 v==fifo_lvl2;
endproperty
ap_fifo: assert property(p_fifo);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
Thank you ,here i seen issue
@(posedge clk2) en[->1]##1 v==fifo_lvl2;
##1 delay is considering @(posedge clk1),i am expecting @(posedge clk2).
clk1 = clk2/2 (here i can use ##2 instead of ##1 to fix above problem - But i don’t want to do work around - is there any way of waiting for ##1 on clk2?)
Thank you.
In reply to gani:
In reply to ben@SystemVerilog.us:
Thank you ,here i seen issue
@(posedge clk2) en[->1]##1 v==fifo_lvl2;
##1 delay is considering @(posedge clk1),i am expecting @(posedge clk2).
clk1 = clk2/2 (here i can use ##2 instead of ##1 to fix above problem - But i don’t want to do work around - is there any way of waiting for ##1 on clk2?)
Thank you.
You are incorrect. I am attaching 2 pages from my SVA Handbook 4th Edition tht explains the clock flow in multiclocking. It is complicated, I agree.
Basically, clock flows across elements of same sequence.
But if that sequence is a sequence instance or a parenthesized sequence, the rules are different. [1] A clocking event in the declaration of a sequence or property does not flow out of an instance of that sequence or property. However, the clock flows across elements of same sequence. Thus, the following 2 properties are different:
@(posedge clk1) (valid, v=fifo_lvl) |->
@(posedge clk2) en[->1] ##1 v==fifo_lv2;
// NOT SAME AS
@(posedge clk1) (valid, v=fifo_lvl) |->
(@(posedge clk2) en[->1]) ##1 v==fifo_lv2;
From SVA Handbook 4th Edition, 2016
Your model:
http://SystemVerilog.us/fv/multi.sv
Property with clk2 in (),
property p_fifo2;
bit[3:0] v;
@(posedge clk1) (valid, v=fifo_lvl) |->
(@(posedge clk2) en[->1]) ##1 v==fifo_lv2;
endproperty
ap_fifo2: assert property(p_fifo2);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
