Improving language containment using fairness graphs

Abstract

Language containment is one important approach to formal design verification. When working at a higher, more abstract level, additional unwanted behavior may be introduced in the model that can be excluded for the verification step using so-called fairness constraints. The language containment computation using Binary Decision Diagrams (BDD’s) typically involves performing reachability analysis, early failure detection, and then applying a set of operators until convergence is achieved ([HTKB92]). The running time of the latter part (called the main computation) is correlated with the number of fairness constraints. In this paper, we introduce techniques which improve the efticieney of the main computation by analyzing a graph induced by the fairness constraints. This graph can be built efficiently using BDD’s. We have implemented our algorithms in the verification system HSIS, and experimental results demonstrate the effectiveness of these ideas.