I don’t understand your need for the case → i have to write the assertion to check the lock condition ( which you gave me solution above) where a can have 4 value (00, 01, 10,11) based on value of a, number of cycle (between 1 to 6 clock cycle of ref_clk) will change like for 00 it is (1 to 6) and for 01 it is (1 to 8) like so on.
I want to put constraint on o_prog_out_fll [0] so it should only trigger the assertion at first transition on prog_out_fll (0 → 1) so that property should not trigger again when pro_out_fll goes from 0 to 1
In reply to rkg_:
On Q1: You could use a casestatement. However, that really does not simplify things as it makes the assertion more complex, harder to read, and harder to debug. I prefer to have 4 separate assertions; when an error occurs, you would know immediately which of the 4 cases causes the error. The general guidelines on assertions is to write more of smaller assertions than less of complex ones.
On Q2:
bit lock;
always_ff @(posedge sampled_monclk) begin
if($rose (o_prog_out_fll[0])) lock <= 1'b1;
end
property sar_eoc_assertion_check_prpty ;
@(posedge sampled_monclk ) disable iff (!i_en_fll)
$rose (o_prog_out_fll[0])&& !lock && i_en_sar |=> $rose (o_fll_sar_eoc);
endproperty
// 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.