implication operators in sva

R

ramnarayan

Guest
Hi,
what is the use of "|-> and |=>" in SVA even we have ##0 and
##1.
Ex: seq1 |-> seq2

seq1 ##0 seq2
which pattern should we use and why ?
 
On 6 Nov 2006 22:07:43 -0800, "ramnarayan"
<ramlh2004@gmail.com> wrote:

what is the use of "|-> and |=>" in SVA even we have ##0 and
##1.
Ex: seq1 |-> seq2

seq1 ##0 seq2
which pattern should we use and why ?
Click to expand...
Consider the APB bus protocol. It has two control signals PENABLE
and PSEL. A cycle occupies two clock periods:

clock1: PENABLE = 0, PSEL = 1
clock2: PENABLE = 1, PSEL = 1

We can detect a cycle using a sequence like this:

sequence APB_cycle;
PSEL & ~PENABLE ##1 PENABLE & PSEL;
endsequence

This is good. We can "cover" this sequence, so that the simulator
counts how many times it happens. We can even use the sequence to
trigger other verification activity.

However, suppose we want to CHECK the bus cycle using an
assertion. If we do this...

assert property (APB_cycle);

then the assertion will fail, often, because it succeeds only on
clocks where the APB_cycle sequence completes successfully;
there will be many, many clocks that are either idle or are the
first clock of a cycle, and the assertion will fail at these points.

Instead, we want to say "If clock1 of the cycle occurs, then
check that clock2 occurs correctly." We can do this using
implication:

property APB_works;
PSEL & ~PENABLE |=> PENABLE & PSEL;
endproperty
assert property (APB_works);

The implication operator works like this:
- if the left-hand side sequence ("antecedent") fails,
then nothing interesting has happened. We don't
want the assertion to fail, but we don't want to
record a success either. We call this a "vacuous success".
- If the left-hand side sequence succeeds, we then move
on to checking the right-hand side ("consequent") sequence.
If the consequent fails, then a bus cycle began but completed
incorrectly and the property fails; the assertion will throw
an error. If the consequent succeeds, then a bus cycle
began and completed successfully; the assertion will
not error, and a simulator will probably record the success
in a coverage database.

As you are probably aware, the *timing* of |=> is the same
as ##1, and the timing of |-> is the same as ##0.

There's more to this story - for example, what does it mean
to say A|=>B|=>C - but this will do for a start...
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
 
ramnarayan wrote:
Hi,
what is the use of "|-> and |=>" in SVA even we have ##0 and
##1.
Ex: seq1 |-> seq2

seq1 ##0 seq2
which pattern should we use and why ?
Click to expand...
To clarify a bit more, let's re-write them in Verilog.

seq1 #0 seq2 corresponds to verilog process:

always @(posedge clk)
if !(seq1 & seq2) <assert error>;


seq1 |-> seq2 corresponds to:

always @(posedge clk)
if (seq1)
if (seq2) <cover sucess>;
else <assert error>;


In terms of checking functionality, both processes are the same.
However, coverage collection is meaningful for the second one only.

Regards,
-Alex
 
Hi Alex,
thanks 4 ur suggestion but i have got one more idea that why
we should use implication operators instead of cycle delay.
lets take an example
seq1 ##0 seq2
In this case if seq1 is matched but seq2 is not matched then it is
interpreted as assertion fail so through this i can't recognize that
which sequence has failed and i have to look both sequences that is
time consuming but in case of implication operator if assertion fails
then no need to look into the seq1.that saves the time.

Alex wrote:
ramnarayan wrote:
Hi,
what is the use of "|-> and |=>" in SVA even we have ##0 and
##1.
Ex: seq1 |-> seq2

seq1 ##0 seq2
which pattern should we use and why ?

To clarify a bit more, let's re-write them in Verilog.

seq1 #0 seq2 corresponds to verilog process:

always @(posedge clk)
if !(seq1 & seq2) <assert error>;


seq1 |-> seq2 corresponds to:

always @(posedge clk)
if (seq1)
if (seq2) <cover sucess>;
else <assert error>;


In terms of checking functionality, both processes are the same.
However, coverage collection is meaningful for the second one only.

Regards,
-Alex
Click to expand...
 
Hi Jonathan,

I understand.

So "a |=> b" is equal to "a |-> ##1 b", is it right? Thanks!

Best regards,
Davy

Jonathan Bromley wrote:
On 12 Nov 2006 18:11:19 -0800, "Davy" <zhushenli@gmail.com> wrote:

Hi Jonathan,

About the "|->" and "|=>" implication, how about I want more than one
clock implication?

Do you mean "if A happens, then B should happen 4 clocks later" ?
That can easily be described...

A |-> ##4 B;

or

A |=> ##3 B;
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
 
On 13 Nov 2006 17:15:26 -0800, "Davy"
<zhushenli@gmail.com> wrote:


So "a |=> b" is equal to "a |-> ##1 b", is it right?
Click to expand...
Yes, by definition.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
 
Hi,Jonathan ,

As you mentioned previously, there is "seq_a |-> seq_b |-> seq_c" in
SVA.

Is " seq_a |-> seq_b |-> seq_c " equal to
" (seq_a and seq_b) |-> seq_c "?

Or shall we need only care the last implication (|-> or |=>), thanks!

Best regards,
Davy

Jonathan Bromley wrote:
On 13 Nov 2006 17:15:26 -0800, "Davy"
zhushenli@gmail.com> wrote:


So "a |=> b" is equal to "a |-> ##1 b", is it right?

Yes, by definition.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
 
Davy,
They are quite different. The "and" you refer to is "temporal anding"
not "boolean and" (even if it is, it won't match nested implications).
A temporal "and" gets satisfied if:

Both seq_q, seq_b start at the same time
The end time of this "composite sequence" is end time of last ending
sequence. i.e. say:

seq_b and seq_a starts at clk_10

seq_a ends at clk_20
seq_b ends at clk_30

Then the composite sequence shall end at clk_30

A nested implication is just that - like a nested if in procedural
code.

HTH
Ajeetha, CVC
www.noveldv.com

Davy wrote:
Hi,Jonathan ,

As you mentioned previously, there is "seq_a |-> seq_b |-> seq_c" in
SVA.

Is " seq_a |-> seq_b |-> seq_c " equal to
" (seq_a and seq_b) |-> seq_c "?

Or shall we need only care the last implication (|-> or |=>), thanks!

Best regards,
Davy

Jonathan Bromley wrote:
On 13 Nov 2006 17:15:26 -0800, "Davy"
zhushenli@gmail.com> wrote:


So "a |=> b" is equal to "a |-> ##1 b", is it right?

Yes, by definition.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
 
Hi Ajeetha,

Thanks a lot!
Shall I visualize "seq_a |-> seq_b |-> seq_c " as
[1] "seq_a |-> (seq_b |-> seq_c)"
or
[2] "(seq_a |-> seq_b) |-> seq_c"

Is [1] and [2] different?

Best regards,
Davy

Ajeetha wrote:
Davy,
They are quite different. The "and" you refer to is "temporal anding"
not "boolean and" (even if it is, it won't match nested implications).
A temporal "and" gets satisfied if:

Both seq_q, seq_b start at the same time
The end time of this "composite sequence" is end time of last ending
sequence. i.e. say:

seq_b and seq_a starts at clk_10

seq_a ends at clk_20
seq_b ends at clk_30

Then the composite sequence shall end at clk_30

A nested implication is just that - like a nested if in procedural
code.

HTH
Ajeetha, CVC
www.noveldv.com

Davy wrote:
Hi,Jonathan ,

As you mentioned previously, there is "seq_a |-> seq_b |-> seq_c" in
SVA.

Is " seq_a |-> seq_b |-> seq_c " equal to
" (seq_a and seq_b) |-> seq_c "?

Or shall we need only care the last implication (|-> or |=>), thanks!

Best regards,
Davy

Jonathan Bromley wrote:
On 13 Nov 2006 17:15:26 -0800, "Davy"
zhushenli@gmail.com> wrote:


So "a |=> b" is equal to "a |-> ##1 b", is it right?

Yes, by definition.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
 
Davy wrote:
Hi Ajeetha,

Thanks a lot!
Shall I visualize "seq_a |-> seq_b |-> seq_c " as
[1] "seq_a |-> (seq_b |-> seq_c)"
or
[2] "(seq_a |-> seq_b) |-> seq_c"

Is [1] and [2] different?
Click to expand...
[1] and [2] are little bit different.
For example, seq_a matches, but seq_b and seq_c don't match till the
end of simulation.
In this case, property [1] will have "pending" status at the end of
simulation, while property [2] will succeed vacuously , without the
"pending" status.
Some simulators may turn "pending" properties into the "failed" ones at
the end of simulation. This requires completion of all pending
properties till the end of simulation.

Please see discussion about "unbounded properties" in verification
guild:

http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=562

Regards,
-Alex
 
Hi Jonathan,

About the "|->" and "|=>" implication, how about I want more than one
clock implication? Shall I walk around when encounter it? Thanks!

Best regards,
Davy

Jonathan Bromley wrote:
On 6 Nov 2006 22:07:43 -0800, "ramnarayan"
ramlh2004@gmail.com> wrote:

what is the use of "|-> and |=>" in SVA even we have ##0 and
##1.
Ex: seq1 |-> seq2

seq1 ##0 seq2
which pattern should we use and why ?

Consider the APB bus protocol. It has two control signals PENABLE
and PSEL. A cycle occupies two clock periods:

clock1: PENABLE = 0, PSEL = 1
clock2: PENABLE = 1, PSEL = 1

We can detect a cycle using a sequence like this:

sequence APB_cycle;
PSEL & ~PENABLE ##1 PENABLE & PSEL;
endsequence

This is good. We can "cover" this sequence, so that the simulator
counts how many times it happens. We can even use the sequence to
trigger other verification activity.

However, suppose we want to CHECK the bus cycle using an
assertion. If we do this...

assert property (APB_cycle);

then the assertion will fail, often, because it succeeds only on
clocks where the APB_cycle sequence completes successfully;
there will be many, many clocks that are either idle or are the
first clock of a cycle, and the assertion will fail at these points.

Instead, we want to say "If clock1 of the cycle occurs, then
check that clock2 occurs correctly." We can do this using
implication:

property APB_works;
PSEL & ~PENABLE |=> PENABLE & PSEL;
endproperty
assert property (APB_works);

The implication operator works like this:
- if the left-hand side sequence ("antecedent") fails,
then nothing interesting has happened. We don't
want the assertion to fail, but we don't want to
record a success either. We call this a "vacuous success".
- If the left-hand side sequence succeeds, we then move
on to checking the right-hand side ("consequent") sequence.
If the consequent fails, then a bus cycle began but completed
incorrectly and the property fails; the assertion will throw
an error. If the consequent succeeds, then a bus cycle
began and completed successfully; the assertion will
not error, and a simulator will probably record the success
in a coverage database.

As you are probably aware, the *timing* of |=> is the same
as ##1, and the timing of |-> is the same as ##0.

There's more to this story - for example, what does it mean
to say A|=>B|=>C - but this will do for a start...
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
 
On 12 Nov 2006 18:11:19 -0800, "Davy" <zhushenli@gmail.com> wrote:

Hi Jonathan,

About the "|->" and "|=>" implication, how about I want more than one
clock implication?
Click to expand...
Do you mean "if A happens, then B should happen 4 clocks later" ?
That can easily be described...

A |-> ##4 B;

or

A |=> ##3 B;
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
 
Hi Alex,

Thanks a lot!
As you said, I guess "seq_a |-> seq_b |-> seq_c" is not equal to "seq_a
|-> (seq_b |-> seq_c)" and "(seq_a |-> seq_b) |-> seq_c".

I guess "seq_a |-> seq_b |-> seq_c" will lead to two "pending", is it
right?

Best regards,
Davy

Alex wrote:
Davy wrote:
Hi Ajeetha,

Thanks a lot!
Shall I visualize "seq_a |-> seq_b |-> seq_c " as
[1] "seq_a |-> (seq_b |-> seq_c)"
or
[2] "(seq_a |-> seq_b) |-> seq_c"

Is [1] and [2] different?

[1] and [2] are little bit different.
For example, seq_a matches, but seq_b and seq_c don't match till the
end of simulation.
In this case, property [1] will have "pending" status at the end of
simulation, while property [2] will succeed vacuously , without the
"pending" status.
Some simulators may turn "pending" properties into the "failed" ones at
the end of simulation. This requires completion of all pending
properties till the end of simulation.

Please see discussion about "unbounded properties" in verification
guild:

http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=562

Regards,
-Alex
Click to expand...
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top