Subject: Re: [sv-ac] boolean implication
From: John Havlicek (john.havlicek@motorola.com)
Date: Fri Mar 07 2003 - 15:56:50 PST
Hi Adam:
Someone sent me the following CBV
if +(1) : (a)
begin
+(1) : a1;
if +(1) : (b)
begin
+(1) : b1;
if +(1) : (c)
+(1) : d;
end
end
and asked me how to write it in SVA. My first answer was that it has
to be broken up and written as something like
assert (([1]a) => ([1]a1));
assert (([1]a;b) => ([1]b1));
assert (([1]a;b;c) => ([1]d));
That raised concern about redundant expression evaluation and how
good the tools will be about eliminating it. I guess that good
simulators will be able to get rid of the redundancy.
Now I see that my first answer neglected the possibility of writing
a single sequence.
assert (1; !a || (1; a1 && (!b || (1; b1 && (!c || 1;d)))));
Other comments below.
Best regards,
John H.
> Date: Fri, 07 Mar 2003 17:18:01 -0600
> From: Adam Krolnik<krolnik@lsil.com>
> X-Accept-Language: en-us, en
> CC: <sv-ac@eda.org>
>
>
>
> Hi John;
>
>
> Hmmm, you are saying that this form:
>
> > (1; a => (1; a1 && (b => (1; b1 && (c => 1;d)))))
>
> is more readable than this equivalent form:
>
> > (1; !a || (1; a1 && (!b || (1; b1 && (!c || 1;d)))))
>
Yes, although they both look pretty bad compared to the CBV. :)
I would probably type the SVA in as something like
(
1;
a =>
(
1;
a1
&&
(
b =>
(
1;
b1
&&
(
c =>
1;
d
)
)
)
)
)
> BTW, why do you call this boolean implication when one of the terms is a sequence?
Just following the LRM. See subsection 11.6.7.
>
>
> Wow!
>
> I think I like having boolean implication where it is to prevent a
> sequence like this... Maybe it looks better with comments and an explanation.
>
> Is this the correct expansion of possible sequences matching the above?
>
> 1; !a
> 1; a ; a1 && !b
> 1; a ; a1 && b; b1 && !c
> 1; a ; a1 && b; b1 && c ; d
>
> I would appreciate the expanded form better as I would be more convinced of its
> correctness.
>
>
> >So, at the 11th hour, I propose that we consider returning
> >boolean implication to the sequence layer, with a different
> >syntax from sequence implication.
>
> What benefit does the user receive from different syntax? I.e. Is there
> ambiguity that different syntax separates? It seems that context already
> separates boolean from sequence.
The operators produce different things--one produces a sequence from a
boolean and a sequence, while the other produces a property from a
sequence and a sequence.
>
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
>
This archive was generated by hypermail 2b28 : Fri Mar 07 2003 - 15:58:15 PST