Functional Dependency for Verification Reduction

11 years 3 months ago
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...
Jie-Hong Roland Jiang, Robert K. Brayton
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CAV
Authors Jie-Hong Roland Jiang, Robert K. Brayton
Comments (0)