Confusing precedence SVA

[Rob Dekker]

Got an interesting case for SystemVerilog Assertion experts.
I am confused on this.

Consider the following assertion statement :

assert property (@(posedge clk1) a ##1 @(posedge clk2) b |=> c ) ;

The LRM precedence rules seem to indicate that this should be interpreted as this :

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b |=> c) ) ;


where |=> c is thus clocked by 'clk2'....
but then the RHS of ##1 is a sequence, and |=> is only allowed in a property,
so this implementation should cause an error.

Or should it be implemented like this :

assert property (@(posedge clk1) (a ##1 @(posedge clk2) b) |=> c ) ;

where |=> c is thus clocked by 'clk1'...
But is that right ?

Or should it be interpreted differently again ?

Any insights would be greatly appreciated.

 

[Vidyasagar .H Vaddadi]

hello Rob its a good twister i must say.

The property ::
assert property (@(posedge clk1) a ##1 @(posedge clk2)
b |=> c ) ;

shoould be interpreted according to LRM as

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b
|=> c) ) ;
u are right .

Now the expression after ##1 " (@(posedge clk2) (b |=> c) ) " is a
property and not a sequence.
This property is called in the above property. ' |=> ' is allowed in
the property.
look LRM pg:no: 259 and write to me to discuss if needed, bye

regards,
vidya.



Rob Dekker wrote:

Got an interesting case for SystemVerilog Assertion experts.
I am confused on this.

Consider the following assertion statement :

assert property (@(posedge clk1) a ##1 @(posedge clk2) b |=> c ) ;

The LRM precedence rules seem to indicate that this should be interpreted as this :

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b |=> c) ) ;


where |=> c is thus clocked by 'clk2'....
but then the RHS of ##1 is a sequence, and |=> is only allowed in a property,
so this implementation should cause an error.

Or should it be implemented like this :

assert property (@(posedge clk1) (a ##1 @(posedge clk2) b) |=> c ) ;

where |=> c is thus clocked by 'clk1'...
But is that right ?

Or should it be interpreted differently again ?

Any insights would be greatly appreciated.

 

[Rob Dekker]

Thank you for your response Vidya !

However, how can the right hand side of ##1 (a cycle delay range) be a property ?
The LRM quite clearly states that it can only be a sequence :

sequence_expression ::=
....
sequence_expression cycle_delay_range sequence_expression
....

Thanks

Rob




"Vidyasagar .H Vaddadi" <sagar.vidya.v@gmail.com> wrote in message news:1163764080.426497.12730@j44g2000cwa.googlegroups.com...

hello Rob its a good twister i must say.

The property ::
assert property (@(posedge clk1) a ##1 @(posedge clk2)
b |=> c ) ;

shoould be interpreted according to LRM as

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b
|=> c) ) ;
u are right .

Now the expression after ##1 " (@(posedge clk2) (b |=> c) ) " is a
property and not a sequence.
This property is called in the above property. ' |=> ' is allowed in
the property.
look LRM pg:no: 259 and write to me to discuss if needed, bye

regards,
vidya.



Rob Dekker wrote:
Got an interesting case for SystemVerilog Assertion experts.
I am confused on this.

Consider the following assertion statement :

assert property (@(posedge clk1) a ##1 @(posedge clk2) b |=> c ) ;

The LRM precedence rules seem to indicate that this should be interpreted as this :

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b |=> c) ) ;


where |=> c is thus clocked by 'clk2'....
but then the RHS of ##1 is a sequence, and |=> is only allowed in a property,
so this implementation should cause an error.

Or should it be implemented like this :

assert property (@(posedge clk1) (a ##1 @(posedge clk2) b) |=> c ) ;

where |=> c is thus clocked by 'clk1'...
But is that right ?

Or should it be interpreted differently again ?

Any insights would be greatly appreciated.

 

[Vidyasagar .H Vaddadi]

Hi Rob the LRM also says on page 257

17.12.2 Multiply-clocked properties
" As in the case of singly-clocked properties, the result of
evaluating a multiply-clocked property is either true or
false. Multiply-clocked properties can be formed in a number of ways.
Multiply-clocked sequences are themselves multiply-clocked properties.

For example,
@(posedge clk0) sig0 ##1 @(posedge clk1) sig1 is a multiply-clocked
property. "

Atleast i dont find any reason why it shud be only sequence after ##1 .
As far as Properties Vs Sequences both are extensively used and
instantiated in another properites similarly. Refer to the
"Multiply-clocked properties" sub section in the LRM and giv ur
comments!!

thanks,
Vidya.

Rob Dekker wrote:

Thank you for your response Vidya !

However, how can the right hand side of ##1 (a cycle delay range) be a property ?
The LRM quite clearly states that it can only be a sequence :

sequence_expression ::=
....
sequence_expression cycle_delay_range sequence_expression
....

Thanks

Rob




"Vidyasagar .H Vaddadi" <sagar.vidya.v@gmail.com> wrote in message news:1163764080.426497.12730@j44g2000cwa.googlegroups.com...

hello Rob its a good twister i must say.

The property ::
assert property (@(posedge clk1) a ##1 @(posedge clk2)
b |=> c ) ;

shoould be interpreted according to LRM as

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b
|=> c) ) ;
u are right .

Now the expression after ##1 " (@(posedge clk2) (b |=> c) ) " is a
property and not a sequence.
This property is called in the above property. ' |=> ' is allowed in
the property.
look LRM pg:no: 259 and write to me to discuss if needed, bye

regards,
vidya.



Rob Dekker wrote:
Got an interesting case for SystemVerilog Assertion experts.
I am confused on this.

Consider the following assertion statement :

assert property (@(posedge clk1) a ##1 @(posedge clk2) b |=> c ) ;

The LRM precedence rules seem to indicate that this should be interpreted as this :

assert property (@(posedge clk1) a ##1 (@(posedge clk2) (b |=> c) ) ;


where |=> c is thus clocked by 'clk2'....
but then the RHS of ##1 is a sequence, and |=> is only allowed in a property,
so this implementation should cause an error.

Or should it be implemented like this :

assert property (@(posedge clk1) (a ##1 @(posedge clk2) b) |=> c ) ;

where |=> c is thus clocked by 'clk1'...
But is that right ?

Or should it be interpreted differently again ?

Any insights would be greatly appreciated.