Functional Dependency for Verification Reduction

Abstract. The existence of functional dependency among the state variables of a state transition system was identified as a common cause of inefficient BDD representation in formal verification. Eliminating such dependency from the system compacts the state space and may significantly reduce the verification cost. Despite the importance, how to detect functional dependency without or before knowing the reachable state set remains a challenge. This paper tackles this problem by unifying two closely related, but scattered, studies -- detecting signal correspondence and exploiting functional dependency. The prior work on either subject turns out to be a special case of our formulation. Unlike previous approaches, we detect dependency directly from transition functions rather than from reached state sets. Thus, reachability analysis is not a necessity for exploiting dependency. In addition, our procedure can be integrated into reachability analysis as an on-the-fly reduction. Preliminary e...

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Jie-Hong Roland Jiang, Robert K. Brayton
• Keywords: CAV 2004, Functional Dependency, Hardware, Reachability Analysis, State Sets