Verification of arithmetic datapath designs using word-level approach — A case study

The paper describes an efficient method to prove equivalence between two integer arithmetic datapath designs specified at the register transfer level. The method is illustrated with an industrial ALU design. As reported in literature, solving it using a commercial equivalence checking tool required case-splitting, which limits its applicability to larger designs. We show how such a task can be solved as a simpler verification problem without case-splitting. We demonstrate both the word-level and bit-level approach to this problem and show that the method is scalable to large combinational datapath circuits. Experimental results demonstrate the application of the method to large combinational arithmetic circuits.