Fairness Constraints Fairness constraints are used to restrict the behavior of the design. Each fairness condition specifies a set of states in the machine, and requires that in any acceptable behavior these states must be traversed infinitely often (i.e., these states must be on a cycle). Such constraints are called ``Büchi fairness'' constraints. Fairness constraints are stored in fairness files (with extension .fair by convention). A fairness file is read in by the read_fairness command. Active fairness conditions can be displayed by means of print_fairness. The reset_fairness command is used to reset the fairness constraint to ``true''; by default, there is one fairness condition that contains all states. Fairness constraints remove unwanted behavior from a system. They are a powerful tool, but should be used with care, because it is easy to make a faulty system pass wanted properties by a careless use of fairness constraints. Also, it has been observed that verification is slowed down considerably when there are many fairness constraints.

Contact 

©2002-2018 U.C. Regents