Subject: Re: [sv-ac] revised SVA semantics
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Apr 23 2003 - 14:39:44 PDT
Hi Adam:
Here are the changes:
1. Subsection 3.4, add definition of "sample".
2. Subsection 3.4, change definition of "block((R_1 intersect R_2))" from
block((R_1 intersect R_2))
= block(R_1) \cup block(R_2) \cup (flow({},R_1) \cap flow({},R_2))
to
block((R_1 intersect R_2))
= block(R_1) \cup block(R_2) \cup (sample(R_1) \cap sample(R_2))
3. Subsection 3.5, change definition of tight satisfaction for intersect from
w,L_0,L_1 |== (R_1 intersect R_2) iff there exist L',L'' such that
w,L_0,L' |== R_1 and w,L_0,L'' |== R_2 and L_1 = L'|_D \cup L''|_D,
where D = flow(dom(L_0), (R_1 intersect R_2))
to
w,L_0,L_1 |== (R_1 intersect R_2) iff there exist L_{(1)}, L_{(2)}
such that w,L_0,L_{(1)} |== R_1 and w,L_0,L_{(2)} |== R_2 and
L_1 = L_{(1)}|_{D_1} \cup L_{(2)}|_{D_2}, where
D_1 = flow(dom(L_0), R_1) - (block((R_1 intersect R_2)) \cup sample(R_2))
D_2 = flow(dom(L_0), R_2) - (block((R_1 intersect R_2)) \cup sample(R_1))
Best regards,
John Havlicek
> Date: Wed, 23 Apr 2003 15:49:46 -0500
> From: Adam Krolnik<krolnik@lsil.com>
> X-Accept-Language: en-us, en
> CC: <sv-ac@eda.org>, <vfv@eda.org>
>
>
>
>
> Hi John;
>
>
> What has changed? Do you have a summary?
>
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
This archive was generated by hypermail 2b28 : Wed Apr 23 2003 - 14:41:38 PDT