"|->" implicate and sequence in SVA?

D

Davy

Guest
Hi all,

I have two problem of SystemVerilog Assertion. About property
implication and sequence.

1. Is
//--------
property rule (a,b,c);
@(posedge clk) a |-> b ##1 c;
endproperty
//--------

equal to
//--------
sequence rule;
@(posedge clk) (a&&b) ##1 c;
endsequence
//--------

2. I was told implication can be same or next cycle. Is same cycle
equal to "|->"? And is next cycle equal to "|=>"?

Thanks a lot!

Best regards,
Davy
 
On 10 Nov 2006 18:36:25 -0800, "Davy" <zhushenli@gmail.com> wrote:

Hi all,

I have two problem of SystemVerilog Assertion. About property
implication and sequence.

1. Is
//--------
property rule (a,b,c);
@(posedge clk) a |-> b ##1 c;
endproperty
//--------

equal to
//--------
sequence rule;
@(posedge clk) (a&&b) ##1 c;
endsequence
//--------
Click to expand...
No. See the recent thread "implication operators in sva"
on comp.lang.verilog. Also, you have parameterised the
property but not the sequence.

2. I was told implication can be same or next cycle. Is same cycle
equal to "|->"? And is next cycle equal to "|=>"?
Click to expand...
Yes. See my post in the thread I just mentioned.
--
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.
 
To myself.

##1 is equivalent to @ (posedge clk).
So
##N is equvalent to repeat (N) @ (posedge clk) ?

Thanks!
Davy

Davy wrote:
Hi Jonathan,

Thanks a lot! Now I understand what's "vacuous success" :)

Best regards,
Davy

Jonathan Bromley wrote:
On 10 Nov 2006 18:36:25 -0800, "Davy" <zhushenli@gmail.com> wrote:

Hi all,

I have two problem of SystemVerilog Assertion. About property
implication and sequence.

1. Is
//--------
property rule (a,b,c);
@(posedge clk) a |-> b ##1 c;
endproperty
//--------

equal to
//--------
sequence rule;
@(posedge clk) (a&&b) ##1 c;
endsequence
//--------

No. See the recent thread "implication operators in sva"
on comp.lang.verilog. Also, you have parameterised the
property but not the sequence.

2. I was told implication can be same or next cycle. Is same cycle
equal to "|->"? And is next cycle equal to "|=>"?

Yes. See my post in the thread I just mentioned.
--
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 6 Dec 2006 23:10:27 -0800, "Shenli" <zhushenli@gmail.com> wrote:

To myself.

##1 is equivalent to @ (posedge clk).
So
##N is equvalent to repeat (N) @ (posedge clk) ?
Click to expand...
Where?

In procedural code, you're almost correct:

##N some_clocking_block.some_output_clockvar <= some_value;

is the same as waiting for N clocks before making the clocking drive.

It is NOT quite true that ##1 is equivalent to @(posedge clk),
because of some subtle issues about the updating of input
clockvars and some less subtle issues about default clocking.

In an assertion, you can't use repeat() so the question makes
no sense.
--
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,

Thanks a lot! Now I understand what's "vacuous success" :)

Best regards,
Davy

Jonathan Bromley wrote:
On 10 Nov 2006 18:36:25 -0800, "Davy" <zhushenli@gmail.com> wrote:

Hi all,

I have two problem of SystemVerilog Assertion. About property
implication and sequence.

1. Is
//--------
property rule (a,b,c);
@(posedge clk) a |-> b ##1 c;
endproperty
//--------

equal to
//--------
sequence rule;
@(posedge clk) (a&&b) ##1 c;
endsequence
//--------

No. See the recent thread "implication operators in sva"
on comp.lang.verilog. Also, you have parameterised the
property but not the sequence.

2. I was told implication can be same or next cycle. Is same cycle
equal to "|->"? And is next cycle equal to "|=>"?

Yes. See my post in the thread I just mentioned.
--
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...
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top