We consider the problem of equivalence checking of circuits N_1,N_2 with a common specification (CS). We show that circuits N_1 and N_2 have a CS iff they can be partitioned into toggle equivalent subcircuits that are connected "in the same way". Based on this result, we formulate a procedure for checking equivalence of circuits N_1 and N_2 with specifications S_1 and S_2. This procedure not only checks equivalence of N_1 and N_2 but also verifies that S_1 and S_2 are identical. The complexity of this procedure is linear in specification size and exponential in the value of a specification parameter. Previously we considered specifications parameterized by the size of the largest subcircuit (specification granularity). In this paper we give a more general parameterization based on specification "width".
展开▼
