This paper presents a methodology for 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. The results win by several order of magnitude in area consumption were the used area is almost 50% less than other compared approaches with a slight increase in CPU run time.
Track
Electronics: Electronic Engineering and Applications
Conference
1st Mosharaka International Conference on Emerging Applications of Electrical Engineering (MIC-ElectricApps 2020)
Congress
2020 Global Congress on Electrical Engineering (GC-ElecEng 2020), 4-6 September 2020, Valencia, Spain
Pages
--1
Topics
Integrated Circuit Verification and Testing Formal Verification of Integrated Circuits
ISSN
2227-331X
DOI
BibTeX
@inproceedings{1166ElecEng2020,
title={Verification of non-linear arithmetic circuits using functionally reduced and-inverter-graph (FRAIG)},
author={Sa'ed Abed, and Manayer Almehteb, and Wathiq Masnsoor, and Amjad Gawanmeh},
booktitle={2020 Global Congress on Electrical Engineering (GC-ElecEng 2020)},
year={2020},
pages={--1},
doi={}},
organization={Mosharaka for Research and Studies}
}