{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T10:30:49Z","timestamp":1782383449266,"version":"3.54.5"},"reference-count":44,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2021,5,26]],"date-time":"2021-05-26T00:00:00Z","timestamp":1621987200000},"content-version":"vor","delay-in-days":145,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100011665","name":"Deanship of Scientific Research, King Saud University","doi-asserted-by":"publisher","award":["RGP-214"],"award-info":[{"award-number":["RGP-214"]}],"id":[{"id":"10.13039\/501100011665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009392","name":"Prince Sattam bin Abdulaziz University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100009392","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["Complexity"],"published-print":{"date-parts":[[2021,1]]},"abstract":"<jats:p>Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user\u2010friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called interactive theorem provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we (1) define two simple, one formal and the other informal, gate\u2010level hardware description languages, (2) design and develop a formal automatic combinational circuit equivalence checker (CoCEC) tool, and (3) test and evaluate our tool. The tool CoCEC is based on human\u2010assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human\u2010friendly user interface. It either returns a machine\u2010readable proof (term) of circuits\u2019 equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables (3.5\u2009 \u00d7 \u200910<jats:sup>13<\/jats:sup> states). CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course.<\/jats:p>","DOI":"10.1155\/2021\/5525539","type":"journal-article","created":{"date-parts":[[2021,5,26]],"date-time":"2021-05-26T16:07:48Z","timestamp":1622045268000},"update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["CoCEC: An Automatic Combinational Circuit Equivalence Checker Based on the Interactive Theorem Prover"],"prefix":"10.1155","volume":"2021","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0993-5964","authenticated-orcid":false,"given":"Wilayat","family":"Khan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7023-7172","authenticated-orcid":false,"given":"Farrukh Aslam","family":"Khan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6498-1528","authenticated-orcid":false,"given":"Abdelouahid","family":"Derhab","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7201-6963","authenticated-orcid":false,"given":"Adi","family":"Alhudhaif","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"311","published-online":{"date-parts":[[2021,5,26]]},"reference":[{"key":"e_1_2_14_1_2","volume-title":"Formal Equivalence Checking and Design Debugging","author":"Huang S. Y.","year":"2012"},{"key":"e_1_2_14_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/tcad.2002.804386"},{"key":"e_1_2_14_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0471-4"},{"key":"e_1_2_14_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/access.2019.2895261"},{"key":"e_1_2_14_5_2","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"e_1_2_14_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/s0065-2458(03)58003-2"},{"key":"e_1_2_14_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"e_1_2_14_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_14_9_2","unstructured":"WilliamM. Son of birdbrain II 2020 https:\/\/www.cs.unm.edu\/%7Emccune\/sobb\/."},{"key":"e_1_2_14_10_2","unstructured":"BarrasB. BoutinS. andCornesC. The Coq proof assistant reference manual: version 6.1 1997 Inria Rocquencourt France Ph.D. thesis."},{"key":"e_1_2_14_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_14_12_2","unstructured":"KaufmannM.andMooreJ. S. Acl2 automated prover 2020 https:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/."},{"key":"e_1_2_14_13_2","doi-asserted-by":"publisher","DOI":"10.3390\/electronics7060081"},{"key":"e_1_2_14_14_2","volume-title":"Survey of Existing Tools for Formal Verification","author":"Armstrong R. C.","year":"2014"},{"key":"e_1_2_14_15_2","volume-title":"Digital Logic and Computer Design","author":"Mano M. M.","year":"2017"},{"key":"e_1_2_14_16_2","volume-title":"Investigation of the Laws of Thought","author":"Boole G.","year":"1854"},{"key":"e_1_2_14_17_2","doi-asserted-by":"publisher","DOI":"10.2307\/1989325"},{"key":"e_1_2_14_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ee.1938.6431064"},{"key":"e_1_2_14_19_2","unstructured":"2018 Logic circuit simplification (SOP and POS).http:\/\/www.32x8.com\/."},{"key":"e_1_2_14_20_2","unstructured":"LeanR.andKryleM. QMSolver 2018 http:\/\/agila.upm.edu.ph\/%7Ekmmolina\/qms\/index.html."},{"key":"e_1_2_14_21_2","unstructured":"PierceB. C. CasinghinoC. andGaboardiM. Software Foundations. Webpage https:\/\/www.cis.upenn.edu\/bcpierce\/sf\/current\/index.html."},{"key":"e_1_2_14_22_2","doi-asserted-by":"publisher","DOI":"10.1155\/2020\/7346763"},{"key":"e_1_2_14_23_2","volume-title":"Principles of Compiler Design (Addison-Wesley Series in Computer Science and Information Processing)","author":"Aho A. V.","year":"1977"},{"key":"e_1_2_14_24_2","doi-asserted-by":"crossref","unstructured":"DelahayeD. A tactic language for the system Coq Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning May 2000 Alicante Spain Springer 85\u201395.","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_2_14_25_2","unstructured":"VCS Online Simulator 2015 http:\/\/www.edaplayground.com\/x\/FfR."},{"key":"e_1_2_14_26_2","unstructured":"Icarus Verilog 2016 http:\/\/www.icarus.com\/eda\/verilog\/."},{"key":"e_1_2_14_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-a"},{"key":"e_1_2_14_28_2","volume-title":"An Executable Formal Model of a Hardware Description Language","author":"Khan W.","year":"2017"},{"key":"e_1_2_14_29_2","unstructured":"Cadence Conformal Equivalence Checker 2021 https:\/\/www.cadence.com\/ko_KR\/home\/tools\/digital-design-and-signoff\/logic-equivalence-checking.html."},{"key":"e_1_2_14_30_2","unstructured":"Siemens FormalPro 2021 https:\/\/eda.sw.siemens.com\/en-US\/ic\/formalpro-equivalence-checking\/."},{"key":"e_1_2_14_31_2","volume-title":"Hardware Design Verification: Simulation and Formal Method-Based Approaches (Prentice Hall Modern Semiconductor Design Series)","author":"Lam W. K.","year":"2005"},{"key":"e_1_2_14_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/tc.1985.1676600"},{"key":"e_1_2_14_33_2","unstructured":"McCuneW. Prover9 and Mace4: version 2009-11A 2013."},{"key":"e_1_2_14_34_2","volume-title":"The State Explosion Problem. Lectures on Petri Nets I: Basic Models 1998","author":"Valmari A.","year":"1998"},{"key":"e_1_2_14_35_2","doi-asserted-by":"crossref","unstructured":"Coupet-GrimalS.andJakubiecL. Coq and hardware verification: a case study Lecture Notes in Computer Science Proceedings of the International Conference on Theorem Proving in Higher Order Logics August 1996 Munich Germany Springer 125\u2013139 https:\/\/doi.org\/10.1007\/bfb0105401.","DOI":"10.1007\/BFb0105401"},{"key":"e_1_2_14_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.01.002"},{"key":"e_1_2_14_37_2","doi-asserted-by":"crossref","unstructured":"MeredithP. KatelmanM. MeseguerJ. andRo\u015fuG. A formal executable semantics of verilog. Formal methods and models for codesign (MEMOCODE) Proceedings of the 8th IEEE\/ACM International Conference on IEEE May 2010 Massachusetts MA USA 179\u2013188.","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_2_14_38_2","doi-asserted-by":"crossref","unstructured":"ClavelM. Dur\u00e1nF. HendrixJ. LucasS. MeseguerJ. and\u00d6lveczkyP. The Maude formal tool environment Proceedings of the International Conference on Algebra and Coalgebra in Computer Science August 2007 Warsaw Poland Springer 173\u2013178.","DOI":"10.1007\/978-3-540-73859-6_12"},{"key":"e_1_2_14_39_2","doi-asserted-by":"crossref","unstructured":"BraibantT.andChlipalaA. Formal verification of hardware synthesis computer aided verification Proceedings of the International Conference on Computer Aided Verification July 2013 Los Angeles CA USA Springer 213\u2013228 https:\/\/doi.org\/10.1007\/978-3-642-39799-8_14 2-s2.0-84881160966.","DOI":"10.1007\/978-3-642-39799-8_14"},{"key":"e_1_2_14_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/tifs.2011.2160627"},{"key":"e_1_2_14_41_2","unstructured":"SondreR. MohamedA. andLarsD. Online database of boolean functions 2018 http:\/\/www.ii.uib.no\/%7Emohamedaa\/odbf\/index.html."},{"key":"e_1_2_14_42_2","unstructured":"WolframAlpha computational knowledge engine 2018 https:\/\/www.wolframalpha.com\/."},{"key":"e_1_2_14_43_2","unstructured":"Online minimization of boolean functions https:\/\/www.tma.main.jp\/logic\/index_en.html\/ ."},{"key":"e_1_2_14_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/tce.1953.6371932"}],"container-title":["Complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/complexity\/2021\/5525539.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/complexity\/2021\/5525539.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1155\/2021\/5525539","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,9]],"date-time":"2024-08-09T21:56:13Z","timestamp":1723240573000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1155\/2021\/5525539"}},"subtitle":[],"editor":[{"given":"Huihua","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"editor"}]}],"short-title":[],"issued":{"date-parts":[[2021,1]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["10.1155\/2021\/5525539"],"URL":"https:\/\/doi.org\/10.1155\/2021\/5525539","archive":["Portico"],"relation":{},"ISSN":["1076-2787","1099-0526"],"issn-type":[{"value":"1076-2787","type":"print"},{"value":"1099-0526","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1]]},"assertion":[{"value":"2021-01-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-04","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"5525539"}}