Static analysis of deadends in SVA constraints

When sequential constraints are used in constrained random simulation, it is possible for the choice of solution for the constraints at any cycle to lead to a deadend at a later cycle. A deadend occurs when the constraints have no solution, which indicates a problem with the constraints. We describe a method to identify deadends for a set of SVA constraints and to generate additional SVA constraints that will prevent these deadends. The generated constraints provide insight into the nature of the deadends and help to resolve them. Our method for identifying deadends also makes use of an efficient technique for finding minimal unsatisfiable subsets of an unsatisfiable set of Boolean expressions.