US 2011/0214096 A1 · 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 200. The semiconductor design is partitioned 202 and associated input constraints 204. The edits are further grouped 206 and ordered 208. The invention also discovers a set of dependencies of the logic edits 210 and checks that the ordering of groups obeys the dependencies 212. Each group of edits is further submitted to formal verification 214 and any input constraints assumed for any partitions are verified in their enclosing partition 216. Finally, the method reports success if formal verification succeeds on each group of logic edits and on each set of input constraints 218.

Claims21

Dependent claims

A method for performing sequential logical formal verification of integrated circuit IC designs using a piecewise hierarchical approach, the method comprising:

providing a reference IC design;
providing a modified IC design that includes one or more logic edits relative to said reference IC design;
performing sequential logical formal verification of logic between said reference IC design and said modified IC design with all of said one or more logic edits disabled;
creating groups of logic edits from said one or more logic edits in said modified IC design;
discovering dependencies between said one or more logic edits in said modified IC design;
ordering said groups of logic edits based upon said dependencies;
checking that said ordering of said groups of logic edits obeys said dependencies between said one or more logic edits in said modified IC design;
performing sequential logical formal verification of logic independently on each of said groups of logic edits in accordance with said ordering;
and
tracking a validation status of said sequential logical formal verification of said logic edits.

7 more elements

A non-transitory computer readable storage device including program instructions executable by a computing device to perform a method for sequential logical formal verification between a reference integrated circuit (IC) design and a modified IC design that includes one or more logic edits relative to the reference IC design using a piecewise hierarchical approach, the method comprising:

providing a second semiconductor design that comprises one or more logic edits relative to said reference semiconductor design;
performing sequential logical formal verification of logic between said reference IC design and said modified IC design with all of said one or more logic edits disabled;
creating groups of logic edits from said one or more logic edits in said modified IC design;
discovering dependencies between said one or more logic edits in said modified IC design;
ordering said groups of logic edits based upon said dependencies;
list of second semiconductor
performing sequential logical formal verification of logic independently on each of said groups of logic edits in accordance with said ordering;
and
tracking a validation status of said sequential logical formal verification of said logic edits.

6 more elements

A method for performing a piecewise hierarchical sequential logical formal verification of integrated circuit (IC) designs, the method comprising:

providing a reference IC design;
creating a modified IC design including logic edits relative to said reference IC design;
performing sequential logical formal verification of logic between said reference IC design to be checked against and said modified IC design with all of said logic edits disabled;
creating groups of logic edits from said logic edits in said modified IC design;
creating a verification ordering of said groups of logic edits in said modified IC design based upon dependencies between said groups of logic edits;
creating instances of said modified IC design, wherein each instance includes one or more enabled groups of logic edits;
performing according to said verification ordering, sequential logical formal verification of logic between successive instances of said modified IC;
and
tracking a validation status of each of said logic edits.

6 more elements

providing a reference IC design;
creating a modified IC design including logic edits relative to said reference IC design;
performing sequential logical formal verification of logic between said reference IC design and said modified IC design with all of said logic edits disabled;
creating groups of logic edits from said logic edits in said modified IC design;
creating a verification ordering of said groups of logic edits in said modified IC design based upon dependencies between said groups of logic edits;
creating instances of said modified IC design, wherein each instance includes one or more enabled groups of logic edits;
performing according to said verification ordering, sequential logical formal verification of logic between successive instances of said modified IC;
and
tracking a validation status of each of said logic edits.

6 more elements

Dependencies are inferred from the claim text.

Method For Piecewise Hierarchical Sequential Verification

Life of this patent

Method For Piecewise Hierarchical Sequential Verification

Life of this patent

Abstract

Claims21