Information theoretic subgraph caching

Abstract

Computer-implemented techniques are disclosed for verifying circuit designs using subgraph caching. A device under test (DUT) is modeled as a graph. The graph is partitioned into one or more subgraphs and problems are generated for each subgraph. Graph and subgraph problem generation is repeated numerous times throughout the verification process. Problems and sub-problems are generated and solved. When a subgraph problem is solved, the problem's variables, values, and information can be stored in a cache. The storage can be based on entropy of variables used in the graph and subgraph problems. The subgraph problem storage cache can be searched for previously stored problems which match another problem in need of a solution. By retrieving subproblem variables, values, and information from the cache, the computational overhead of circuit design verification is reduced as problems are reused. Caching can be accomplished using an information theoretic approach.