research-article

A General Equivalence Checking Framework for Multivalued Logic

Authors:

Sheng-Hsiu Wei,

Yung-Chih Chen,

Chun-Yao WangAuthors Info & Claims

ASPDAC '21: Proceedings of the 26th Asia and South Pacific Design Automation Conference

Pages 61 - 66

https://doi.org/10.1145/3394885.3431588

Published: 29 January 2021 Publication History

Abstract

Logic equivalence checking is a critical task in the ASIC design flow. Due to the rapid development in nanotechnology-based devices, an efficient implementation of multivalued logic becomes practical. As a result, many synthesis algorithms for ternary logic were proposed. In this paper, we bring out an equivalence checking framework based on multivalued logic exploiting the modern SAT solvers. Furthermore, a structural conflict-driven clause learning (SCDCL) technique is also proposed to accelerate the SAT solving process. The SCDCL algorithm deploys some strategies to cut off the search space for SAT algorithms. The experimental results show that the proposed SCDCL technique saves 42% CPU time from SAT solvers on average over a set of industrial benchmarks.

References

[1]

C. M. Allen and D. D. Givone, "A minimization technique for multiple-valued logic systems," IEEE Trans. on Computers, vol. C-17, no. 2, pp. 182--184, 1968.

[2]

R. J. Bayardo Jr and R. C. Schrag, "Using CSP look-back techniques to solve real world SAT instances," in Proc. AAAI, pp. 203--208, 1997.

[3]

C. L. Berman and L. H. Trevillyan, "Functional comparison of logic designs for VLSI circuits," Proc. ICCAD, pp. 456--459, 1989.

[4]

A. Biere and W. Kunz, "SAT and ATPG: Boolean engines for formal hardware verification," Proc. ICCAD, pp. 782--785, 2002.

Digital Library

[5]

M.K. Ganai, A. Aziz, and A. Kuehlmann, "Enhancing simulation with BDDs and ATPG," in Proc. DAC, pp. 385--390, 1999.

[6]

T. A. Giuma, M.A. Tapia, "Canonical representation of multivalued logic functions," in Proc. IEEE Southeastcon, 1992

[7]

E. I. Goldberg, M. R. Prasad and R. K. Brayton, "Using SAT for combinational equivalence checking," in Proc. DATE, 2001.

[8]

J. Jain, R. Mukherjee, and M. Fujita, "Advanced verification technique based on learning," in Proc. DAC, pp. 420--426, 1995.

[9]

A. Kuehlmann and F. Krohm, "Equivalence checking using cuts and heaps," in Proc. DAC, pp. 263--268, 1997.

Digital Library

[10]

C. Y. Lee and W. H. Chen, "Several-valued combinational switching circuits," Trans. of the American Institute of Electrical Engineers, vol. 75, no. 3, pp. 278--283, 1956.

[11]

S. Lin, Y.-B. Kim, and F. Lombardi, "A novel CNTFET-based ternary logic gate design," in Proc. International Midwest Symposium on Circuits and Systems, 2009

[12]

J. P. Marques-Silva and K. A. Sakallah, "GRASP-A new search algorithm for satisfiability," in Proc. ICCAD, pp. 220--227, 1996.

[13]

J. P. Marques-Silva and K. A. Sakallah, "GRASP: A search algorithm for propositional satisfiability," IEEE Trans. on Computers, pp. 506--521, 1999.

Digital Library

[14]

E.J. McCluskey, "Minimization of Boolean functions," Bell Syst. tech J., vol. 35, no. 5, pp. 1417--1444, Nov. 1956.

[15]

A. Mishchenko, R. Brayton, J.-H. Jiang, and S. Jang, "Scalable don't-care-based logic optimization and resynthesis," in International Symposium on FPGA, pp. 151--160, 2009

[16]

S. M. Reddy, W. Kunz, and D. K. Pradhan, "Novel verification framework combining structural and OBDD methods in a synthesis environment," in Proc. DAC, pp. 414--419, 1995.

[17]

T. Sasao, "Ternary decision diagrams," in Proc. International Symposium on Multiple-Valued Logic, 1997.

[18]

N. Soliman, M. E. Fouda, and A. G. Radwan, "Memristor-CNTFET based ternary logic gates," Microelectronics Journal, vol. 72, pp. 74--85, 2018.

[19]

N. Soliman, M. E. Fouda, A. G. Alhurbi, L. A. Said, A. H. Madian, and A. G. Radwan, "Ternary functions design using memristive threshold logic," IEEE Access, vol. 7, 2019.

[20]

B. Srinivasu and K. Sridharan, "A synthesis methodology for ternary logic circuits in emerging device technologies," IEEE Trans. on Circuits and Systems, vol. 64, no. 8, pp. 2146--2159, 2017.

[21]

S. Y. H. Su, and P. T. Cheung, "Computer minimization of multivalued switching functions," IEEE Trans. on Computers, vol. C-21, no. 9, pp. 995--1003, 1972.

[22]

G. Tseitin, "On the complexity of derivation in propositional calculus," Studies in constructive mathematics and mathematical logic, vol. 2, no. 115--125, pp. 10--13, 1968.

[23]

Z. G. Vranesic, E. S. Lee, and K. C. Smith, "A many-valued algebra for switching systems," IEEE Trans. on Computers, vol. C-19, no. 10, pp. 964--971, 1970.

[24]

C. Vudadha, A. Surya, S. Agrawal and M. B. Srinivas, "Synthesis of ternary logic circuits using 2:1 multiplexers", IEEE Trans. on Circuits and Systems, vol. 65, no. 12, pp. 4313--4325, 2018.

[25]

L. Zhang, C. F. Madigan, M. H. Moskewicz and S. Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver," Proc. ICCAD, 2001.

[26]

IEEE Standard Verilog Hardware Description Language, in IEEE Standard 1364-2005.

[27]

Berkeley Logic Synthesis and Verification Group, "ABC: a system for sequential synthesis and verification," Available: https://people.eecs.berkeley.edu/~alanmi/abc/.

[28]

https://www.labri.fr/perso/lsimon/glucose/.

[29]

https://github.com/arminbiere/cadical/.

[30]

http://iccad-contest.org/2020/problems.html

Cited By

Wang YLuo YChien PWang PWang HLin WJiang JHuang C(2021)Compatible Equivalence Checking of X-Valued Circuits2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643515(1-9)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643515

A General Equivalence Checking Framework for Multivalued Logic
1. Hardware
  1. Integrated circuits

Recommendations

Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
Abstract
Finite transducers, two-tape automata, and biautomata are related computational models descended from the concept of finite-state automaton. In these models an automaton controls two heads that read or write symbols on the tapes in the one-way ...
Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints

For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates ...
DP Lower bounds for equivalence-checking and model-checking of one-counter automata

We present a general method for proving DP-hardness of problems related to formal verification of one-counter automata. For this we show a reduction of the SAT-UNSAT problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPDAC '21: Proceedings of the 26th Asia and South Pacific Design Automation Conference

January 2021

930 pages

ISBN:9781450379991

DOI:10.1145/3394885

Copyright © 2021 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
IEEE CAS
IEEE CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 January 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Ministry of Science and Technology, Taiwan

Conference

ASPDAC '21

Sponsor:

SIGDA

ASPDAC '21: 26th Asia and South Pacific Design Automation Conference

January 18 - 21, 2021

Tokyo, Japan

Acceptance Rates

ASPDAC '21 Paper Acceptance Rate 111 of 368 submissions, 30%;

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

1
Total Citations
View Citations
92
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang YLuo YChien PWang PWang HLin WJiang JHuang C(2021)Compatible Equivalence Checking of X-Valued Circuits2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643515(1-9)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643515

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents