Equivalence Checking of Bounded Sequential Circuits Based on Gröbner Basis

The sequential circuit equivalence verification problem is researched in this paper, bounding equivalence verification method based on Grobner basis is put forwarded. First, to be verified sequential circuit expansion to a set of Polynomial Symbolic Algebra Representation in accordance with time frame, so the sequential equivalence checking problem translate into combinational equivalence checking problem, The global constraints are mined over the expression database according to time series. Moreover, the approach can also mine the illegal constraints and complex polynomial relationship, with this the solving space is pruned dramatically. Then calculate the Grobner basis of the two sets, testing equivalence with equivalence checking algorithm. The experiment results show that this approach can realize rapid convergence, eliminate false verification effectively.