Kuo-Hua Wang
ABSTRACT
Boolean matching is to check the equivalence of two target functions under input permutation and input/output phase assignment. This paper addresses the permutation independent (P-equivalent) Boolean matching problem. We will propose a matching algorithm seamlessly integrating Simulation and Boolean Satisfiability (S&S) techniques. Our proposed algorithm will first utilize functional properties like unateness and symmetry to reduce the searching space. In the followed simulation phase, three types of input vector generation and checking method will be used to match the inputs of two target functions. Experimental results on large benchmarking circuits demonstrate that our matching algorithm is indeed very effective and efficient to solve Boolean matching for large Boolean networks.
- A. Mishchenko, S. Chatterjee, R. Brayton, and N. En, "Improvements to Combinational Equivalence Checking," in Proc. of Internatioanl Conference on Computer-Aided Design, pp. 836--843, Nov. 2006. Google Scholar
Digital Library
- S. Plaza, K. Chang, I. Markov, and V. Bertacco, "Node Mergers in the Presence of Don't Cares," in Proc. of Asia and South Pacific Design Automation Conference, pp. 414--419, Jan. 2007. Google ScholarDigital Library
- Qi Zhu, N. Kitchen, A. Kuehlmann, A. Sangiovanni-Vincentelli, "SAT Sweeping with Local Observability Don't-Cares," in Proc. of Design Automation Conference, pp. 229--234, July 2006. Google ScholarDigital Library
- A. Mishchenko, et. al, "Using Simulation and Satisfiability to Compute Flexibilities in Boolean Networks," IEEE Transaction on Computer-Aided-Design of Integrated Circuits and Systems, Vol. 25, No. 5, pp. 743--755, May 2006. Google ScholarDigital Library
- L. Benini and G. De Micheli, "A Survey of Boolean Matching Techniques for Library Binding," ACM Trans. on Design Automation of Electronic Systems, Vol. 2, No. 3, pp. 193--226, July 1997. Google ScholarDigital Library
- Afshin Abdollahi, "Signature Based Boolean Matching in the Presence of Don't Cares," in Proc. of Design Automation Conference, pp. 642--647, June 2008. Google ScholarDigital Library
- G. Agosta, et. al, "A Unified Approach to Canonical Form-based Boolean Matching," in Proc. of Design Automation Conference, pp. 841--846, June 2007. Google ScholarDigital Library
- A. Abdollahi and M. Pedram, "A New Canonical Form for Fast Boolean Matching in Logic Synthesis and Verification," in Proc. of Design Automation Conference, pp. 379--384, June 2005. Google ScholarDigital Library
- K. H. Wang and Chung-Ming Chan, "Incremental Learning Approach and SAT Model for Boolean Matching with Don't Cares," in Proc. of International Conference on Computer-Aided Design, pp. 234--239, November 2007. Google ScholarDigital Library
- A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ranai, "Robust Boolean Reasoning for Equivalence Checking and Functioanl Property Verification," IEEE Transaction on Computer-Aided-Design of Integrated Circuits and Systems, Vol. 21, No. 12., pp. 1377--1394, Dec. 2002. Google ScholarDigital Library
- J. Mohnke, P. Molitor, and S. Malik, "Limits of Using Signatures for Permutation Independent Boolean Comparison," in Proc. of ASP Deisgn Automaiton Conference, pp. 459--464, 1995. Google ScholarDigital Library
- A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton, "FRAIGS: A Unifying Representation for Logic Synthesis and Verification," ERL Technical Report, EECS Dept., UC Berkeley, March 2005.Google Scholar
- J. Marques-Silva and K. A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computer-Aided-Design of Integrated Circuits and Systems, Vol. 48, No. 5, pp. 506--521, May 1999. Google ScholarDigital Library
- M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," in Proc. of Design Automation Conference, pp. 530--535, June 2001. Google ScholarDigital Library
- J. P. Marques-Silva and K. A. Sakallah, "Boolean Satisfiability in Electronic Design Automation," in Proc. of Design Automation Conference, pp. 675--680, June 2000. Google ScholarDigital Library
Index Terms
- Simulation and SAT-based Boolean matching for large Boolean networks
Recommendations
Signature based Boolean matching in the presence of don't cares
DAC '08: Proceedings of the 45th annual Design Automation ConferenceBoolean matching is to determine whether two functions are equivalent under input permutation and input/output phase assignment. This paper will address the Boolean Matching problem for incompletely specified functions. Signatures have previously been ...
Efficient SAT-based Boolean matching for FPGA technology mapping
DAC '06: Proceedings of the 43rd annual Design Automation ConferenceMost FPGA technology mapping approaches either target Lookup Tables (LUTs) or relatively simple Programmable Logic Blocks (PLBs). Considering networks of PLBs during technology mapping has the potential of providing unique optimizations unavailable ...
Improved SAT-based Boolean matching using implicants for LUT-based FPGAs
FPGA '07: Proceedings of the 2007 ACM/SIGDA 15th international symposium on Field programmable gate arraysBoolean matching (BM) is a widely used technique in FPGA resynthesis and architecture evaluation. In this paper we present several improvements to the recently proposed SAT-based Boolean matching formulation (SAT-BM-M) [11]. The principal improvement ...
Comments