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.
> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> From: <VhdlCohen@aol.com>
> Date: Mon, 3 May 2004 17:34:18 EDT
> Sender: owner-sv-ac@eda.org
> Precedence: bulk
>
> -------------------------------1083620058
> Content-Type: text/plain; charset="US-ASCII"
> Content-Transfer-Encoding: 7bit
>
> 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. <http://www.vhdlcohen.com/> 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
> ------------------------------------------------------------------------
> ------
>
> -------------------------------1083620058
> Content-Type: text/html; charset="US-ASCII"
> Content-Transfer-Encoding: quoted-printable
>
> <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
> <HTML><HEAD>
>
> <META content=3D"MSHTML 6.00.2800.1400" name=3DGENERATOR></HEAD>
> <BODY id=3Drole_body style=3D"FONT-SIZE: 10pt; COLOR: #000000; =
> FONT-FAMILY: Arial"=20
> bottomMargin=3D7 leftMargin=3D7 topMargin=3D7 rightMargin=3D7><FONT =
> id=3Drole_document=20
> face=3DArial color=3D#000000 size=3D2>
> <DIV> I am having difficulty emulating the PSL "a before b". =
> In PSL=20
> "The left operand of the before family of operators is an FL Property =
> that holds=20
> before the FL Property that is<BR>the right operand holds."</DIV>
> <DIV> </DIV>
> <DIV>The following does not work: </DIV>
> <DIV> <STRONG>property</STRONG> Test;</DIV>
> <DIV> int a_v; </DIV>
> <DIV> (<STRONG>$rose</STRONG>(a), a_v=3Da) ##[0:$] b && ! =
>
> $<STRONG>rose</STRONG>(a=3D=3Da_v);</DIV>
> <DIV> <STRONG>endproperty</STRONG> : Test</DIV>
> <DIV> </DIV>
> <DIV>That does not work because the sequence passed the property Test: =
> </DIV>
> <DIV> <STRONG>$rose</STRONG>(a) =
> ##2 <STRONG>$rose</STRONG>(a) ##4=20
> b</DIV>
> <DIV>even if each <STRONG>$rose</STRONG>(a) is at the same value of a. =
> </DIV>
> <DIV>This is because ##[0:$] keeps on waiting until the condition "b =
> &&=20
> ! $<STRONG>rose</STRONG>(a=3D=3Da_v)" is satisfied. </DIV>
> <DIV> </DIV>
> <DIV>Any suggestion on how this "before" function can be emulated in =
> SVA? </DIV>
> <DIV>Thanks,</DIV>
> <DIV>Ben </DIV>
> <DIV><B> </B><FONT lang=3D0 face=3DArial size=3D1 =
> FAMILY=3D"SANSSERIF"=20
> PTSIZE=3D"8">-----------------------------------------------------------=
> ------------------<BR>Ben=20
> Cohen Trainer, Consultant, Publisher (310) 721-4830 <BR><A=20
> href=3D"http://www.vhdlcohen.com/">http://www.<B>vhdlcohen</B>.com/</A> =
>
> vhdlcohen@aol.com <BR>Author of following textbooks: <BR>* <B>Using =
> PSL/SUGAR=20
> for Formal and Dynamic Verification 2nd Edition, </B>2004 isbn=20
> 0-9705394-6-0<BR>* <B>Real Chip Design and Verification Using Verilog =
> and=20
> VHDL</B>, 2002 isbn 0-9705394-2-8 <BR>* <B>Component Design by =
> Example</B> ",=20
> 2001 isbn 0-9705394-0-1<BR>* <B>VHDL Coding Styles and Methodologies, =
> 2nd=20
> Edition</B>, 1999 isbn 0-7923-8474-1<BR>* <B>VHDL Answers to Frequently =
> Asked=20
> Questions, 2nd Edition</B>, isbn=20
> 0-7923-8115<BR>---------------------------------------------------------=
> ---------------------</FONT></DIV></FONT></BODY></HTML>
> -------------------------------1083620058--
Received on Mon May 3 19:06:09 2004
This archive was generated by hypermail 2.1.8 : Mon May 03 2004 - 19:06:29 PDT