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

Ben:

> I wonder why SVA did not use a "before" a la PSL, thus making it an
> integral part of the language.

I think there are a number of derived operators in PSL that
are not in SVA. One reason these do not appear in SVA is that
they only became representable with the extensions of 3.1a
(as in the case of "before"). This meant that it was late
in the 3.1a effort (arguably too late) before we could begin
to look at adding new derived operators.

A technical complication with adding an operator like "before"
to SVA is that in the SVA 3.1a framework you cannot negate an
instance of a recursive property, and this adds a restriction
on the arguments of the derived operator.

Best regards,

John H.

P.S. I think that because my e-mail has changed to "@freescale.com"
my mail will bounce from the reflector. :(

>
> 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
>
Received on Mon May 3 20:30:16 2004