Vanessa,
I suggest you write a small blif-mv model (or even a Verilog one ! ) which
simply says :
...
output enable_out;
assign enable_out = 1;
...
and compose it with the arbiter.
Emil
>
>
> 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 - 05:23:50 MST