>>>>> "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.
-- Fabio Somenzi | Phone: 303-492-3466 University of Colorado | Fax: 303-492-2758 ECE Dept. | Email: Fabio@Colorado.EDU Boulder CO 80309-0425 | WWW: http://vlsi.colorado.edu/~fabio
This archive was generated by hypermail 2b30 : Fri Apr 05 2002 - 00:49:06 MST