[sv-ac] SVA: Emulating sequence "a before b"

I am having difficulty emulating the PSL "a before b". In PSL "The left
operand of the before family of operators is an FL Property that holds before
the FL Property that is
the right operand holds."
The following does not work:
property Test;
int a_v;
($rose(a), a_v=a) ##[0:$] b && ! $rose(a==a_v);
endproperty : Test
That does not work because the sequence passed the property Test:
$rose(a) ##2 $rose(a) ##4 b
even if each $rose(a) is at the same value of a.
This is because ##[0:$] keeps on waiting until the condition "b && !
$rose(a==a_v)" is satisfied.
Any suggestion on how this "before" function can be emulated in SVA?
Thanks,
Ben
-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
_http://www.vhdlcohen.com/_ (http://www.vhdlcohen.com/) vhdlcohen@aol.com
Author of following textbooks:
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004 isbn
 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
------------------------------------------------------------------------------
Received on Mon May 3 14:34:28 2004