Formal Verification of Integrated Circuits Integrated Circuit Verification and Testing
Biography
This paper presents a methodology of verifying non-linear arithmetic circuits by applying diffident concepts. In our proposed methodology, combination of gate -level netlist, Functionally Reduced And-inverter Graph (FRAIG) and Taylor Expansion Diagram (TED) will be used to verify that the implementation satisfies the specification. Backward algebraic rewriting technique is used for function extraction of the word-level abstraction. Gate level-netlist is used to form FRAIG graph which will be verified via TED representation. Our work will focus on the complex verification process of multiplier and alternatives of the traditional AIG for Arithmetic circuits. Experiments were conducted on both post and pre synthesized non-linear arithmetic circuit of various multipliers such as Booth and CSA. Experimental results win by several order of magnitude in area consumption were the used area is almost 50% less than other compared approaches. However, our methodology fails to prove its efficiency in terms of CPU run time.
