On Fri, 05 Apr 2002 Fabio Somenzi wrote :
> >>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com>
>writes:
>
> vg> Hello Sir,
> vg> In the arbiter example,suppose there is one more
> vg> primary input "enable".
>
> vg> Then there exists one more constraint(other than fairness
> vg> constraints) "enable should be high forever".
>
>It depends on how "enable" works, but normally one would want a
>constraint that says "enable should be high infinitely often."
>
> vg> Only under this constraint we can check any liveness
>property.
>
> vg> Can you please tell me the way I should apply this
>constraint in
> vg> CTL, along with fairness constraints.
>
>There should be a latched version of "enable," say "en_l." Then
>you
>just add the constraint
>
>en_l=1;
>
>to the other constraints.
>
++++++++++++++++++++++++++++++++++++++++++++++
Sir,
But I want to put constraint [ always "en_1=1" ] .
To put "en_1=1" in fairness-constraint-file is not sufficient
becoz meaning of "infinitely-often" is not ALWAYS.
Please tell me I am right or wrong ?
Thankyou
Vanessa
This archive was generated by hypermail 2b30 : Fri Apr 05 2002 - 04:03:10 MST