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

John,
Thanks.
That was very useful!
I wonder why SVA did not use a "before" a la PSL, thus making it an integral
part of the language. Now a user has to add this property somewhere in a
file or in the code to use the "before".
Ben
<Hi Ben:

By definition

f before g

is equivalent in PSL to

[!g W (f && !g)]

Therefore, if you can emulate f,g themselves in SVA 3.1a
and if you do not need to use a recursive property to
emulate g, then you can emulate "f before g" in SVA 3.1a
by defining

property sva_before(F,G);
(not G) and (F or (1'b1 |=> sva_before(F,G)));
endproperty

and using the following recursive property instance:

sva_before(f,g)

If a,b are boolean expressions, then you can emulate

a before b

by the SVA 3.1a property

(not (##[0:$] b)) or (!b[*0:$] ##1 (a && !b))

Best regards,

John H.
>
-----------------------------------------------------------------------------
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 19:18:59 2004