-
A Canonical-based NPN Boolean Matching Algorithm Utilizing Boolean Difference and Cofactor Signature
Authors:
Juling Zhang,
Guowu Yang,
William N. N. Hung,
Jinzhao Wu
Abstract:
This paper presents a new compact canonical-based algorithm to solve the problem of single-output completely specified NPN Boolean matching. We propose a new signature vector Boolean difference and cofactor (DC) signature vector. Our algorithm utilizes the Boolean difference, cofactor signature and symmetry properties to search for canonical transformations. The use of symmetry and Boolean differe…
▽ More
This paper presents a new compact canonical-based algorithm to solve the problem of single-output completely specified NPN Boolean matching. We propose a new signature vector Boolean difference and cofactor (DC) signature vector. Our algorithm utilizes the Boolean difference, cofactor signature and symmetry properties to search for canonical transformations. The use of symmetry and Boolean difference notably reduces the search space and speeds up the Boolean matching process compared to the algorithm proposed in [1]. We tested our algorithm on a large number of circuits. The experimental results showed that the average runtime of our algorithm 37% higher and its average search space 67% smaller compared to [1] when tested on general circuits.
△ Less
Submitted 9 November, 2017;
originally announced November 2017.
-
An Efficient NPN Boolean Matching Algorithm Based on Structural Signature and Shannon Expansion
Authors:
Juling Zhang,
Guowu Yang,
William N. N. Hung,
Yan Zhang
Abstract:
An efficient pairwise Boolean matching algorithm to solve the problem of matching single-output specified Boolean functions under input negation and/or input permutation and/or output negation (NPN) is proposed in this paper. We present the Structural Signature (SS) vector, which is composed of a 1st signature value, two symmetry marks, and a group mark. As a necessary condition for NPN Boolean ma…
▽ More
An efficient pairwise Boolean matching algorithm to solve the problem of matching single-output specified Boolean functions under input negation and/or input permutation and/or output negation (NPN) is proposed in this paper. We present the Structural Signature (SS) vector, which is composed of a 1st signature value, two symmetry marks, and a group mark. As a necessary condition for NPN Boolean matching, the structural signature is more effective than is the traditional signature. Two Boolean functions, f and g, may be equivalent when they have the same SS vector. The symmetry mark can distinguish symmetric variables and asymmetric variables and search multiple variable mappings in a single variable-mapping search operation, which reduces the search space significantly. Updating the SS vector using Shannon decomposition provides benefits in distinguishing unidentified variables, and the group mark and the phase collision check discover incorrect variable mappings quickly, which also speeds up the NPN Boolean matching process. Using the algorithm proposed in this paper, we tested both equivalent and non-equivalent matching peeds on the MCNC benchmark circuit sets and the random circuit sets. In the experiment, our algorithm is two times faster than competitors when testing equivalent circuits and averages at least one hundred times faster when testing non-equivalent circuits. The experimental results show that our approach is highly effective in solving the NPN Boolean matching problem.
△ Less
Submitted 9 November, 2017; v1 submitted 11 August, 2017;
originally announced August 2017.
-
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
Authors:
Hui Kong,
Fei He,
Xiaoyu Song,
William N. N. Hung,
Ming Gu
Abstract:
A barrier certificate is an inductive invariant function which can be used for the safety verification of a hybrid system. Safety verification based on barrier certificate has the benefit of avoiding explicit computation of the exact reachable set which is usually intractable for nonlinear hybrid systems. In this paper, we propose a new barrier certificate condition, called Exponential Condition,…
▽ More
A barrier certificate is an inductive invariant function which can be used for the safety verification of a hybrid system. Safety verification based on barrier certificate has the benefit of avoiding explicit computation of the exact reachable set which is usually intractable for nonlinear hybrid systems. In this paper, we propose a new barrier certificate condition, called Exponential Condition, for the safety verification of semi-algebraic hybrid systems. The most important benefit of Exponential Condition is that it has a lower conservativeness than the existing convex condition and meanwhile it possesses the property of convexity. On the one hand, a less conservative barrier certificate forms a tighter over-approximation for the reachable set and hence is able to verify critical safety properties. On the other hand, the property of convexity guarantees its solvability by semidefinite programming method. Some examples are presented to illustrate the effectiveness and practicality of our method.
△ Less
Submitted 27 March, 2013;
originally announced March 2013.
-
Exact Synthesis of 3-Qubit Quantum Circuits from Non-Binary Quantum Gates Using Multiple-Valued Logic and Group Theory
Authors:
Guowu Yang,
William N. N. Hung,
Xiaoyu Song,
Marek Perkowski
Abstract:
We propose an approach to optimally synthesize quantum circuits from non-permutative quantum gates such as Controlled-Square-Root-of-Not (i.e. Controlled-V). Our approach reduces the synthesis problem to multiple-valued optimization and uses group theory. We devise a novel technique that transforms the quantum logic synthesis problem from a multi-valued constrained optimization problem to a grou…
▽ More
We propose an approach to optimally synthesize quantum circuits from non-permutative quantum gates such as Controlled-Square-Root-of-Not (i.e. Controlled-V). Our approach reduces the synthesis problem to multiple-valued optimization and uses group theory. We devise a novel technique that transforms the quantum logic synthesis problem from a multi-valued constrained optimization problem to a group permutation problem. The transformation enables us to utilize group theory to exploit the properties of the synthesis problem. Assuming a cost of one for each two-qubit gate, we found all reversible circuits with quantum costs of 4, 5, 6, etc, and give another algorithm to realize these reversible circuits with quantum gates.
△ Less
Submitted 25 October, 2007;
originally announced October 2007.
-
Defect-Tolerant CMOL Cell Assignment via Satisfiability
Authors:
William N. N. Hung,
Changjian Gao,
Xiaoyu Song,
Dan Hammerstrom
Abstract:
We present a CAD framework for CMOL, a hybrid CMOS/ molecular circuit architecture. Our framework first transforms any logically synthesized circuit based on AND/OR/NOT gates to a NOR gate circuit, and then maps the NOR gates to CMOL. We encode the CMOL cell assignment problem as boolean conditions. The boolean constraint is satisfiable if and only if there is a way to map all the NOR gates to t…
▽ More
We present a CAD framework for CMOL, a hybrid CMOS/ molecular circuit architecture. Our framework first transforms any logically synthesized circuit based on AND/OR/NOT gates to a NOR gate circuit, and then maps the NOR gates to CMOL. We encode the CMOL cell assignment problem as boolean conditions. The boolean constraint is satisfiable if and only if there is a way to map all the NOR gates to the CMOL cells. We further investigate various types of static defects for the CMOL architecture, and propose a reconfiguration technique that can deal with these defects through our CAD framework. This is the first automated framework for CMOL cell assignment, and the first to model several different CMOL static defects. Empirical results show that our approach is efficient and scalable.
△ Less
Submitted 29 May, 2007;
originally announced May 2007.
