Structure-driven algorithms for equivalence verification and infeasibility checking.
Karem A. Sakallah, Maher N. Mneimneh · Deep Blue (University of Michigan) · 2006
Today's digital systems are at the forefront of modern technology. Electronic chips with a billion transistors are not a farfetched goal. For digital systems to continue pervading our lives, we must strive to build rigorous technologies for designing them and ensuring their functional correctness. The difficulty of this problem is a direct consequence of its inherent computational intractability; the design and verification tasks requires extensive computational resources. In this thesis, we tackle this problem by constructing scalable algorithms for verifying the correctness of these systems as well as identifying infeasiblities during their design. Our work addresses one problem of formal verification known as sequential equivalence verification. Despite considerable research, sequential verification algorithms are hindered by the inherent state explosion problem. Our premise is that verifying the sequential equivalence of actual circuits should be tractable. The simple intuition behind this assertion is that human designers routinely create complex designs and are able to cope with them. The inability of automatic verification tools to analyze these designs is due to their failure to recognize, and judiciously account for, the structure present in these systems. Thus, we explore and develop a battery of techniques whose aim is to identify and effectively utilize knowledge derived from the structure of real-life verification tasks. Identifying the causes of infeasibility of a set of contraints frequently arises during the design and verification of digital systems. These systems are modeled using Boolean formulas whose unsatisfiability usually identifies a problem that needs to be diagnosed and fixed. In design applications, for example, a large Boolean function is formed such that a feasible design is obtained when the function is satisfiable, and design infeasibility is indicated when the function is unsatisfiable. Without further analysis of the causes of unsatisliability, we have no clue as to what design constraints must be modified to make the design feasible. We develop algorithms for identifying the causes of infeasibility by extracting minimal unsatisfiable subformulas. We present algorithms for extracting single and multiple such subformulas as well as algorithms for extracting the smallest of such formulas in terms of its number of constraints.