>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> Sir,
vg> But I want to put constraint [ always "en_1=1" ] .
vg> To put "en_1=1" in fairness-constraint-file is not sufficient
vg> becoz meaning of "infinitely-often" is not ALWAYS.
vg> Please tell me I am right or wrong ?
You are obviously right. If you indeed need to constrain en_1 to be
always 1, then it is not a fairness constraint; you can do as
suggested by Emil Dumitrescu in a previous posting, and modify your
model. That is probably the most efficient way from the CPU time
point of view.
If, on the other hand, you do not want to change the model, so that
perhaps you can use the same model for all properties, here is
another possibility.
Suppose that you want to prove that p is inevitably followed by q as
long as r is always 1. Then, you can write
AG(p -> AF(r -> q))
-- 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 - 11:28:59 MST