/*
Signal (a) and Signal (b).
How do you write this assertion?
Thanks,
JeffD
In reply to dvuvmsv:
ap_a2b: assert property( @(posedge clk) a |-> ##[2:5] b);
// 2. signal (a) can be asserted 3 times consecutively before signal b asserts,
// Before signal (a) assert 4th time, signal (b) should assert at least once
// Meaning, difference in the number of signal (a) and signal (b) should not exceed 3.
ap_3athenb: assert property(@(posedge clk) a[*1:3] |-> b);
// Not a, aa, or aaa then another a and a&&b
ap_no3q_ab: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
I believe that your first “a” should be $rose(a) or an “a” ended with a “start”.
Let me know if this works for you.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh
In reply to ben@SystemVerilog.us:
Hi Ben,
Still getting some failures with valid a and b.
a2 - EDA Playground
Did not follow the third assertion
ap_no3q_ab: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
Thanks,
JeffD
In reply to dvuvmsv:
The Assertions are correct, but you have to understand what they mean and make the necessary
adjustments to do what you really need to specify.
ap_a2b: assert property( @(posedge clk) a |-> ##[2:5] b);
// Above states that at every attempt (the posedge clk) if(a) then within 2 to 5 cycles b==1.
//--------------------
ap_3athenb: assert property(@(posedge clk) a[*1:3] |-> b);
// at every attempt, all 3 threads of the Antecedent and consequent must be true for he Assertion to be true. Thus, for a true you need
a |->b and a[*2] |->b and a[*3] |-> b;
If a==0, that is a vacuous true.
Maybe what you need is just a[*3] |-> b
Or, maybe what you need is
First_match(a[*1:3]) |-> b
Remember, every attempt is separate from other attempts.
------------------------
ap_no3q_ab: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
// Thus says I should never see the sequence of 3 consecutive a
// that is followed at any time later by another a
// in the same time frame of no b's than a b.
//Thus, the following is an error condition because you have 4 a's in 1 1b
// a 1 1 1 0 0 0 0 0 1
// b 0 0 0 0 0 0 0 0 1
// Not a, aa, or aaa then another a and a&&b
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for the code. I used the below stimulus to test the assertion.
I got the following error shown below
initial
forever #5 clk = ~clk;
initial
begin
@(posedge clk);
a=1; b=0;
repeat(3) @(posedge clk);
a=0; b=0;
@(posedge clk);
a=0; b=1;
repeat(3) @(posedge clk);
a=0; b=0;
end
"testbench.sv", 19: tb.ap_3athenb: started at 15ns failed at 15ns
Offending 'b'
"testbench.sv", 19: tb.ap_3athenb: started at 25ns failed at 25ns
Offending 'b'
"testbench.sv", 19: tb.ap_3athenb: started at 35ns failed at 35ns
Offending 'b'
Thanks,
JeffD
In reply to ben@SystemVerilog.us:
In reply to dvuvmsv:
The Assertions are correct, but you have to understand what they mean and make the necessary
adjustments to do what you really need to specify.
ap_a2b: assert property( @(posedge clk) a |-> ##[2:5] b);
// Above states that at every attempt (the posedge clk) if(a) then within 2 to 5 cycles b==1.
//--------------------
ap_3athenb: assert property(@(posedge clk) a[*1:3] |-> b);
// at every attempt, all 3 threads of the Antecedent and consequent must be true for he Assertion to be true. Thus, for a true you need
a |->b and a[*2] |->b and a[*3] |-> b;
If a==0, that is a vacuous true.
Maybe what you need is just a[*3] |-> b
Or, maybe what you need is
First_match(a[*1:3]) |-> b
Remember, every attempt is separate from other attempts.
------------------------
ap_no3q_ab: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
// Thus says I should never see the sequence of 3 consecutive a
// that is followed at any time later by another a
// in the same time frame of no b's than a b.
//Thus, the following is an error condition because you have 4 a's in 1 1b
// a 1 1 1 0 0 0 0 0 1
// b 0 0 0 0 0 0 0 0 1
// Not a, aa, or aaa then another a and a&&b
Ben, Please help me understand.
you mentioned
"
//--------------------
ap_3athenb: assert property(@(posedge clk) a[*1:3] |-> b);
// at every attempt, all 3 threads of the Antecedent and consequent must be true for he Assertion to be true. Thus, for a true you need
a |->b and a[*2] |->b and a[*3] |-> b;
"
so if a is only triggered once before b i.e a |-> b then the assertion ap_3athenb failed ? according LRM a[*1:3] is same as a OR a[*2] OR a[*3]. Does it mean any of a |-> b, a[*2] |->b, a[*3] |-> b in this assertion is true then assertion successes.
THanks
In reply to VE:
Ib the 2 papers mentioned below (see 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 Links_to_papers_books - Google Docs )
True/False: A property is either true or false. There is also the concept of vacuity, and a vacuously true property is considered ‘true’ in the sense that it is not ‘false’.
Consider the following property that has three property threads:
a ##[1:3] b |-> c. For this property to succeed,
a[*1:3] |-> b); // is equivalent to
a[*1] or a[*2] or a[*3] |-> b
so if a is only triggered once before b i.e a |-> b then the assertion ap_3athenb failed ? according LRM a[*1:3] is same as a OR a[*2] OR a[*3]. Does it mean any of a |-> b, a[*2] |->b, a[*3] |-> b in this assertion is true then assertion successes.
The 3 threads are
a[*1] |-> b // of a==1, then b must be 1 or assertion fails
a[*2] |-> b // if a==1 and ##1 a==0, the antecedent is vacuous
// and this thread if vacuously true
a[*3] |-> b / if a==1 and ##1 a==0 and ##2 a==0, the antecedent is vacuous
// and this thread if vacuously true
// Thus, for success you need a, or a##1 a, or a ##1 a ##1 a with b==1
// A vacuous antecedent yields a true (though vacuous) thread.
From my papers:
1 Understanding the SVA Engine Using the Fork-Join Model
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.
2 Reflections on Users’ Experiences with SVA, part 1
Important concepts on EXPRESSING REQUIREMENTS,
Terminology, threads in ranges and repeats in antecedents, multiple antecedents.
I really encourage you to red thru all my papers; they are the results of actual users like you.
BEn
In reply to ben@SystemVerilog.us:
Hi VE or Ben or anyone,
Do you know why I am getting this errors. How to fix the errors
"testbench.sv", 19: tb.ap_3athenb: started at 15ns failed at 15ns
Offending 'b'
"testbench.sv", 19: tb.ap_3athenb: started at 25ns failed at 25ns
Offending 'b'
"testbench.sv", 19: tb.ap_3athenb: started at 35ns failed at 35ns
Offending 'b'
Thanks,
JeffD
In reply to dvuvmsv:
Edaplayground says that I do not have permisison to view this page.
Copy code here, and I’ll look at it with my simulator.
In reply to dvuvmsv:
“testbench.sv”, 19: tb.ap_3athen: started at 15ns failed at 15ns
// 2. signal (a) can be asserted 3 times consecutively before signal b asserts,
// Before signal (a) assert 4th time, signal (b) should assert at least once
// Meaning, difference in the number of signal (a) and signal (b) should not exceed 3.
ap_3athenb: assert property(@(posedge clk) a[*1:3] |-> b);
At 15, 25, and 35 a==1, b==0
a[*1:3] |-> b // is equivalent to
(a |-> b) or
(a[*2] |-> b) or
(a[*3] |-> b)
At every attempt, the first a==1 and b==0
You need to define your requirements.
ap_no3q_ab: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
This assertion says that for every attempt there should NOT be the case when
“a” is repeated 3 times and then followed
by another “a” in the same time frame when “b” is asserted.
Is this what you want?
Hi Ben,
This assertion says that for every attempt there should NOT be the case when
“a” is repeated 3 times and then followed
by another “a” in the same time frame when “b” is asserted.
Yes. Before the 4th “a” arrive, “b” should arrive.
Please help in resolving the assertion failed 3 times.
I put “a” 3 clk cycles and 1 clock gap, then “b” arrive
Assertion should not fail. Not sure why it failed 3 times
Thanks,
JeffD
In reply to dvuvmsv:
My error, apologies. I should have used the within instead of intersect
ap_BAD: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
// aaa...b satisfies (a[*3] ##1 a[->1] intersect b[->1])
// the not of that makes it false
// a a a !a !a b
ap_no3q_ab: assert property(@(posedge clk) $rose(a) |->
a[*1:3] ##1 !a[*] intersect b[->1]);
// Also OK
ap_OK: assert property(@(posedge clk) not(a[*3] ##1 a[->1] within b[->1]));