# US 2014/0157216 A1 · Managing model checks of sequential designs > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 2014/0157216 A1 - Document ID: US20140157216A1 - Status: Published application - Kind: A1 - Application number: 13/691,789 - Filed: 2012-12-01 - Published: 2014-06-05 - Earliest claimed: 2012-12-01 - Assignees: Synopsys, Inc. - Applicants: Synopsys Inc. - Inventors: Manish Pandey; Jinqing Yu - Web page: https://patentgrep.com/patent/US20140157216A1 ## CPC - G06F 30/3323: using formal methods, e.g. equivalence checking or property checking - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract A method, system or computer usable program product for model checking a first circuit model including determining whether the first circuit model is functionally equivalent to one of a set of prior circuit models stored in persistent memory, and in response to determining functional equivalence, utilizing a processor to provide test results for the functionally equivalent prior circuit model. ## Claims ### Claim 1 A method of model checking a first circuit model comprising: utilizing a processor to determine whether the first circuit model is functionally equivalent to one of a set of prior circuit models previously stored in persistent memory with corresponding prior test results for each of the set of prior circuit models; and in response to determining functional equivalence, utilizing the processor to provide the corresponding prior test results for the functionally equivalent prior circuit model. ### Claim 2 (depends on 1) The method of claim 1 further comprising utilizing the processor to perform a model check of the first circuit model when a functional equivalent model is not found in the set of prior circuit models. ### Claim 3 (depends on 2) The method of claim 2 further comprising: utilizing the processor to determine whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models previously stored in persistent memory; and in response to determining isomorphic equivalence, utilizing the processor to provide the corresponding prior test results for the isomorphically equivalent prior circuit model; wherein the step of utilizing the processor to perform the model check of the first circuit model is performed in response to a negative determination of functional and isomorphic equivalence. ### Claim 4 (depends on 3) The method of claim 3 wherein the step of determining whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models is performed prior to the step of determining whether the first circuit model is functionally equivalent to one of the set of prior circuit models. ### Claim 5 (depends on 3) The method of claim 3 further comprising: generating a first signature of the first circuit model; and determining whether the first signature matches a prior signature of one of the set of prior circuit models; wherein each prior circuit model is stored with a corresponding prior signature in persistent memory. ### Claim 6 (depends on 5) The method of claim 5 wherein the step of signature matching is performed prior to the steps of determining isomorphic equivalence and functional equivalence, and wherein the step of utilizing the processor to perform a model check of the first circuit model is performed in response to a negative determination of signature matching. ### Claim 7 (depends on 3) The method of claim 3 wherein the circuit model is generated from a circuit design. ### Claim 8 (depends on 7) The method of claim 7 further comprising manufacturing a semiconductor device based on the circuit design. ### Claim 9 A computer usable program product comprising a computer usable persistent storage medium including computer usable code for use in model checking a first circuit model, the computer usable program product comprising code for performing the steps of: utilizing a processor to determine whether the first circuit model is functionally equivalent to one of a set of prior circuit models previously stored in persistent memory with corresponding prior test results for each of the set of prior circuit models; and in response to determining functional equivalence, utilizing the processor to provide the corresponding prior test results for the functionally equivalent prior circuit model. ### Claim 10 (depends on 9) The computer usable program product of claim 9 further comprising utilizing the processor to perform a model check of the first circuit model when a functional equivalent model is not found in the set of prior circuit models. ### Claim 11 (depends on 10) The computer usable program product of claim 10 further comprising: utilizing the processor to determine whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models previously stored in persistent memory; and in response to determining isomorphic equivalence, utilizing the processor to provide the corresponding prior test results for the isomorphically equivalent prior circuit model; wherein the step of utilizing the processor to perform the model check of the first circuit model is performed in response to a negative determination of functional and isomorphic equivalence. ### Claim 12 (depends on 11) The computer usable program product of claim 11 wherein the step of determining whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models is performed prior to the step of determining whether the first circuit model is functionally equivalent to one of the set of prior circuit models. ### Claim 13 (depends on 11) The computer usable program product of claim 11 further comprising: generating a first signature of the first circuit model; and determining whether the first signature matches a prior signature of one of the set of prior circuit models; wherein each prior circuit model is stored with a corresponding prior signature in persistent memory. ### Claim 14 (depends on 13) The computer usable program product of claim 13 wherein the step of signature matching is performed prior to the steps of determining isomorphic equivalence and functional equivalence, and wherein the step of utilizing the processor to perform a model check of the first circuit model is performed in response to a negative determination of signature matching. ### Claim 15 (depends on 11) The computer usable program product of claim 11 wherein the circuit model is generated from a circuit design. ### Claim 16 A data processing system for model checking a first circuit model, the data processing system comprising: a processor; and a persistent memory storing program instructions which when executed by the processor determine whether the first circuit model is functionally equivalent to one of a set of prior circuit models previously stored in persistent memory with corresponding prior test results for each of the set of prior circuit models, and if functional equivalence is shown, utilizing the processor to provide the corresponding prior test results for the functionally equivalent prior circuit model. ### Claim 17 (depends on 16) The data processing system of claim 16 further comprising program instructions stored in persistent memory which when executed by the processor perform a model check of the first circuit model when a functional equivalent model is not found in the set of prior circuit models. ### Claim 18 (depends on 17) The data processing system of claim 17 further comprising program instructions stored in memory which when executed by the processor: utilizing the processor to determine whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models previously stored in persistent memory, and if isomorphic equivalence is shown, utilizing the processor to provide the corresponding prior test results for the isomorphically equivalent prior circuit model; wherein the program instructions, which when executed by the processor perform a model check of the first circuit model when a functional equivalent model is not found in the set of prior circuit models, also perform a model check of the first circuit model when an isomorphic equivalent model is not found in the set of prior circuit models. ### Claim 19 (depends on 18) The data processing system of claim 18 further comprising program instructions stored in persistent memory which when executed by the processor: generate a first signature of the first circuit model; and determine whether the first signature matches a prior signature of one of the set of prior circuit models; wherein each prior circuit model is stored with a corresponding prior signature in persistent memory. ### Claim 20 A method of model checking a first circuit model comprising: utilizing a processor to determine whether the first circuit model is functionally equivalent to one of a set of prior circuit models stored in a database in persistent memory, each prior circuit model previously stored with a corresponding set of prior test results in the database; in response to a positive determination of functional equivalence, providing the corresponding set of prior test results stored with the functionally equivalent prior circuit model; and in response to a negative determination of functional equivalence, utilizing the processor to perform a model check of the first circuit model. ### Claim 21 (depends on 20) The method of claim 20 further comprising: determining whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models previously stored in the database; and in response to a positive determination of isomorphic equivalence, providing the corresponding set of prior test results stored with the isomorphically equivalent prior circuit model; wherein the step of utilizing a processor to perform a model check of the first circuit model is performed in response to a negative determination of functional and isomorphic equivalence. ### Claim 22 (depends on 21) The method of claim 21 wherein the step of determining whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models is performed prior to the step of determining whether the first circuit model is functionally equivalent to one of the set of prior circuit models. ### Claim 23 (depends on 21) The method of claim 21 wherein the circuit model is generated from a circuit design. ### Claim 24 (depends on 21) The method of claim 21 further comprising generating a first signature of the first circuit model; and determining whether the first signature matches a prior signature of one of the set of prior circuit models previously stored in the database; wherein each prior circuit model is stored with a corresponding prior signature in the database. ### Claim 25 (depends on 24) The method of claim 24 wherein the step of signature matching is performed prior to the steps of determining isomorphic equivalence and functional equivalence, and wherein in response to a negative determination of signature matching, performing the model check of the circuit model. ### Claim 26 (depends on 25) The method of claim 25 wherein each of the corresponding set of prior test results include a set of prior test parameters, wherein the prior signature includes prior test parameters, and wherein the first signature includes a set of first test parameters for the first circuit model. ### Claim 27 (depends on 21) The method of claim 21 further comprising generating a first signature of the first circuit model; and determining whether the first signature matches a prior signature of one of the set of prior circuit models stored in the database; wherein each prior circuit model is stored with a corresponding prior signature in the database; wherein the step of signature matching is performed prior to the steps of determining isomorphic equivalence and functional equivalence; wherein in response to a negative determination of signature matching, performing the model check of the circuit model; wherein each of the corresponding set of prior test results include a set of prior test parameters; wherein the prior signature includes prior test parameters; wherein the first signature includes a set of first test parameters for the first circuit model; wherein the step of determining whether the first circuit model is isomorphically equivalent to one of the set of prior circuit models is performed prior to the step of determining whether the first circuit model is functionally equivalent to one of a set of prior circuit models; and wherein the circuit model is generated from a circuit design.