Method for piecewise hierarchical sequential verification

Abstract

This disclosure describes a method for accomplishing sequential logical equivalence verification using a hierarchical piecewise approach. Initially, the method provides a reference semiconductor design and a second semiconductor design with logic edits relative to it. The method submits both to formal verification to check the reference design against the second semiconductor design with all edits disabled. The semiconductor design is partitionedand associated input constraints. The edits are further groupedand ordered. The invention also discovers a set of dependencies of the logic editsand checks that the ordering of groups obeys the dependencies. Each group of edits is further submitted to formal verificationand any input constraints assumed for any partitions are verified in their enclosing partition. Finally, the method reports success if formal verification succeeds on each group of logic edits and on each set of input constraints