research-article

Public Access

Spectral approach to verifying non-linear arithmetic circuits

Authors:

Maciej CiesielskiAuthors Info & Claims

ASPDAC '19: Proceedings of the 24th Asia and South Pacific Design Automation Conference

Pages 261 - 267

https://doi.org/10.1145/3287624.3287662

Published: 21 January 2019 Publication History

Abstract

This paper presents a fast and effective computer algebraic method for analyzing and verifying non-linear integer arithmetic circuits using a novel algebraic spectral model. It introduces a concept of algebraic spectrum, a numerical form of polynomial expression; it uses the distribution of coefficients of the monomials to determine the type of arithmetic function under verification. In contrast to previous works, the proof of functional correctness is achieved by computing an algebraic spectrum combined with local rewriting of word-level polynomials. The speedup is achieved by propagating coefficients through the circuit using And-Inverter Graph (AIG) datastructure. The effectiveness of the method is demonstrated with experiments including standard and Booth multipliers, and other synthesized non-linear arithmetic circuits up to 1024 bits containing over 12 million gates.

References

[1]

Armin Biere. 2013. Lingeling, plingeling and treengeling entering the sat competition 2013. Proceedings of SAT Competition (2013), 51--52.

[2]

Randal E Bryant. 1986. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers 100, 8 (1986), 677--691.

Digital Library

[3]

Yirng-An Chen and Randal Bryant. 1997. <sup>*</sup>PHDD: An Efficient Graph Representation for Floating Point Circuit Verification. Technical Report CMU-CS-97-134. School of Computer Science, Carnegie Mellon University.

[4]

M. Ciesielski, P. Kalla, and S. Askar. 2006. Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs. IEEE Trans. on Computers 55, 9 (Sept. 2006), 1188--1201.

Digital Library

[5]

M Ciesielski, C Yu, W Brown, D Liu, and André Rossi. 2015. Verification of Gate-level Arithmetic Circuits by Function Extraction. In 52nd DAC. ACM, 52--57.

Digital Library

[6]

Farimah Farahmandi and Prabhat Mishra. 2016. Automated Test Generation for Debugging Arithmetic Circuits. In Proceedings of the conference on Design, automation and test in Europe (DATE). EDA Consortium.

Digital Library

[7]

Saman Froehlich, Daniel Große, and Rolf Drechsler. 2018. Approximate hardware generation using symbolic computer algebra employing grobner basis. In Design, Automation & Test in Europe Conference & Exhibition (DATE), 2018. IEEE, 889--892.

[8]

Samaneh Ghandali, Cunxi Yu, Duo Liu, Brown Walter, and Maciej Ciesielski. 2015. Logic Debugging of Arithmetic Circuits. In IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE, 113--118.

[9]

Evgueni Goldberg, Mukul Prasad, and Robert Brayton. 2001. Using SAT for combinational equivalence checking. In Proceedings of the conference on Design, automation and test in Europe. IEEE Press, 114--121.

Digital Library

[10]

Naofumi Homma, Yuki Watanabe, Takafumi Aoki, and Tatsuo Higuchi. 2006. Formal design of arithmetic circuits based on arithmetic description language. IEICE transactions on fundamentals of electronics, communications and computer sciences 89, 12 (2006), 3500--3509.

Digital Library

[11]

Zheng Huang, Lingli Wang, Yakov Nasikovskiy, and Alan Mishchenko. 2013. Fast Boolean matching based on NPN classification. In FPT'13.

[12]

Andreas Kuehlmann and Florian Krohm. 1997. Equivalence checking using cuts and heaps. In DAC'97. ACM, 263--268.

Digital Library

[13]

Alireza Mahzoon, Daniel Große, and Rolf Drechsler. 2018. Combining Symbolic Computer Algebra and Boolean Satisfiability for Automatic Debugging and Fixing of Complex Multipliers. In ISVLSI'18. IEEE, 351--356.

[14]

Alan Mishchenko et al. 2007. ABC: A system for sequential synthesis and verification. URL http://www.eecs.berkeley.edu/~alanmi/abc (2007).

[15]

Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton. 2006. DAG-aware AIG Rewriting: A Fresh Look at Combinational Logic Synthesis. In 43rd DAC. ACM, 532--535.

Digital Library

[16]

Aina Niemetz, Mathias Preiner, and Armin Biere. 2015. Boolector 2.0. Journal on Satisfiability, Boolean Modeling and Computation 9 (2015).

[17]

E. Pavlenko, M. Wedler, D. Stoffel, W. Kunz, et al. 2011. STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra. In DATE. 155--160.

[18]

Tim Pruss, Priyank Kalla, and Florian Enescu. 2016. Efficient Symbolic Computation for Word-Level Abstraction From Combinational Circuits for Verification Over Finite Fields. TCAD'16 35, 7 (2016), 1206--1218.

Digital Library

[19]

Daniela Ritirc, Armin Biere, and Manuel Kauers. 2017. Column-wise verification of multipliers using computer algebra. In FMCAD'17.

Digital Library

[20]

Daniela Ritirc, Armin Biere, and Manuel Kauers. 2018. Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers. In DATE'18.

[21]

Amr Sayed-Ahmed, Daniel Große, Ulrich Kühne, Mathias Soeken, and Rolf Drechsler. 2016. Formal Verification of Integer Multipliers by Combining Grobner Basis with Logic Reduction. In DATE'16. 1--6.

Digital Library

[22]

Mathias Soeken, Baruch Sterin, Rolf Drechsler, and Robert Brayton. {n. d.}. Simulation Graphs for Reverse Engineering. FMCAD 2015 ({n. d.}).

Digital Library

[23]

Niklas Sorensson and Niklas Een. 2005. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT 2005 (2005), 53.

[24]

Tiankai Su, Atif Yasin, Cunxi Yu, and Maciej Ciesielski. 2018. Computer Algebraic Approach to Verification and Debugging of Galois Field Multipliers. In Circuits and Systems (ISCAS), 2018 IEEE International Symposium on. IEEE, 1--5.

[25]

Cunxi Yu, Walter Brown, Duo Liu, André Rossi, and Maciej J. Ciesielski. 2016. Formal Verification of Arithmetic Circuits using Function Extraction. IEEE Trans. on CAD of Integrated Circuits and Systems 35, 12 (2016), 2131--2142.

Digital Library

[26]

Cunxi Yu, Maciej Ciesielski, and Alan Mishchenko. 2018. Fast Algebraic Rewriting Based on And-Inverter Graphs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37, 9 (2018), 1907--1911.

Digital Library

[27]

Cunxi Yu and Maciej J. Ciesielski. 2016. Automatic word-level abstraction of datapath. In ISCAS'16. 1718--1721.

Cited By

Ciesielski MYasin ADasari J(2022)Functional Verification of Arithmetic Circuits: Survey of Formal Methods2022 25th International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS)10.1109/DDECS54261.2022.9770161(94-99)Online publication date: 6-Apr-2022
https://doi.org/10.1109/DDECS54261.2022.9770161
Abed SAlMehteb MMansoor WGawanmeh A(2020)Verification of Non-linear Arithmetic Circuits using Functionally Reduced And-Inverter-Graph (FRAIG)2020 Global Congress on Electrical Engineering (GC-ElecEng)10.23919/GC-ElecEng48342.2020.9285982(118-123)Online publication date: 4-Sep-2020
https://doi.org/10.23919/GC-ElecEng48342.2020.9285982

Spectral approach to verifying non-linear arithmetic circuits
1. Hardware
  1. Integrated circuits
    1. Logic circuits

Recommendations

Multiple-Valued Arithmetic Integrated Circuits Based on 1.5V-Supply Dual-Rail Source-Coupled Logic
ISMVL '95: Proceedings of the 25th International Symposium on Multiple-Valued Logic

Abstract: This paper presents a new multiple-valued current-mode MOS integrated circuit for high-speed arithmetic systems with a low supply voltage. The use of a multiple-valued source-coupled logic circuit with dual-rail complementary inputs makes a ...
High-Level Design of Multiple-Valued Arithmetic Circuits Based on Arithmetic Description Language
ISMVL '08: Proceedings of the 38th International Symposium on Multiple Valued Logic

This paper proposes a high-level design method of multiple-valued arithmetic circuits. The proposed method uses a cell-based approach with a dedicated hardware description language called ARITH. By using ARITH, we can describe and verify any binary/...
Formal Design of Arithmetic Circuits Based on Arithmetic Description Language

This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPDAC '19: Proceedings of the 24th Asia and South Pacific Design Automation Conference

January 2019

794 pages

ISBN:9781450360074

DOI:10.1145/3287624

General Chair:
Toshiyuki Shibuya
Fujitsu Laboratories

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation

In-Cooperation

IEICE ESS: Institute of Electronics, Information and Communication Engineers, Engineering Sciences Society
IEEE CAS
IEEE CEDA
IPSJ SIG-SLDM: Information Processing Society of Japan, SIG System LSI Design Methodology

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

ASPDAC '19

Sponsor:

SIGDA

ASPDAC '19: 24th Asia and South Pacific Design Automation Conference

January 21 - 24, 2019

Tokyo, Japan

Acceptance Rates

Overall Acceptance Rate 466 of 1,454 submissions, 32%

Upcoming Conference

ASPDAC '25

Sponsor:
sigda

30th Asia and South Pacific Design Automation Conference

January 20 - 23, 2025

Tokyo , Japan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
240
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)11

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ciesielski MYasin ADasari J(2022)Functional Verification of Arithmetic Circuits: Survey of Formal Methods2022 25th International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS)10.1109/DDECS54261.2022.9770161(94-99)Online publication date: 6-Apr-2022
https://doi.org/10.1109/DDECS54261.2022.9770161
Abed SAlMehteb MMansoor WGawanmeh A(2020)Verification of Non-linear Arithmetic Circuits using Functionally Reduced And-Inverter-Graph (FRAIG)2020 Global Congress on Electrical Engineering (GC-ElecEng)10.23919/GC-ElecEng48342.2020.9285982(118-123)Online publication date: 4-Sep-2020
https://doi.org/10.23919/GC-ElecEng48342.2020.9285982

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents