Paper Info
Title
Equivalence Checking and Simulation By Computing Range Reduction
Abstract
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.
Year
Venue
Field
2015
CoRR
Formal equivalence checking,Discrete mathematics,Functional verification,Algorithm,Combinational logic,Equivalence (measure theory),Mathematical proof,Mathematics,Computation
DocType
Volume
Citations 
Journal
abs/1507.02297
3
PageRank 
References 
Authors
0.52
5
1
Name
Order
Citations
PageRank
Eugene Goldberg1258.01