2015/07/08 by Goldberg, Eugene
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1507.02297
We introduce new methods of equivalence checking and simulation based on Computing Range Reduction (CRR). Given a combinational circuit N, the CRR problem is to compute the set of outputs that disappear from the range of N if a set of inputs of N is excluded from consideration. Importantly, in many cases, range reduction can be efficiently found even if computing the entire range of N is infeasible. Solving equivalence checking by CRR facilitates generation of proofs of equivalence that mimic a "cut propagation" approach. A limited version of such an approach has been successfully used by commercial tools. Functional verification of a circuit N by simulation can be viewed as a way to reduce the complexity of computing the range of N. Instead of finding the entire range of N and checking if it contains a bad output, such a range is computed only for one input. Simulation by CRR offers an alternative way of coping with the complexity of range computation. The idea is to exclude a subset of inputs of N and compute the range reduction caused by such an exclusion. If the set of disappeared outputs contains a bad one, then N is buggy.