Can we assign a variable inside assertion?
In reply to christin kripa John:
Kindly elaborate - strictly speaking the answer is NO, but there are work-arounds if you have to really do this.
If you can elaborate on why you want to do this, maybe we can help.
Srini
In reply to Srini @ CVCblr.com:
property Assert_IICDL_1;
// int n;// assigning the variable here is not working
// n=`CORE.iicdl[4:0];
@(posedge tb_top.dut_u1.clkp) disable iff (tb_top.dut_u1.rst)
$fell(`DUT_TOP.sc_tei_n) ##[0:$] $rose(`DUT_TOP.sc_rxd_n) |-> ##n $fell(`DUT_TOP.sc_txd_n);//can we declare it like this?
endproperty
IICDL_1: assert property (Assert_IICDL_1)
else
$error(“Failed”);
In reply to christin kripa John:
A local variable can be used inside assertion to store some value at particular time state.
As it is local it’s visibility is inside that assertion only.
Following example is there in SV LRM :
Suppose you have 5 pipeline stages. and data_in keep on varying at every clock cycle if data_in_valid is high. You need to write a check for every valid_data_in data_out = data_in+1 at the output of the pipeline.
property pipeline_out_check;
int local_var ;
@(posedge clk) data_in_valid, local_var = data_in |-> ##5 data_out == (local_var+1)
endproperty
assert pipeline_out_check ;
Here for each data_in_valid a seperate thread got forked. For that thread local_var is the present data_in that is stored in local_var. At the end of the thread data_out is checked to be equal to the local_var that is actually equal to the value of data_in 5 cycles before.
The key is to compare data_out to the data_in that was valid 5 cycles before not present data_in.
In reply to christin kripa John:
We can’t directly have a variable delay.
But we can use local variable to implement that:
property Assert_IICDL_1;
int delay;
@(posedge tb_top.dut_u1.clkp) disable iff (tb_top.dut_u1.rst)
$fell(`DUT_TOP.sc_tei_n) ##[0:$] ($rose(`DUT_TOP.sc_rxd_n), delay = `CORE.iicdl[4:0]) |-> (delay >= 0,delay = delay-1'b1)[*0:$] ##1 (delay == 0) ##0 $fell(`DUT_TOP.sc_txd_n);
endproperty
In reply to christin kripa John:
You can declare local variables and make assignments to those variables within the assertion (See 6.10 Local variables in the 1800-2017 LRM).
You can make assignments to variables outside the assertion indirectly by calling a function as part of a sequence matching (16.11 Calling subroutines on match of a sequence). Note that you do not see the effect of any assignment until after the next sample of that variable.
In general, this practice should be avoided as assertions are supposed to be passive.
In reply to dave_59:
The easiest way to handle dynamic delays & repeas is to use the package that I wrote after advisement from this forum.
http://SystemVerilog.us/vf/sva_delay_repeat_pkg.sv
http://SystemVerilog.us/vf/sva_delay_repeat.sv
package sva_delay_repeat_pkg;
sequence dynamic_repeat(q_s, count);
int v=count;
(1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
endsequence
sequence dynamic_delay(count);
int v;
(1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
endsequence
endpackage
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.
In reply to Anurag Gupta:
Thanks.Tried with this piece of code.
THere is no more compilation issue ,but the assertion is failing.
The delay portion (that is supposed to be 3, wen IICDL value is 3, is not hitting and it hits wen value=5 ,which is a fail)
In reply to Anurag Gupta:
property Assert_IICDL_1;
int delay;
@(posedge tb_top.dut_u1.clkp) disable iff (tb_top.dut_u1.rst)
fell(`DUT_TOP.sc_tei_n) ##[0:] ($rose(DUT_TOP.sc_rxd_n), delay = CORE.iicdl[4:0]) |-> ((delay >= 0,delay = delay-1’b1,$display(time, "\t delay %0d",delay)) [*0:] ##1 (delay == 0)) ##0 $rose(`DUT_TOP.sc_txd_n);
endproperty
IICDL_1: assert property (Assert_IICDL_1)
else
$error(“Failed”);
could develop like this…but still the assertion is not hitting
In reply to christin kripa John:
There are several issues with your property that is of the form:
property Assert_IICDL_1;
int delay;
@(posedge clk) disable iff (rst)
$fell(a) ##[0:$] ($rose(b), delay = r) |->
((delay >= 0,delay = delay-1'b1) [*0:$]
##1 (delay == 0)) ##0 c;
endproperty
- The antecedent is multithreaded because of the ##[0:$], and for the assertion to succeed, al threads (the infinity) must be tested for success. It can fail though. The fix: a first_match().
- The end condition (delay == 0) for the reapeat should be (delay <= 0)
I still recommend the use of my package. Below is updated code using “a” “b” c"c" istead of your variables.
package sva_delay_repeat_pkg;
sequence dynamic_repeat(q_s, count);
int v=count;
(1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
endsequence
sequence dynamic_delay(count);
int v;
(1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
endsequence
endpackage
import uvm_pkg::*; `include "uvm_macros.svh"
import sva_delay_repeat_pkg::*;
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b, c=1, rst;
int r=3;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
property Assert_IICDL_1; // ORIGINAL BAD Property
int delay;
@(posedge clk) disable iff (rst)
$fell(a) ##[0:$] ($rose(b), delay = r) |-> // ** NEED a first_match() in antecedent **
((delay >= 0,delay = delay-1'b1,$display($time, "\t delay %0d",delay)) [*0:$]
##1 (delay <= 0)) ##0 c;
endproperty
IICDL_1: assert property (Assert_IICDL_1)
else
$error("Failed");
property A_IICDL_OK;
int delay;
@(posedge clk) disable iff (rst)
first_match($fell(a) ##[0:$] ($rose(b), delay = r)) |->
((delay >= 0,delay = delay-1'b1,$display($time, "\t delay %0d",delay)) [*0:$]
##1 (delay <= 0)) ##0 c;
endproperty
IICDL_OK: assert property (A_IICDL_OK);
// USING THE delay and repeat package.
ap_IIC: assert property(@ (posedge clk) disable iff (rst)
first_match($fell(a) ##[0:$] ($rose(b), $display($time, "\t delay %0d",r))) |->
dynamic_delay(r) ##0 c);
initial begin
repeat(100) begin
@(posedge clk); #2;
if (!randomize(a, b, c) with
{ a dist {1'b1:=1, 1'b0:=1};
b dist {1'b1:=1, 1'b0:=2};
c dist {1'b1:=1, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
#1 r=0;
repeat(100) begin
@(posedge clk); #2;
if (!randomize(a, b, c) with
{ a dist {1'b1:=1, 1'b0:=1};
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
$stop;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
October 2013 | Volume 9, Issue 3 | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
In reply to ben@SystemVerilog.us:
A correction and why I recommend that you use my package.
In the property below, there is a need for a first_match() because without it, if c==0, there will be another repeat count.
Another reason for the use of the package is that the local variable is within the sequence dynamic_delay(count) or sequence dynamic_repeat(q_s, count), thus there is no need to declare a property and then an sn statement, you can go directly to the assertion statement, making it more compact. Below is the corrected code
property A_IICDL_NotOK; // THIS IS IN ERROR, there is a need for a first_match()
int delay;
@(posedge clk) disable iff (rst)
first_match($fell(a) ##[0:$] ($rose(b), delay = r)) |->
((delay >= 0,delay = delay-1'b1,$display($time, "\t delay %0d",delay)) [*0:$]
##1 (delay <= 0)) ##0 c;
endproperty
IICDL_NotOK: assert property (A_IICDL_NotOK);
property A_IICDL_OK;
int delay;
@(posedge clk) disable iff (rst)
first_match($fell(a) ##[0:$] ($rose(b), delay = r)) |->
first_match((delay >= 0,delay = delay-1'b1,$display($time, "\t delay %0d",delay)) [*0:$]
##1 (delay <= 0)) ##0 c;
endproperty
IICDL_OK: assert property (A_IICDL_OK);
// A BETTER WAY
// USING THE delay and repeat package.
ap_IIC: assert property(@ (posedge clk) disable iff (rst)
first_match($fell(a) ##[0:$] ($rose(b), $display($time, "\t delay %0d",r))) |->
dynamic_delay(r) ##0 c);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
October 2013 | Volume 9, Issue 3 | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
In reply to ben@SystemVerilog.us:
Hi Ben,
If we don’t use the first_match in the consequent side the property anyway will fail right even though c==0
Please correct me if i am wrong.
In reply to sudharshan:
If we don’t use the first_match in the consequent side the property anyway will fail right even though c==0
The consequent can only SUCCEED in 2 cases because of the (delay <= 0) (less than or equal cases). If c==0, because of the OR of all the possible threads, the test of all the threads will be done (till the end of simulation) The assertion will not fail, it can never fail.
You need the first_match() to exclude all other threads that can never succeed.
a |-> // without the first_match()
(delay >= 0,delay = delay-1'b1) [*0:$] ##1 (delay <= 0)) ##0 c; CS==because
// Assuming delay==3, the consequent is same as:
// Notation: (F==false; T==true)
((3 >= 0) [*0] ##1 (2<= 0) ##0 c) OR // F; (2<= 0) is false
((2 >= 0) [*1] ##1 (1<= 0) ##0 c) OR // F; (2 >= 0)[*1 ]==T but (1<= 0) is false
((1 >= 0) [*2] ##1 (0<= 0) ##0 c) OR // "c"; (1 >= 0)[*2], (0<= 0)==T, T if c==1, else continue
((0 >= 0) [*3] ##1 (-1<= 0)##0 c) OR // "c"; (0 >= 0)[*3]==T,(-1<= 0)==T, T if c==1, else continue
((-1 >= 0)[*4] ##1 (-2<= 0)##0 c) OR // F because (-1 >= 0) [*4]==F
.. F F F F..... F
( (-n >= 0) [*n ] ##1 (-n-1 <= 0) ##0 c ) OR // F because (-n >= 0) [*n ]==F
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue - SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
[i]In reply to ben@SystemVerilog.us:[since
if we use delay=0 then there is no need for first_match in consequent side am i correct.
is there any reason for not using The end condition (delay == 0) for the reapeat should be (delay <= 0)
please let me know
In reply to sudharshan:
if we use delay=0 then there is no need for first_match in consequent side am i correct.
You still need the first_match, unless c==1 before (delay >= 0,delay = delay-1’b1) goes negative. If “c” is zero, the assertion will not fail because it is looking for a success (the OR).
is there any reason for not using The end condition (delay == 0) for the reapeat should be (delay <= 0)
no, delay ==0 is ok
|-> // without the first_match()
(delay >= 0,delay = delay-1'b1) [*0:$] ##1 (delay == 0)) ##0 c; CS==because
// Assuming delay==3, the consequent is same as:
// Notation: (F==false; T==true)
((3 >= 0) [*0] ##1 (2== 0) ##0 c) OR // F; (2<= 0) is false
((2 >= 0) [*1] ##1 (1== 0) ##0 c) OR // F; (2 >= 0)[*1 ]==T but (1== 0) is false
((1 >= 0) [*2] ##1 (0== 0) ##0 c) OR // "c"; (1 >= 0)[*2], (0== 0)==T, T if c==1, else continue
((0 >= 0) [*3] ##1 (-1== 0)##0 c) OR // "c"; (0 >= 0)[*3]==T,(-1== 0)==F,
((-1 >= 0)[*4] ##1 (-2== 0)##0 c) OR // F because (-1 >= 0) [*4]==F
.. F F F F..... F
( (-n >= 0) [*n ] ##1 (-n-1 == 0) ##0 c ) OR // F because (-n >= 0) [*n ]==F