Hi,
I want to write assertion to check the below scenario
if (a == 00) between 1 to 6 clock cycle of ref_clk if two positive edges of dec signal or incr signal is detected then lock is asserted.
I am not sure how to check two positive edges of dec or incr on 1 to 6 clock cycle of ref_clk.
Can i write case statement inside property since a can have 01 , 10, 11 as well so Do need to to write four separate property for (a == 2’b01, 2’b11 …) ?
Could someone help
In reply to rkg_:
Your requirements are not clear; I don’t understand your need for the case.
The caseis a property statement
property_statement ::=
property_expr ;
| case ( expression_or_dist ) property_case_item
{ property_case_item } endcase
| if ( expression_or_dist ) property_expr
[ else property_expr ]
// example
case (cntrl)
2'd0 : a |=> c;
2'd1 : a ##2 b;
2'd2 : a ##1 b |-> c;
default: 0;
endcase
// You could also use the **generate** statement.
// For your model, consider this (again, requirements ??)
/* if (a == 00) between 1 to 6 clock cycle of ref_clk if two positive edges of dec signal
or incr signal is detected then lock is asserted.
I am not sure how to check two positive edges of dec or incr on 1 to 6 clock cycle of ref_clk.
Can i write case statement inside property since a can have 01 , 10, 11 as well so Do need to
to write four separate property for (a == 2'b01, 2'b11 ..) ? */
module m;
bit[1:0] a, lock;
bit ref_clk, inc, dec;
property p_incdec;
int inc_count, dec_count;
(a==2'b00, inc_count=0, dec_count=0) |->
(##1 (1, inc_count+= $rose(inc), dec_count+= $rose(dec)))[*6] ##0
lock==(inc_count==2 || dec_count==2);
endproperty
ap_incdec: assert property(@ (posedge ref_clk) p_incdec );
generate for (genvar i=0; i<=3; i++)
begin
property p_incdeci;
int inc_count, dec_count;
(a==i, inc_count=0, dec_count=0) |->
(##1 (1, inc_count+= $rose(inc), dec_count+= $rose(dec)))[*6] ##0
lock==(inc_count==2 || dec_count==2);
endproperty
ap_incdeci: assert property(@ (posedge ref_clk) p_incdeci);
end
endgenerate
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
Thanks you.
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.
One more doubts :
I have written property below
property sar_eoc_assertion_check_prpty ;
@(posedge sampled_monclk ) disable iff (!i_en_fll)
$rose (o_prog_out_fll[0])&& i_en_sar |=> $rose (o_fll_sar_eoc);
endproperty
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
is it possible ?
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
In reply to ben@SystemVerilog.us:
Hi Ben ,
below line is causing problem
( $rose (o_fll_sar_eoc) , i_fll_unlock_prog == 2’b00, inc_count=0, dec_count=0)
am i doing anything wrong here
case - 1 → is fine
property p_incdec;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( $rose (o_fll_sar_eoc) , inc_count=0, dec_count=0) |->
(##1 (1, inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec)))[*6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
case-2 --is fine
property p_incdec;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( 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)))[*6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
case-3 → getting compilation error
property p_incdec;
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 (1, inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec)))[*6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
do we have limitation number of expression on antecedent ?
In reply to rkg_:
// 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)
In reply to ben@SystemVerilog.us:
I am writing assertion to check the o_fll_lock deassertion.
Specification :- At posedge of o_fll_lock happen , four consecutive of o_fll_inc signal or fll_dec signal detected , o_fll_lock should be de-asserted.
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)))##0
!o_fll_lock==(inc_count==4 || dec_count==4);
endproperty
Problem :- assertion is getting finished before the o_fll_lock de assertion.
Could someone help, what mistake i am doing and how can i print the value of inc_count in my log ?
In reply to rkg_:
You are missing the [*6], also using both |=> ##1, and missing the o_fll_lock de assertion if needed
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; // if needed
endproperty
// note the " |-> ##1 (expr1)[*6] ##0..."
// this is different from
// " |-> (##1 (expr1))[*6] ##0.."
//
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
Hi Ben,
Thank you for reply .
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…" ??
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]);
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
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,
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]
property p_lock_condition_check_unlock_prog_00;
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
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].
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
I have added the waveform for lock assertion and de- assertion :
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
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:
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?