Download pdf
Combinational Equivalence Checking on AIGs
- 1 Shenzhen Middle School, Luohu District, Shenzhen, Guangdong, China
* Author to whom correspondence should be addressed.
Abstract
Combinational Equivalence Checking (CEC) is a critical process in digital circuit design, ensuring that two versions of a circuit are functionally equivalent. Functionally Reduced And-Inverter Graphs (FRAIGs) are a data structure extensively used in CEC, representing Boolean functions as directed acyclic graphs with AND gates and inverters. The main advantage of FRAIGs is their ability to integrate structural hashing with functional reduction, allowing for the elimination of functionally equivalent nodes during graph construction. However, conventional FRAIG approaches face challenges with scalability in complex circuits. To overcome these limitations, we propose three novel methods: improved sampling techniques that refine random simulation and SAT-based methods for early identification of equivalent nodes; advanced graph partitioning strategies that enable parallel processing and localized equivalence checking to accelerate computation; and support node analysis combined with probability distribution modeling to reduce unnecessary checks. Extensive experiments show the effectiveness and efficiency of our proposed methods
Keywords
Logic Synthesis, And-Inverter Graphs, Combinational Equivalence Checking, Graph Partition
[1]. L. Amar´u, F. Marranghello, E. Testa, C. Casares, V. Possani, J. Luo, P. Vuillod, A. Mishchenko, and G. De Micheli. Sat-sweeping enhanced for logic synthesis. In 2020 57th ACM/IEEE Design Automation Conference (DAC), pages 1–6. IEEE, 2020.
[2]. M. Backes, J. M. Matos, R. Ribas, and A. Reis. Reviewing aig equivalence checking approaches. In Proceedings of the ACM Microelectronics Student Forum, pages 1–4, 2014.
[3]. S. Chatterjee and N. Een. Improvements to combinational equivalence checking.
[4]. A. Mishchenko, S. Chatterjee, R. Brayton, and N. Een. Improvements to combinational equivalence checking. In Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, pages 836–843, 2006.
[5]. Q. Zhu, N. Kitchen, A. Kuehlmann, and A. Sangiovanni-Vincentelli. Sat sweeping with local observability don’t-cares. In Proceedings of the 43rd Annual Design Automation Conference, pages 229–234, 2006.
[6]. A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton. Fraigs: A unifying representation for logic synthesis and verification. Technical report, ERL Technical Report, 2005.
[7]. C. Yu, M. Ciesielski, and A. Mishchenko. Fast algebraic rewriting based on and-inverter graphs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(9):1907–1911, 2017.
[8]. N. E´en and N. S¨orensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pages 502–518. Springer, 2003.
[9]. W. Gong and X. Zhou. A survey of sat solver. In AIP Conference Proceedings, volume 1836. AIP Publishing, 2017.
[10]. Y. Hamadi, S. Jabbour, and L. Sais. Manysat: a parallelsat solver. Journal on Satisfiability, Boolean Modeling and Computation, 6(4):245–262, 2010.
[11]. R. Brayton and A. Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, pages 24–40, 2010.
[12]. L. Amar´u, P.-E. Gaillardon, and G. De Micheli. The epfl combinational benchmark suite. In Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS), 2015.
Cite this article
Tang,L. (2025). Combinational Equivalence Checking on AIGs. Theoretical and Natural Science,87,91-102.
Data availability
The datasets used and/or analyzed during the current study will be available from the authors upon reasonable request.
Disclaimer/Publisher's Note
The statements, opinions and data contained in all publications are solely those of the individual author(s) and contributor(s) and not of EWA Publishing and/or the editor(s). EWA Publishing and/or the editor(s) disclaim responsibility for any injury to people or property resulting from any ideas, methods, instructions or products referred to in the content.
About volume
Volume title: Proceedings of the 4th International Conference on Computing Innovation and Applied Physics
© 2024 by the author(s). Licensee EWA Publishing, Oxford, UK. This article is an open access article distributed under the terms and
conditions of the Creative Commons Attribution (CC BY) license. Authors who
publish this series agree to the following terms:
1. Authors retain copyright and grant the series right of first publication with the work simultaneously licensed under a Creative Commons
Attribution License that allows others to share the work with an acknowledgment of the work's authorship and initial publication in this
series.
2. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the series's published
version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgment of its initial
publication in this series.
3. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and
during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See
Open access policy for details).