Abstract
This thesis presents probability based approaches to combinational equivalence checking. First, an exact approach using aliasing-free assignments is introduced. To improve the efficiency of probability calculation, a new encoding scheme and operations are proposed. The encoding scheme and operations also solve the signal correlation issue during the output probability calculation. However, the aliasing-free assignments exponentially grow. This inherent disadvantage limits the exact approach to solve large circuits. Thus, an approximate approach is proposed. We propose a verification architecture, PEACH, such that a virtually-zero aliasing rate is obtained in a single-pass probability calculation. Furthermore, the aliasing rate can be easily configured in various precision by designers.