In reply to ben@SystemVerilog.us:
An option for your 1st property using the Non-consecutive repetition, Boolean([=n]
property p_lock_condition_check_unlock_prog_00_Voption; // Using |-> ##1 (consequent)
//int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:6])
##0 o_fll_lock;
endproperty
In reply to ben@SystemVerilog.us:
In reply to ben@SystemVerilog.us:
An option for your 1st property using the Non-consecutive repetition, Boolean([=n]
property p_lock_condition_check_unlock_prog_00_Voption; // Using |-> ##1 (consequent)
//int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:6])
##0 o_fll_lock;
endproperty
Hi Ben
Thank you for all your suggestion. and “p_lock_condition_check_unlock_prog_00_Voption” is not working. But others are working well.
In reply to rkg_:
The following test model worked OK for me
ap_a2b2c: assert property(@ (posedge clk)
$rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));
//code
module top;
timeunit 1ns; timeprecision 100ps;
`include "uvm_macros.svh" import uvm_pkg::*;
bit clk, a, b, c, reset_n;
default clocking @(posedge clk);
endclocking
initial forever #10 clk = !clk;
ap_a2b2c: assert property(@ (posedge clk)
$rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));
initial begin
repeat (200) begin
@(posedge clk);
if (!randomize(a, b, c) with {
a dist {1'b1 := 1, 1'b0 := 3};
b dist {1'b1 := 1, 1'b0 := 2};
c dist {1'b1 := 1, 1'b0 := 2};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
Hi Ben,
property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |=>
(1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
This assertion is failing even after lock is asserted ( just after 6 posedge of sampled_monclk after lock assertion ). Do we need to put some extra logic so that one lock is asserted it should not check until the next packet will come ?
In reply to rkg_:
After every successful antecedent, a new thread is fired, and that thread is independent of any other previously fired thread. That can cause errors if you want to check the packets independently. Below is a simulatable example where I used the block.
/*property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |=>
(1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
This assertion is failing even after lock is asserted ( just after 6 posedge of sampled_monclk after lock assertion ).
Do we need to put some extra logic so that one lock is asserted it should not check until the next packet will come ? */
module top;
timeunit 1ns; timeprecision 100ps;
`include "uvm_macros.svh" import uvm_pkg::*;
bit clk, a, b, c, reset_n, block;
initial forever #10 clk = !clk;
function void set_block(bit x);
block=x;
endfunction
ap_a2b2c: assert property(@ (posedge clk)
$rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));
ap_a2b2cBLOCK: assert property(@ (posedge clk)
($rose(a) && block==0, set_block(1)) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]))
set_block(0); else set_block(0) ;
initial begin
repeat (200) begin
@(posedge clk);
if (!randomize(a, b, c) with {
a dist {1'b1 := 1, 1'b0 := 3};
b dist {1'b1 := 1, 1'b0 := 4};
c dist {1'b1 := 1, 1'b0 := 4};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
In reply to ben@SystemVerilog.us:
In reply to rkg_:
Addressing your second question first
http://systemverilog.us/vf/rpt2.sv
// After the |-> ##1 the sequence (b} is repeated twice
ap2: assert property(a |-> ##1 (b)[*2]);
// After the |-> the sequence (##1 b) is repeated twice
ap2_1: assert property(a |-> (##1 b)[*2]);
Hi Ben, I don’t get the difference. When I see both and try to rewrite the repetition operator I get
##1 b ##1 b
for both style. What am I missing?
In reply to emin:
In this case, there is no difference because the sequence is one term. However, let the sequence to be repeated is longer than one term.
|-> ##1 (b ##2 c)[*2]); // same as
##1 (b ##2 c) ##1 (b ##2 c)
|-> (##1 b ##2 c)[*2]); // same as
(##1 b ##2 c) ##1 (##1 b ##2 c)
// The difference :
##1 (b ##2 c) ##1 (b ##2 c) // |-> ##1 (b ##2 c)[*2]);
(##1 b ##2 c) ##1 (##1 b ##2 c) // |-> (##1 b ##2 c)[*2]);
// ^^^
In reply to ben@SystemVerilog.us:
Ben,
a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a
a[->3] ##1 b; //3 non consecutive/consecutive a and then b immediately after one clock cycle of a
If above understanding is correct , then can we use ##5 instead of ##1 in the first case?
In reply to ben@SystemVerilog.us:
In reply to emin:
In this case, there is no difference because the sequence is one term.
Great. Thank you for clarifying!
But we see different behaviour here,
In reply to ben@SystemVerilog.us:
In reply to rkg_:
How did ap2_1’s first thread did pass even though there we have b deasserted? I thought that must fail as well at the same time as ap2 since you said there is no difference.
In reply to emin:
OOPs! I spoke too fast, my apologies, the two ARE different.
Humans make mistakes :)
|-> ##1 (b)[*2]);
##1 b ##1 b
|-> (##1 b)[*2]
(##1 b) ##1 (##1 b)
In reply to emin:
Hi Ben,
Property :-
// 1st requirement (fll_lock_assertion):- FLL LOCK is asserted on detecting two positive edges
// of FLL INC or FLL DEC only when (fll_sar_eoc == 1). and fll_inc or fll_dec anytime after (sar_eoc==1) but once any thing (posedge of dec or inc) comes second comes between 1 to 8 (since prog_unlock is 1 here) then only lock should asserted.
// and two positive edge of fll_inc or fll_dec (consecutive is not necessary )
//between 1 to 6 clock cycle of sampled_clk
Type - 1
property p_lock_condition_check_unlock_prog_01;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( o_fll_sar_eoc == 1 && i_fll_unlock_prog == 2'b01, inc_count=0, dec_count=0 ) |=>
(1, inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec))[*1:8] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
Problem 1 :-lock is asserted after 22 clk cycle of sample_monclk. and above assertion is not able to caught. (marked in purple)
Problem 2 :- assertion failing after de-assertion of lock. (marked in red )
problem 3:- Unexpected triggered (marked in blue colour)
waveform attached.
Type -2 :
property p_lock_condition_check_unlock_prog_01;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
endproperty
Problem -1 :- Assertion triggered but it start checking fll_inc or fll_dec right after the sar_eoc assertion till the 1 to 8 clock cycle of sample clk (instead it should wait and check fll_inc or fll_dec anytime after (sar_eoc==1) but once any thing (two posedge of dec or inc whoever come early ) between 1 to 8 of sample_monclk (since prog_unlock is 1 here) then only lock should asserted.[/b])
Waveform :-
do you see any issue ?
In reply to rkg_:
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for suggestion and i am totally agree with you.
Just one doubt on below assertion
property p_lock_condition_check_unlock_prog_01;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
endproperty
** intersect 1’b1[*1:8] , will it start matching just after sar_eoc==1. is it correct understanding ?
** if yes, how to put condition so that it should only match after first posedge of fll_inc and fll_dec (anytime after sar_eoc==1)
In reply to rkg_:
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
// Rearranging the ()s
antecedent |->
##1 ( (a_sequence or b_sequence) intersect 1'b1[*1:8]
)
##0 o_fll_lock;
// Thus, in
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8]
// the following two threads start at the same cycle
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) // One thread
1'b1[*1:8] // a parallel thread
intersect 1’b1[*1:8] , will it start matching just after sar_eoc==1. is it correct understanding ?
NO, sar_eoc==1 is in the antecedent. As mentioned above, the intersect starts after the ##1 at
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2])
Ben
In reply to ben@SystemVerilog.us:
Hi Ben ,
I have enabled the debug mode and i have few observation.
NO,$rose (sar_eoc) modified is in the antecedent. As mentioned above, the intersect starts after the ##1 at
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) → one thread start just after 1 clock cycle on detection of posedge of sar_eoc and it will run based on intersect 1’b1**[1:8]* here for 8 clock cycle , (if i change to 20 thread will finish at 20 clock cycle ).
case: 2 And one place even, there is no toggle in inc and dec, it has triggered .
*it seems, what i asked question looking right here "intersect 1’b1[1:8] , will it start matching just after sar_eoc==1" (in my case )
I guess it is not taking care $rose of (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2])
thus it is triggering case 2 (my assumption )
And from above comment : (a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a ) we have used [=] operator so if anytime inc or dec goes high 2 times continuously it will start intersect which is happening in my case 2 (i guess).
I have attached the waveform :
if you can suggest changes , for after detection of posedge of sar_eoc , if ($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2] (gap between two posedge of non- consecutive of inc or dec should be 8 sampled_monclk ) lock should asserted.
And in the same way
property p_lock_condition_check_unlock_prog_00;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( $rose (o_fll_sar_eoc ) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |->
**##1 ((inc_count==1 ||dec_count==1 ), inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec),$display("\t **time=%t inc_count**= %d, dec_count ",$time,inc_count,dec_count))**[*1:6] ##0
o_fll_lock===(inc_count==2 || dec_count==2);
endproperty
** inc_count and dec_count is always zero in my log even i can see the posedge of fll_inc and dec in my simulation (Seems $rose it is not taking)
In reply to rkg_:
I am having trouble deciphering your question.
I modeled your code using the variables a, b, c
http://systemverilog.us/vf/may7b.sv
What is the issue?
// DO you want this?
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
// OR this "intersect 1'b1[*1:8] , will it start matching just after sar_eoc==1"
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
(($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
I suggest that you play with my code, and add debugging features.
You may also want to rephrase your requirements in English.
module top;
timeunit 1ns; timeprecision 100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b, c, frame;
event start, one, two, isct0, endc;
initial forever #10 clk = !clk;
/* ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock; */
function automatic void gen_e(int i);
if(i==0) -> start;
if(i==0) frame = 1'b0;
if(i==1) -> one;
if(i==2) -> two;
if(i==3) -> isct0;
if(i==3) frame = 1'b1;
if(i==4) begin frame = 1'b0; -> endc; end
endfunction
always @(posedge clk) begin
ap_test: assert property(@ (posedge clk) ($rose(a),gen_e(0)) |->
##1 (1, gen_e(1)) ##0 ( ($rose(b)[=2], gen_e(2)) intersect
(1, gen_e(3)) ##0 1 [*1:8] )
##0 (c, gen_e(4))) else frame <= 1'b0;
repeat(15) @(posedge clk) ; // separate threads for analysis
end
initial begin
repeat (200) begin
@(posedge clk); #2;
if (!randomize(a, b, c) with {
a dist {1'b1 := 1, 1'b0 := 4};
b dist {1'b1 := 1, 1'b0 := 1};
c dist {1'b1 := 1, 1'b0 := 1};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
Hi Ben,
As you asked,
What is the issue?
// DO you want this? ---> **i want this**
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
// OR this "intersect 1'b1[*1:8] , will it start matching just after sar_eoc==1"
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
(($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
http://systemverilog.us/vf/your_screen.png → In this snippet,(at your green arrow marker ) why is assertion is getting triggered since I do not see two non-consecutive inc or dec.
I am writing assertion to check lock is happening only if two posedge of inc or dec (means only two non consecutive ) and gap between two posedge inc or dec is 1 to 8 cycle of sample_monclk.
In reply to rkg_:
(at your green arrow marker ) why is assertion is getting triggered since I do not see two non-consecutive inc or dec.
I updated the snippet http://systemverilog.us/vf/intersect8.png
The assertion is working as defined. See my example in my previous reply where instead of your variables and your sequences, I use a simplified version of the same form with the variables a, b, c.
In reply to ben@SystemVerilog.us:
Thanks for detailed description.
Just last doubt regarding this assertion.
How to modify this assertion so that intersect event(isct0) should only active after the first posedge of inc or dec.
Specification says : lock should only asserted only when (eoc ==1) and two non consecutive posedge of inc or dec anytime after when (eoc =1) and length or gap between two non cosecutive posedge of inc or dec should be 1 to 8 clock cycle of sampled monclk. if length is more then 8 and if lock get asserted it should fail.
property p_lock_condition_check_unlock_prog_01;
@(posedge sampled_monclk) disable iff (!i_en_fll)
(($rose(o_fll_sar_eoc) && i_fll_unlock_prog == 2'b01 ),gen_e(0)) |->
##1(1, gen_e(1)) ##0 ((($rose(o_fll_inc)[=2],gen_e(2)) or ($rose(fll_dec)[=2],gen_e(2))) intersect (1, gen_e(3)) ##0 1[*1:8]) ##0 (o_fll_lock,gen_e(4));
endproperty
waveform :
