{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,7]],"date-time":"2025-03-07T05:18:41Z","timestamp":1741324721324,"version":"3.38.0"},"reference-count":35,"publisher":"Walter de Gruyter GmbH","issue":"4-5","funder":[{"name":"This work was supported in part by the German Research Foundation (DFG) within the project VerA","award":["DR 297\/37-1"],"award-info":[{"award-number":["DR 297\/37-1"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,8,26]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p xml:lang=\"en\">Truncated adders are widely used in applications where using lower bit-width is enough to generate the desired outputs. Truncated adders give benefits in area, power, and delay as compared to their non-truncated counterparts. While prior works deal with the formal verification of <jats:italic>n<\/jats:italic>-bit adders, there is no prior work dealing with the formal verification of unverified m-bit truncated adders using verified n-bit adder designs, where <jats:italic>m<\/jats:italic>\n                  <jats:inline-formula id=\"j_itit-2024-0068_ineq_001\">\n                     <jats:alternatives>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" overflow=\"scroll\">\n                           <m:mo>&lt;<\/m:mo>\n                        <\/m:math>\n                        <jats:tex-math>\n${&lt; } $\n<\/jats:tex-math>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_itit-2024-0068_ineq_001.png\"\/>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula>\n                  <jats:italic>n<\/jats:italic>. In this work, we propose a methodology that enables the verification for any truncated adder designs, irrespective of the architecture, called Extend and Reduce (EnR). EnR uses a three-step methodology to formally verify the truncated adders, which are considered as Design Under Verification (DUV). Firstly, it extends the bit-width of the DUV (truncated adder) to match with the nearest higher 2<jats:sup>\n                     <jats:italic>n<\/jats:italic>\n                  <\/jats:sup>-bit adder, called an Extended Truncated Adder (ETA). Secondly, it reduces off-the-shelf formally verified golden reference adder design by forcing 0\u2019s at the input bits to match it to the extended DUV design and re-synthesizing it to generate a Reduced Golden Adder (RGA). Lastly, a combinational equivalence check is then performed between the ETA and the RGA for formal verification. If the truncated adder is correct, the ETA and RGA are equivalent and vice versa. We evaluate a number and variety of adder designs to show the efficacy of the EnR methodology. We performed the formal verification using Binary Decision Diagrams (BDDs) and And-Inverter Graphs (AIGs). Lastly, we show the scalability of EnR methodology using adders up to a bit-width of 512 bits.<\/jats:p>\n               <jats:sec id=\"j_itit-2024-0068_abs_001\">\n                  <jats:title>ACM CCS<\/jats:title>\n                  <jats:p xml:lang=\"en\">Hardware \u2192 Arithmetic and datapath circuits; Combinational circuits; Equivalence checking; Functional verification; Electronic design automation.<\/jats:p>\n               <\/jats:sec>","DOI":"10.1515\/itit-2024-0068","type":"journal-article","created":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T10:21:51Z","timestamp":1730888511000},"page":"124-136","source":"Crossref","is-referenced-by-count":0,"title":["EnR: extend and reduce methodology to enable formal verification of truncated adders"],"prefix":"10.1515","volume":"66","author":[{"given":"Chandan Kumar","family":"Jha","sequence":"first","affiliation":[{"name":"University of Bremen , 28359 Bremen , Germany"}]},{"given":"Khushboo","family":"Qayyum","sequence":"additional","affiliation":[{"name":"German Research Center for Artificial Intelligence , DFKI GmbH , 28359 Bremen , Germany"}]},{"given":"Muhammad","family":"Hassan","sequence":"additional","affiliation":[{"name":"University of Bremen , 28359 Bremen , Germany"},{"name":"German Research Center for Artificial Intelligence , DFKI GmbH , 28359 Bremen , Germany"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"University of Bremen , 28359 Bremen , Germany"},{"name":"German Research Center for Artificial Intelligence , DFKI GmbH , 28359 Bremen , Germany"}]}],"member":"374","published-online":{"date-parts":[[2024,11,7]]},"reference":[{"key":"2025030616183075234_j_itit-2024-0068_ref_001","doi-asserted-by":"crossref","unstructured":"Z. Aizaz and K. Khare, \u201cArea and power efficient truncated booth multipliers using approximate carry-based error compensation,\u201d IEEE Trans. Circuits Syst. II Express Briefs, vol.\u00a069, no.\u00a02, pp.\u00a0579\u2013583, 2021. https:\/\/doi.org\/10.1109\/tcsii.2021.3094910.","DOI":"10.1109\/TCSII.2021.3094910"},{"key":"2025030616183075234_j_itit-2024-0068_ref_002","doi-asserted-by":"crossref","unstructured":"H.-J. Ko and S.-F. Hsiao, \u201cDesign and application of faithfully rounded and truncated multipliers with combined deletion, reduction, truncation, and rounding,\u201d IEEE Trans. Circuits Syst. II Express Briefs, vol.\u00a058, no.\u00a05, pp.\u00a0304\u2013308, 2011. https:\/\/doi.org\/10.1109\/tcsii.2011.2148970.","DOI":"10.1109\/TCSII.2011.2148970"},{"key":"2025030616183075234_j_itit-2024-0068_ref_003","doi-asserted-by":"crossref","unstructured":"Y. Pan and P. K. Meher, \u201cBit-level optimization of adder-trees for multiple constant multiplications for efficient fir filter implementation,\u201d IEEE Trans. Circuits Syst. I: Regul. Pap., vol.\u00a061, no.\u00a02, pp.\u00a0455\u2013462, 2013. https:\/\/doi.org\/10.1109\/tcsi.2013.2278331.","DOI":"10.1109\/TCSI.2013.2278331"},{"key":"2025030616183075234_j_itit-2024-0068_ref_004","doi-asserted-by":"crossref","unstructured":"J. Ding and S. Li, \u201cA modular multiplier implemented with truncated multiplication,\u201d IEEE Trans. Circuits Syst. II Express Briefs, vol.\u00a065, no.\u00a011, pp.\u00a01713\u20131717, 2017. https:\/\/doi.org\/10.1109\/tcsii.2017.2771239.","DOI":"10.1109\/TCSII.2017.2771239"},{"key":"2025030616183075234_j_itit-2024-0068_ref_005","doi-asserted-by":"crossref","unstructured":"S. Vahdat, M. Kamal, A. Afzali-Kusha, M. Pedram, and Z. Navabi, \u201cTruncApp: a truncation-based approximate divider for energy efficient dsp applications,\u201d in Design, Automation & Test in Europe Conference & Exhibition, IEEE, 2017, pp.\u00a01635\u20131638.","DOI":"10.23919\/DATE.2017.7927254"},{"key":"2025030616183075234_j_itit-2024-0068_ref_006","doi-asserted-by":"crossref","unstructured":"S. Amanollahi, M. Kamal, A. Afzali-Kusha, and M. Pedram, \u201cCircuit-level techniques for logic and memory blocks in approximate computing systems,\u201d Proc. IEEE, vol.\u00a0108, no.\u00a012, pp.\u00a02150\u20132177, 2020. https:\/\/doi.org\/10.1109\/jproc.2020.3020792.","DOI":"10.1109\/JPROC.2020.3020792"},{"key":"2025030616183075234_j_itit-2024-0068_ref_007","doi-asserted-by":"crossref","unstructured":"C. K. Jha, S. Singh, R. Thakker, M. Awasthi, and J. Mekie, \u201cZero aware configurable data encoding by skipping transfer for error resilient applications,\u201d IEEE Trans. Circuits Syst. I: Regul. Pap., vol.\u00a068, no.\u00a08, pp.\u00a03337\u20133350, 2021. https:\/\/doi.org\/10.1109\/tcsi.2021.3081623.","DOI":"10.1109\/TCSI.2021.3081623"},{"key":"2025030616183075234_j_itit-2024-0068_ref_008","doi-asserted-by":"crossref","unstructured":"C. K. Jha, A. Nandi, and J. Mekie, \u201cSingle exact single approximate adders and single exact dual approximate adders,\u201d IEEE Trans. Very Large Scale Integr. Syst., vol. 31, no. 7, pp. 907\u2013916, 2023. https:\/\/doi.org\/10.1109\/tvlsi.2023.3268275.","DOI":"10.1109\/TVLSI.2023.3268275"},{"key":"2025030616183075234_j_itit-2024-0068_ref_009","doi-asserted-by":"crossref","unstructured":"Y. S. Shao, et al.., \u201cSimba: scaling deep-learning inference with multi-chip-module-based architecture,\u201d in Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Microarchitecture, 2019, pp.\u00a014\u201327.","DOI":"10.1145\/3352460.3358302"},{"key":"2025030616183075234_j_itit-2024-0068_ref_010","doi-asserted-by":"crossref","unstructured":"J. Guo, et al.., \u201cBit-width adaptive accelerator design for convolution neural network,\u201d in 2018 IEEE International Symposium on Circuits and Systems, IEEE, 2018, pp.\u00a01\u20135.","DOI":"10.1109\/ISCAS.2018.8351666"},{"key":"2025030616183075234_j_itit-2024-0068_ref_011","doi-asserted-by":"crossref","unstructured":"Y. Zhu, et al.., \u201cLwrpro: an energy-efficient configurable crypto-processor for module-lwr,\u201d IEEE Trans. Circuits Syst. I: Regul. Pap., vol.\u00a068, no.\u00a03, pp.\u00a01146\u20131159, 2021. https:\/\/doi.org\/10.1109\/tcsi.2020.3048395.","DOI":"10.1109\/TCSI.2020.3048395"},{"key":"2025030616183075234_j_itit-2024-0068_ref_012","doi-asserted-by":"crossref","unstructured":"M. Imran, Z. U. Abideen, and S. Pagliarini, \u201cAn open-source library of large integer polynomial multipliers,\u201d in 2021 24th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS), IEEE, 2021, pp.\u00a0145\u2013150.","DOI":"10.1109\/DDECS52668.2021.9417065"},{"key":"2025030616183075234_j_itit-2024-0068_ref_013","doi-asserted-by":"crossref","unstructured":"T. Su, C. Yu, A. Yasin, and M. Ciesielski, \u201cFormal verification of truncated multipliers using algebraic approach and re-synthesis,\u201d in 2017 IEEE Computer Society Annual Symposium on VLSI, IEEE, 2017, pp.\u00a0415\u2013420.","DOI":"10.1109\/ISVLSI.2017.79"},{"key":"2025030616183075234_j_itit-2024-0068_ref_014","doi-asserted-by":"crossref","unstructured":"R. Drechsler, Advanced Formal Verification, vol. 122, New York, NY, Springer, 2004.","DOI":"10.1007\/b105236"},{"key":"2025030616183075234_j_itit-2024-0068_ref_015","doi-asserted-by":"crossref","unstructured":"A. Mahzoon, D. Gro\u00dfe, and R. Drechsler, \u201cRevsca-2.0: sca-based formal verification of nontrivial multipliers using reverse engineering and local vanishing removal,\u201d IEEE Trans. Comput. Aided Des. Integrated Circ. Syst., vol.\u00a041, no.\u00a05, pp.\u00a01573\u20131586, 2021.","DOI":"10.1109\/TCAD.2021.3083682"},{"key":"2025030616183075234_j_itit-2024-0068_ref_016","doi-asserted-by":"crossref","unstructured":"G. Fey and R. Drechsler, \u201cImproving simulation-based verification by means of formal methods,\u201d in ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No. 04EX753), IEEE, 2004, pp.\u00a0640\u2013643.","DOI":"10.1109\/ASPDAC.2004.1337670"},{"key":"2025030616183075234_j_itit-2024-0068_ref_017","unstructured":"S. Williams and M. Baxter, \u201cIcarus verilog: open-source verilog more than a year later,\u201d Linux J., vol.\u00a02002, no.\u00a099, p.\u00a03, 2002."},{"key":"2025030616183075234_j_itit-2024-0068_ref_018","unstructured":"T. Kropf, Introduction to Formal Hardware Verification, Heidelberg, Springer Berlin, 2013."},{"key":"2025030616183075234_j_itit-2024-0068_ref_019","unstructured":"R. Ebendt, G. Fey, and R. Drechsler, Advanced BDD Optimization, New York, NY, Springer, 2005."},{"key":"2025030616183075234_j_itit-2024-0068_ref_020","doi-asserted-by":"crossref","unstructured":"M. Ganai and A. Gupta, SAT-Based Scalable Formal Verification Solutions, New York, NY, Springer, 2007.","DOI":"10.1007\/978-0-387-69167-1"},{"key":"2025030616183075234_j_itit-2024-0068_ref_021","doi-asserted-by":"crossref","unstructured":"C. K. Jha, M. Hassan, and R. Drechsler, \u201ccecapprox: enabling automated combinational equivalence checking for approximate circuits,\u201d IEEE Trans. Circuits Syst. I: Regul. Pap., vol. 71, no. 7, pp. 3282\u20133293, 2024. https:\/\/doi.org\/10.1109\/tcsi.2024.3388256.","DOI":"10.1109\/TCSI.2024.3388256"},{"key":"2025030616183075234_j_itit-2024-0068_ref_035","doi-asserted-by":"crossref","unstructured":"Z. Vasicek, \u201cFormal methods for exact analysis of approximate circuits,\u201d IEEE Access, vol. 7, pp. 177309\u2013177331, 2019.","DOI":"10.1109\/ACCESS.2019.2958605"},{"key":"2025030616183075234_j_itit-2024-0068_ref_022","doi-asserted-by":"crossref","unstructured":"R. Brayton and A. Mishchenko, \u201cAbc: an academic industrial-strength verification tool,\u201d in Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15\u201319, 2010. Proceedings 22, Springer, 2010, pp.\u00a024\u201340.","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"2025030616183075234_j_itit-2024-0068_ref_023","doi-asserted-by":"crossref","unstructured":"A. Mishchenko, S. Chatterjee, R. Brayton, and N. Een, \u201cImprovements to combinational equivalence checking,\u201d in Proceedings of the 2006 IEEE\/ACM International Conference on Computer-Aided Design, 2006, pp.\u00a0836\u2013843.","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"2025030616183075234_j_itit-2024-0068_ref_024","unstructured":"J. M. Rabaey and B. Nikolic, Digital Integrated Circuits, vol. 2, New Jersey, Pearson Education, Inc, 2002."},{"key":"2025030616183075234_j_itit-2024-0068_ref_025","doi-asserted-by":"crossref","unstructured":"C. K. Jha, A. Mahzoon, and R. Drechsler, \u201cInvestigating various adder architectures for digital in-memory computing using magic-based memristor design style,\u201d in 2022 IEEE International Conference on Emerging Electronics, IEEE, 2022, pp.\u00a01\u20134.","DOI":"10.1109\/ICEE56203.2022.10117915"},{"key":"2025030616183075234_j_itit-2024-0068_ref_026","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Trans. Comput., vol.\u00a0100, no.\u00a08, pp.\u00a0677\u2013691, 1986. https:\/\/doi.org\/10.1109\/tc.1986.1676819.","DOI":"10.1109\/TC.1986.1676819"},{"key":"2025030616183075234_j_itit-2024-0068_ref_027","doi-asserted-by":"crossref","unstructured":"Akers, \u201cBinary decision diagrams,\u201d IEEE Trans. Comput., vol.\u00a0100, no.\u00a06, pp.\u00a0509\u2013516, 1978. https:\/\/doi.org\/10.1109\/tc.1978.1675141.","DOI":"10.1109\/TC.1978.1675141"},{"key":"2025030616183075234_j_itit-2024-0068_ref_028","doi-asserted-by":"crossref","unstructured":"R. Drechsler, \u201cPolyadd: polynomial formal verification of adder circuits,\u201d in 2021 24th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS), IEEE, 2021, pp.\u00a099\u2013104.","DOI":"10.1109\/DDECS52668.2021.9417052"},{"key":"2025030616183075234_j_itit-2024-0068_ref_029","unstructured":"A. Biere, \u201cThe AIGER and-inverter graph (AIG) format version 20071012,\u201d 2007. Available at: https:\/\/epub.jku.at\/obvulioa\/content\/titleinfo\/5971910."},{"key":"2025030616183075234_j_itit-2024-0068_ref_030","doi-asserted-by":"crossref","unstructured":"C. Yu, M. Ciesielski, and A. Mishchenko, \u201cFast algebraic rewriting based on and-inverter graphs,\u201d IEEE Trans. Comput. Aided Des. Integrated Circ. Syst., vol.\u00a037, no.\u00a09, pp.\u00a01907\u20131911, 2017. https:\/\/doi.org\/10.1109\/tcad.2017.2772854.","DOI":"10.1109\/TCAD.2017.2772854"},{"key":"2025030616183075234_j_itit-2024-0068_ref_031","unstructured":"C. Wolf, J. Glaser, and J. Kepler, \u201cYosys-a free verilog synthesis suite,\u201d in Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip), vol.\u00a097, 2013."},{"key":"2025030616183075234_j_itit-2024-0068_ref_032","unstructured":"F. Somenzi, CUDD: CU Decision Diagram Package Release 2.5.0, University of Colorado at Boulder, 2012."},{"key":"2025030616183075234_j_itit-2024-0068_ref_033","doi-asserted-by":"crossref","unstructured":"K. Qayyum, A. Mahzoon, and R. Drechsler, \u201cMonitoring the effects of static variable orders on the construction of bdds,\u201d in 2022 International Interdisciplinary Conference on Mathematics, Engineering and Science, IEEE, 2022, pp.\u00a01\u20136.","DOI":"10.1109\/MESIICON55227.2022.10093493"},{"key":"2025030616183075234_j_itit-2024-0068_ref_034","doi-asserted-by":"crossref","unstructured":"A. Mahzoon, D. Gro\u00dfe, and R. Drechsler, \u201cGenMul: generating architecturally complex multipliers to challenge formal verification tools,\u201d in Recent Findings in Boolean Techniques: Selected Papers from the 14th International Workshop on Boolean Problems, Springer, 2021, pp.\u00a0177\u2013191.","DOI":"10.1007\/978-3-030-68071-8_9"}],"container-title":["it - Information Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/itit-2024-0068\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/itit-2024-0068\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T16:19:47Z","timestamp":1741277987000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/itit-2024-0068\/html"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,1]]},"references-count":35,"journal-issue":{"issue":"4-5","published-online":{"date-parts":[[2025,3,3]]},"published-print":{"date-parts":[[2024,8,26]]}},"alternative-id":["10.1515\/itit-2024-0068"],"URL":"https:\/\/doi.org\/10.1515\/itit-2024-0068","relation":{},"ISSN":["1611-2776","2196-7032"],"issn-type":[{"type":"print","value":"1611-2776"},{"type":"electronic","value":"2196-7032"}],"subject":[],"published":{"date-parts":[[2024,8,1]]}}}