// You are using the following definition of what a sequence is:
sequence_expr ::=
| (sequence_expr {, sequence_match_item})
// NOTE: before the "," is a sequence, after the "," is a sequence_match_item
// and a sequence_match item is
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call
// Your antecedent
( $rose (o_fll_sar_eoc) , i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)
// <--sequence_expr--> , <---------------- sequence_match_item -------------->
i_fll_unlock_prog == 2'b00 // is NOT an operator_assignment or inc_or_dec_expression
// It is a comparison (T or F), thus illegal.
// You meant to say in the sequence_expr. Thus,
( $rose (o_fll_sar_eoc) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)
// Also OK
( $rose (o_fll_sar_eoc) ##0 i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)
what is the use of [*6} ?
for lock de-assertion it can happen at any number of sampled clk unlike lock condition . only thing is four consecutive fll_inc or fll_dec after the lock assertion .
May i know the difference between
// note the " |-> ##1 (expr1)[*6] ##0…"
// this is different from
// " |-> (##1 (expr1))[*6] ##0…" ??
// 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]);
what is the use of [*6} ?
for lock de-assertion it can happen at any number of sampled clk unlike lock condition . only thing is four consecutive fll_inc or fll_dec after the lock assertion .
The [*6} came from your original requirements … based on value of a, number of cycle (between 1 to 6 clock cycle of ref_clk)
Also, without a repeat operator how could the local variable inc_count, dec_count ever be ==4? SOmething is missing in your requirements. With poorly expressed requirements, I am doing my best to make assumptions, hoping that you’ll get the idea as to what best todo.
It might be a good idea to express again all the requirements in English.
As to you last comments for lock de-assertion it can happen at any number of sampled clk unlike lock condition . only thing is four consecutive fll_inc or fll_dec after the lock assertion . You could change the property to something like:
// Fix as needed per requirements
property p_unlock_condition_check_unlock_prog_00;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( $rose (o_fll_lock) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |->
##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
!o_fll_lock==(inc_count==4 || dec_count==4)
##0 !o_fll_lock[->1]; // if needed
Thank you for reply. let me tell my requirement. I have basically two reequipment. one is for fll_lock assertion and second is for fll_lock deassertion.
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 two positive edge of fll_inc or fll_dec ([b]consecutive is not necessary ) between 1 to 6 clock cycle of sampled_clk[/b]
2nd requirement (fll_lock de assertion ) :- FLL lock is de-asserted on detecting of four consecutive of o_fll_inc signal or fll_dec signal. here the.
Note :- 1. for requirement two : positive edge is not needed but consecutive of fll_dec or
fll_inc is must. 1 to 6 clock cycle is [b]not required[/b].
In reply to rkg_:
See if the following works. Make sure you use the |-> ##1 (consequent)[*n] and NOT the
|-> (##1 consequent)[*n]
module m;
bit[1:0] o_fll_sar_eoc, i_fll_unlock_prog;
bit o_fll_inc, o_fll_lock, sampled_monclk, i_en_fll, fll_dec;
// 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 two positive edge of fll_inc or fll_dec (**consecutive is not necessary )
//between 1 to 6 clock cycle of sampled_clk**
property p_lock_condition_check_unlock_prog_00; // 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, inc_count=0, dec_count=0) |->
##1 (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
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
//---------------------------------------
//2nd requirement (fll_lock de assertion ) :- FLL lock is de-asserted on detecting of four consecutive
// of o_fll_inc signal or fll_dec signal. here the.
// Note :- 1. for requirement two : positive edge is not needed but consecutive of fll_dec or
// fll_inc is must. 1 to 6 clock cycle is **not required**.
property p_unlock_condition_check_unlock_prog_00_v1; // NOT per requirements
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |->
##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
// does not satisfy "consecutive of fll_dec or fll_inc is must"
!o_fll_lock==(inc_count==4 || dec_count==4)
##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty
// Upon a rose of 0_fll_lock and i_fll_unlock_prog == 2'b00 then
// at anytime thereafter (the ##[1:$]) any 4 sequential occurrence of
// o_fll_inc or 4 sequential occurrence of fll_dec the o_fll_lock==0 at that 4th occurrence
property p_unlock_condition_check_unlock_prog_00_v2; //One option
// int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00) |->
first_match(##[1:$] (o_fll_inc==1)[*4] or (fll_dec==1)[*4]) ##0 !o_fll_lock;
// ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
// does not satisfy "consecutive of fll_dec or fll_inc is must"
// !o_fll_lock==(inc_count==4 || dec_count==4)
// ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty
// If the "at anytime" is constrained to "n" static cycles,
let n=10;
// Upon a rose of 0_fll_lock and i_fll_unlock_prog == 2'b00 then
// at anytime thereafter (the ##[1:$]) any 4 sequential occurrence of
// o_fll_inc or 4 sequential occurrence of fll_dec the o_fll_lock==0 at that 4th occurrence
property p_unlock_condition_check_unlock_prog_00; //One option
// int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00) |->
first_match(##[1:$] (o_fll_inc==1)[*4] or (fll_dec==1)[*4] intersect 1'b1[*n]) ##0 !o_fll_lock;
// ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
// does not satisfy "consecutive of fll_dec or fll_inc is must"
// !o_fll_lock==(inc_count==4 || dec_count==4)
// ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty
endmodule
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
// 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]);
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]);
// ^^^
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?
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.
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
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)
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])
Looking at the waveforms, I see the antecedent being true for many cycles. ( o_fll_sar_eoc == 1 && i_fll_unlock_prog == 2’b01, inc_count=0, dec_count=0 )
That creates multiple successful attempts, and each attempt triggers its own consequent thread that is independent of other threads. That can provide unexpected failures.
See my paper - Understanding the SVA Engine. Verification Horizons - July 2020 | Verification Academy
Try ($rose(o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2’b01[/b], inc_count=0, dec_count=0 )
It is very difficult for someone (me included) to debug an assertion without understanding the complete image. My best advice is to run your assertion in a small testbench environment with the simulation tool in a debug mode. In that mode, you can view the threads and the local variables and understand why the tool is telling of a pass or failure. The tool (if correct, most likely so) will do what SVA expresses, not what you wish. Thus you need to understand why SVA is behaving this way.
Assertion never got triggered Check your testbench. Test your assertions separately in a small testbench.
