assertion to test 3 signals where when A goes high it should for B or C to go high and checking should continue till a is high
property p;
@(posedge Clk) disable iff((Reset==0)||($isunknown(Reset)))
A |-> (B || C) throughout(A==1) until (A==0);
endproperty
P_check: assert property(p) else
`uvm_error(“assertions”, $sformatf("UVM_Error on assertion " ))
please let me know throughout and until use is good and cane be done.
secondly assertion will pass?
In reply to bhajanpreetsinght:
If I have to really think about it because of the definition of the until, then I would rather find something that it clear and easier to read.
A |-> (B || C) throughout !A[->1]; // B||C ==1 when A==0
A |-> (B || C)[*1:$] ##1 !A; // B||C ==don’t care when A==0
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
If I have to really think about it because of the definition of the until, then I would rather find something that it clear and easier to read.
A |-> (B || C) throughout !A[->1]; // B||C ==1 when A==0( can you explain more what this will check and how we control this)
A |-> (B || C)[*1:$] ##1 !A; // B||C ==don’t care when A==0
( req you elaborate on this why we use B||c = don’t care ,we care it should be high we are checking till the period is A is high and stop if A goes low and B and C is high.
Hi Ben,
Thanks for the reply but we need to keep on checking value of B || c to be high throughout A is high and stop if only A goes low and they donot get the value of B || c to be high. Can you comment on this
In reply to bhajanpreetsinght:
In reply to ben@SystemVerilog.us:
( req you elaborate on this why we use B||c = don’t care ,we care it should be high we are checking till the period is A is high and stop if A goes low and B and C is high.
Hi Ben,
Thanks for the reply but we need to keep on checking value of B || c to be high throughout A is high and stop if only A goes low and they donot get the value of B || c to be high. Can you comment on this
so basically assertion fails if a is high and we donot get either b or c is high in the time period of A is high and if we get either of them to be high in the time period of a is high the assertion passes .
In reply to bhajanpreetsinght:
In reply to ben@SystemVerilog.us:
( req you elaborate on this why we use B||c = don’t care ,we care it should be high we are checking till the period is A is high and stop if A goes low and B and C is high.
Hi Ben,
Thanks for the reply but we need to keep on checking value of B || c to be high throughout A is high and stop if only A goes low and they donot get the value of B || c to be high. Can you comment on this
so basically assertion fails if a is high and we donot get either b or c is high in the time period of A is high and if we get either of them to be high in the time period of a is high the assertion passes .
In reply to bhajanpreetsinght:
In reply to bhajanpreetsinght:
so basically assertion fails if a is high and we donot get either b or c is high in the time period of A is high and if we get either of them to be high in the time period of a is high the assertion passes .
please rewrite the code for that would help
In reply to bhajanpreetsinght:
@(posedge clk) $rose(c) |-> ((a||c) throughout(c==1)) until (c==0)
which also can be rewritten as
@(posedge clk) $rose(c) |-> ((a||c) && (c==1)) until (c==0)
it can be further rewritten as
@(posedge clk) rose(c) |-> ((a||c) && (c==1))[*0:] ##1 (c==0)
I suggest that you try various tests with different assertions; this will help in your
understanding of these operators. Also, read my paper Reflections on Users’ Experiences with SVA, part 2
Addresses the usage of these four relationship operators: throughout, until, intersect, implies
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
@(posedge clk) $rose(c) |-> ((a||c) throughout(c==1)) until (c==0)
which also can be rewritten as
@(posedge clk) $rose(c) |-> ((a||c) && (c==1)) until (c==0)
it can be further rewritten as
@(posedge clk) rose(c) |-> ((a||c) && (c==1))[*0:] ##1 (c==0)
I suggest that you try various tests with different assertions; this will help in your
understanding of these operators. Also, read my paper Reflections on Users’ Experiences with SVA, part 2
Reflections on Users’ Experiences with SVA, Part II
Addresses the usage of these four relationship operators: throughout, until, intersect, implies
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh
Hi Ben,
I am asking a very dificult question
i know the concept of your dynamic delay which states like below
(count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);// in my case consider the count variable to be clkgate_hysteresis which is [11:0] variable .
now my antecedent is dependent on 5 variable which is
a && b && c && d && e throughout count|-> (count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0)##0 final variable =0;
so this assertion I am checking value a b c d e should be high throughout count which here count represent clock edges number which will be given dynamic and same clockedge numbers will be used as consequent to check the final variable is 0 after that many clock edge numbers.
Suppose clockedge number ='h10 so decimal 16, so assertion means till 16 clockedge a b c d e should be high and after that we would check the consequent which will trigger at same clock edge number 16 to check final variable is 0 and should reamin 0 atleast for 3 clock edge.
Request you to help with the code I have written pseudo cod eto please help me complete this assertion
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
@(posedge clk) $rose(c) |-> ((a||c) throughout(c==1)) until (c==0)
which also can be rewritten as
@(posedge clk) $rose(c) |-> ((a||c) && (c==1)) until (c==0)
it can be further rewritten as
@(posedge clk) rose(c) |-> ((a||c) && (c==1))[*0:] ##1 (c==0)
I suggest that you try various tests with different assertions; this will help in your
understanding of these operators. Also, read my paper Reflections on Users’ Experiences with SVA, part 2
Reflections on Users’ Experiences with SVA, Part II
Addresses the usage of these four relationship operators: throughout, until, intersect, implies
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh
Hi Ben,
I am asking a very dificult question
i know the concept of your dynamic delay which states like below
(count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);// in my case consider the count variable to be clkgate_hysteresis which is [11:0] variable .
now my antecedent is dependent on 5 variable which is
a && b && c && d && e throughout count|-> (count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0)##0 final variable =0;
so this assertion I am checking value a b c d e should be high throughout count which here count represent clock edges number which will be given dynamic and same clockedge numbers will be used as consequent to check the final variable is 0 after that many clock edge numbers.
Suppose clockedge number ='h10 so decimal 16, so assertion means till 16 clockedge a b c d e should be high and after that we would check the consequent which will trigger at same clock edge number 16 to check final variable is 0 and should reamin 0 atleast for 3 clock edge.
Request you to help with the code I have written pseudo cod eto please help me complete this assertion
In reply to bhajanpreetsinght:
// Requirements should be defined by an implementation, and this is what I see.
// I am struggling with your requirements. This is what I understand:
// 1) a, b, c, d, e must remain hi for a duration defined by a variable.
// 2) At the end of this duration of cycles, signal w should reamin deasserted (i.e., w==0) for 1 to 3 cycles.
// [Ben] This test is to be done for any string of a, b, c, d, e that remains hi for that period of cycles.
// 3) If a, b, c, d, e do not remain hi for the dynamically specified duration,
// this is a don't care situation.
//
//[Ben] This type of spec appears to be a sync pattern
/* I intend to use the dynamic repeat from the package
//----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Implements a_sequence[*count]
// Application: $rose(a) |-> sq_rpt_simple_count(sq_1, d1)
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)."
*/
module m;
import sva_delay_repeat_range_pkg::*;
bit clk, a, b, c, d, e, w;
int duration;
sequence q_abcde; @(posedge clk) a && b && c && d && e; endsequence
assert property(@(posedge clk)
sq_rpt_simple_count(q_abcde,duration) |-> w==0[*1:3]);
endmodule
Ben
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
// Requirements should be defined by an implementation, and this is what I see.
// I am struggling with your requirements. This is what I understand:
// 1) a, b, c, d, e must remain hi for a duration defined by a variable.
// 2) At the end of this duration of cycles, signal w should reamin deasserted (i.e., w==0) for 1 to 3 cycles.
// [Ben] This test is to be done for any string of a, b, c, d, e that remains hi for that period of cycles.
// 3) If a, b, c, d, e do not remain hi for the dynamically specified duration,
// this is a don't care situation.
//
//[Ben] This type of spec appears to be a sync pattern
/* I intend to use the dynamic repeat from the package
//----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Implements a_sequence[*count]
// Application: $rose(a) |-> sq_rpt_simple_count(sq_1, d1)
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)."
*/
module m;
import sva_delay_repeat_range_pkg::*;
bit clk, a, b, c, d, e, w;
int duration;
sequence q_abcde; @(posedge clk) a && b && c && d && e; endsequence
assert property(@(posedge clk)
sq_rpt_simple_count(q_abcde,duration) |-> w==0[*1:3]);
endmodule
Ben
Hi Ben,
The sequence is not working properly like
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
as it is not reading the dynamic delay , suppose dynamic delay=``h10 then what will be 16 clock edge it is not taking it does not gets triggered at all
In reply to bhajanpreetsinght:
It is working, it is just that the evaluation of the sequence q_abcde for each attempt is
delayed by duration. Consider a static delay of 2, then
sq_rpt_simple_count(q_abcde,duration) |-> w==0[*1:3])
// is equivalent to
##2 a |-> w==0[*1:3])
// for attempt1 at t0 a is not evaluated
// for attempt1 at t1 (the ##1) a is not evaluated
// for attempt2 at t1 a is not evaluated
// for attempt1 at t2 (the ##2) a is evaluated, w==0[*1:3]) starts now
// for attempt2 at t2 (the ##1) a is not evaluated
// for attempt3 at t2 a is not evaluated
...
Again, you are missing SVA concepts,
Read my papers, particularly the one about the modeling of SVA.