Generalized Affine Equivalence Checking of Boolean Functions via Reachability Analysis
Published In
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Document Type
Citation
Publication Date
9-1-2023
Abstract
We consider the problem of checking the generalized affine equivalence of two given Boolean functions. This problem arises in various computer-aided design (CAD) and cryptographic applications, such as circuit synthesis and Reed–Muller codes. Based on the theory of affine group acting on the Boolean functions, we define the coefficient spaces and transition relations, and transform the checking problem into reachability analysis of finite state machines. Two methods are proposed to check the affine equivalence of Boolean functions using binary decision diagrams (BDDs) and property directed reachability (PDR), respectively. Both methods can check affine equivalence of bent and semi-bent functions, which state-of-the-art methods can hardly handle. Furthermore, existing methods only consider the case of affine equivalence, while our methods can handle the generalized affine equivalence of subspaces of Boolean functions. In the application of circuit synthesis, our methods can significantly reduce the size of the library compared to Boolean matching. To classify Boolean functions up to the generalized affine equivalence, we propose a method to obtain a complete classification based on BDDs. In the experiments, we have successfully applied our methods to some examples that can hardly be solved by using the previous methods, thus, validating the effectiveness of our methods.
Rights
© IEEE
Locate the Document
DOI
10.1109/TCAD.2023.3235802
Persistent Identifier
https://archives.pdx.edu/ds/psu/40751
Publisher
IEEE
Citation Details
Zeng, X., Liang, H., Yuan, J., Song, X., & Yang, G. (2023). Generalized Affine Equivalence Checking of Boolean Functions via Reachability Analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.