Constraint Solving for Synthesis and Verification of Threshold Logic Circuits
Journal
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Journal Volume
40
Journal Volume
40
Journal Issue
5
Journal Issue
5
Pages
904-917
Start Page
904
End Page
917
Date Issued
2021
Author(s)
Abstract
Threshold logic (TL) circuits gain increasing attention due to their feasible realization with emerging technologies and strong bind to neural network applications. In this work, we devise techniques for automatic synthesis and verification of TL circuits based on constraint solving. For synthesis, we formulate a fundamental operation to collapse TL functions, and derive a necessary and sufficient condition of collapsibility for linear combination of two TL functions. An approach based on solving the subset sum problem is proposed for fast circuit transformation. For verification, we propose a procedure to convert a TL function to a multiplexer (MUX) tree and to pseudo-Boolean (PB) constraints for formal Boolean and PB reasoning, respectively. Experiments on synthesis show that the collapse operation further reduces gate counts of synthesized TL circuits by an average of 18%. Experiments on verification demonstrate good scalability of the MUX-based method for equivalence checking of synthesized TL circuits, and efficiency of PB constraint conversion in cases where the conjunctive normal form (CNF) formula conversion and MUX tree conversion suffer from memory explosion.
Subjects
Boolean functions; Forestry; Logic circuits; Logic programming; Logic Synthesis; Threshold logic; Timing circuits; Circuit transformation; Conjunctive normal forms; Emerging technologies; Equivalence checking; Fundamental operations; Linear combinations; Neural network application; Subset sum problems; Computer circuits
SDGs
Type
journal article