  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.
