Subject: Re: [sv-ac] SVA/PSL equivalences
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Oct 30 2003 - 07:42:18 PST
Hi Roy:
I agree with you on this pair. Of course, my proposed change
to the SVA semantics will fix this problem and make these two
equivalent.
Best regards,
John H.
>
> Hi John,
>
> You are right. The ones that are not equivalent are:
> initial assert @(c) not (x || y)
> and
> (!(x! | y!)) @c
>
> The SVA version is a liveness property while the PSL is a safety.
>
> Regards,
> Roy
>
>
This archive was generated by hypermail 2b28 : Thu Oct 30 2003 - 07:43:15 PST