A Grover-Meets-Simon Approach to Match Vector Boolean Functions

The Boolean matching problem via NP-equivalence requires determining whether two Boolean functions are equivalent or not up to a permutation and negation of the input binary variables. Its solution is a fundamental step in the electronic design automation (EDA) tool chains commonly used for digital...

Full description

Saved in:
Bibliographic Details
Main Authors: Marco Venere, Alessandro Barenghi, Gerardo Pelosi
Format: Article
Language:English
Published: IEEE 2025-01-01
Series:IEEE Transactions on Quantum Engineering
Subjects:
Online Access:https://ieeexplore.ieee.org/document/11108706/
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The Boolean matching problem via NP-equivalence requires determining whether two Boolean functions are equivalent or not up to a permutation and negation of the input binary variables. Its solution is a fundamental step in the electronic design automation (EDA) tool chains commonly used for digital circuit design. In fact, the <italic>library-mapping</italic> step of an EDA workflow requires matching parts of the gate-level design (<italic>netlist</italic>) with the components available in a technology library, considering them as Boolean functions, while taking into account that permutations and negations of input variables can be efficiently implemented through rewiring and the use of inverters. For <inline-formula><tex-math notation="LaTeX">$n$</tex-math></inline-formula>-to-<inline-formula><tex-math notation="LaTeX">$n$</tex-math></inline-formula> vector Boolean functions, where <inline-formula><tex-math notation="LaTeX">$n$</tex-math></inline-formula> is the number of input and output variables, the search space of possible negations and permutations is super-exponential in size, while the <inline-formula><tex-math notation="LaTeX">$\mathcal {O}(n!n2^{2n})$</tex-math></inline-formula> time complexity of classical approaches allows solving only small instances of the NP-problem, often limited to <inline-formula><tex-math notation="LaTeX">$n$</tex-math></inline-formula>-to-1 Boolean functions (executing <inline-formula><tex-math notation="LaTeX">$\mathcal {O}(n!2^{2n})$</tex-math></inline-formula> bit operations). This work presents a quantum algorithm for matching <inline-formula><tex-math notation="LaTeX">$n$</tex-math></inline-formula>-to-<inline-formula><tex-math notation="LaTeX">$n$</tex-math></inline-formula> vector Boolean functions by effectively combining the Grover-meets-Simon approach with an original and novel use of the Simon solver without the constraints imposed by its usual premises. We provide a fully detailed quantum circuit implementing our proposal, calculate its cost by evaluating key performance indicators for circuit synthesis, and show an exponential speedup over classical solutions. Finally, we validate our approach on the Boolean functions included in the ISCAS benchmark suite, which are of practical interest in EDA.
ISSN:2689-1808