Most of the verification tools in industry today are hard to fit for the rapid increase of the sizes of integrated circuits. In this paper, a layered verification using SMT solvers through hypergraph partitioning based constraint decomposition is proposed, which is provided for formal verification of the satisfiability of RTL circuit. In this method, after modeling structural constraints of the RTL circuit and its correlative variables as a hypergraph model with appropriate weights, a hypergraph partitioning based constraints decomposition procedure is used to find a proper balanced bi-partiti...
