Constraints decomposition for RTL verification by SMT

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-partitioning with min-cut, in order to accomplish bounded model checking more efficiently for the RTL circuit. The experimental results show the efficiency for pruning of the search space and in solving the satisfiability problem.