can be seen, the average runtime is proportional to the number of the outputs.
Figure 4.9: Runtime of multi-output Ashenhurst decomposition
4.5 Quality of Composite Functions
We take benchmark circuit s9234 as an example to show the circuit information of functions g and h derived from Ashenhurst decomposition. The results are shown in Table 4.4.
The first column indicates the different efforts we applied to the test cases before we feed it into the algorithm. “Sin” and “Dul” denote the single- and two-output Ashenhurst decomposition, respectively. “Clp” denotes ABC commands collapse and strash are further applied to collapse and structure hash a circuit. “Syn”
de-4.5. Quality of Composite Functions
notes ABC command resyn is further applied to synthesize a circuit. The next three columns show the information of the test cases with different efforts as the pre-processing. The next six columns indicate the average number of nodes, levels, and support variables of the derived g function before and after applying the com-mand collapse to the derived g function. The last six columns are the results for h function. Note that functions g and h in different rows may not have the same functionalities. Although the test cases in different rows have the same functional-ities, they can have different circuit structures. The different circuit structures of the test cases result in different variable partitions as well as the functionality of derived functions g and h.
As can be seen, by ABC command collapse the size and level of the functions g and h are reduced. The same fact happens in the preprocessing step. One fact
4.5. Quality of Composite Functions
we can observe from the table is that, for function g without further optimized by collapse, the generated g in row “Dul” is smaller than the generated g in row
“DulClp”.
It is interesting that smaller test cases(with collapse) may not generate smaller composite functions. The reason why this happens is because the derivation of the interpolant function is directly based on the refutation proof of an UNSAT instance.
So for a given function with different circuit structures, the circuit with smaller size may not generate smaller refutation proof and so do the interpolant functions.
However the sizes of g and h after command collapse are greatly reduced to sizes comparable to original test cases.
Chapter 5
Conclusions and Future Work
In this thesis, we have proposed a SAT-based algorithm to handle single- and multiple-output Ashenhurst decompositions. Our proposed method can handle not only disjoint decomposition, but also non-disjoint decomposition in a natural way.
We formulated the problem into SAT solving; by using Craig interpolation and functional dependency, the decomposed sub-functions can be derived. Variable par-tition process can be automated and integrated into the algorithm by introducing the control variables for each input variable. To prevent trivial variable partition from happening, we enforced some seed partitions to achieve this goal. Furthermore, we enumerated different seed partitions to find a good variable partition which is more balanced and disjoint. In addition, the variable partition results can be further greatly improved by the proposed UNSAT core refinement process.
Chapter 5. Conclusions and Future Work
In our method, the formulation that solves the problem of single-output de-composition can be easily extended to deal with the multiple-output dede-composition problem. Also, in comparison with the prior BDD-based algorithms, the bound set variables of our method need not be small. Functions with hundreds of variables, which cannot be represented by BDD, can be handled by our SAT-based algorithm.
The scalability of our proposed method was justified by experimental results. The results showed that we can successfully decompose functions with up to 300 input variables. Because the experimental results showed that the method we proposed can handle large design instances, our approach may be applied at a top level of hierarchical decomposition in logic synthesis, which may provide a global view on optimization. For example, our algorithm may be used on chip-level decomposition to implement a large design instance using many FPGA cores. Also our algorithm can be a step forward towards topologically constrained logic synthesis.
For future work, how to effectively deal with general functional decomposition remains future investigation. The application of our approach to FPGA Boolean matching and multilevel hypergraph partitioning [13] are interesting subjects to study. In contrast to multilevel hypergraph partitioning, which focuses on structure-based manipulations, our Ashenhurst decomposition is a function-structure-based algorithm.
This is the major difference between the two subjects, although both of them can partition a circuit into two parts. Furthermore, for the characterization of don’t-care conditions, how to quickly identify all sub-matrices that have only one kind of column pattern, and how to use these don’t-care conditions to minimize the circuit
Chapter 5. Conclusions and Future Work
will be the future study.
Bibliography
[1] R. L. Ashenhurst. The decomposition of switching functions. Computation Lab, Harvard University, Vol. 29, pp.74-116, 1959.
[2] Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification. http://www.eecs.berkeley.edu/∼alanmi/abc/
[3] J. Cong and Y.-Y. Hwang. Boolean matching for LUT-based logic blocks with applications to architecture evaluation and technology mapping. IEEE Transac-tions on Computer-Aided Design of Integrated Circuits, 20(9):1077-1090, 2001.
[4] J. Cong and K. Minkovich. Improved SAT-based Boolean matching using im-plicants for LUT-based FPGAs. In Proc. ACM International Symposium on Field Programmable Gate Arrays, pp.139-147, 2007.
[5] S. A. Cook. The complexity of theorem proving procedures. Proc. Third Annual ACM Symposium on the Theory of Computing, pp.151-158, 1971.
[6] W. Craig. Linear reasoning: A new form of the Herbrand-Gentzen theorem. J.
Symbolic Logic, 22(3):250-268, 1957.
Bibliography
[7] H. A. Curtis. New Approach to the Design of Switching Circuits. Van Nostrand, Princeton, NJ, 1962.
[8] M. Davis and H. Putnam. A Computing Procedure for Quantification Theory.
Journal of the ACM, 7(3):201-215, 1960.
[9] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962.
[10] N. E´en and N. S¨oensson. An extensible SAT-solver. In Proc. International Con-ference on Theory and Applications of Satisfiability Testing, pp.502-518, 2003.
[11] J.-H. R. Jiang and R. K. Brayton. Functional dependency for verification re-duction. In Proc. International Conference on Computer Aided Verification, pp.268-280, 2004.
[12] J.-H. R. Jiang, J.-Y. Jou, and J.-D. Huang. Compatible class encoding in hyper-function decomposition for FPGA synthesis. In Proc. ACM/IEEE Design Au-tomation Conference, pp.712-717, 1998.
[13] G. Karypis, R. Aggarwal, V. Kumar, and S. Shekhar. Multilevel Hypergraph Partitioning: Application in VLSI Domain. In Proc. ACM/IEEE Design Au-tomation Conference, pp.526-529, 1997.
[14] R. M. Karp. Functional decomposition and switching circuit design. J. Soc.
Ind. Appl. Math. 11(2):291-335, 1963.
Bibliography
[15] Y.-T. Lai, M. Pedram, and S. B. K. Vrudhula. BDD based decomposition of logic functions with applications to FPGA synthesis. In Proc. ACM/IEEE De-sign Automation Conference, pp.642-647, 1993.
[16] C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. Scalable explo-ration of functional dependency by interpolation and incremental SAT solv-ing. In Proc. IEEE/ACM International Conference on Computer-Aided Design, pp.227-233, 2007.
[17] R.-R. Lee, J.-H. R. Jiang, and W.-L. Hung. Bi-decomposing large Boolean func-tions via interpolation and satisfiability solving. In Proc. ACM/IEEE Design Automation Conference, pp.636-641, 2008.
[18] H.-P. Lin, J.-H. R. Jiang, and R.-R. Lee. To SAT or Not to SAT: Ashenhurst Decomposition in a Large Scale. In Proc. IEEE/ACM International Conference on Computer-Aided Design, pp.32-37, 2008.
[19] A. C. Ling, D. P. Singh, and S. D. Brown. FPGA technology mapping: A study of optimality. In Proc. ACM/IEEE Design Automation Conference, pp.427-432, 2005.
[20] K. L. McMillan. Interpolation and SAT-based model checking. In Proc. Inter-national Conference on Computer Aided Verification, pp.1-13, 2003.
[21] P. Pudl´ak. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981-998, September 1997.
Bibliography
[22] J. P. Roth and R. M. Karp. Minimization over Boolean graphs. IBM Journal, pp.227-238, 1962.
[23] C. Scholl. Functional Decomposition with Applications to FPGA Synthesis.
Kluwer Academic Publishers, 2001.
[24] H. Sawada, T. Suyama, and A. Nagoya. Logic synthesis for look-up table based FPGAs using functional decomposition and support minimization. In Proc.
IEEE/ACM International Conference on Computer-Aided Design, pp.353-358, 1995.
[25] T. Stanion and C. Sechen. A Method for Finding Good Ashenhurst Decompo-sitions and Its Application to FPGA Synthesis. In Proc. ACM/IEEE Design Automation Conference, pp.60-64, 1995.
[26] S. Safarpour, A. G. Veneris, G. Baeckler, and R. Yuan. Efficient SAT-based Boolean matching for FPGA technology mapping. In Proc. ACM/IEEE Design Automation Conference, pp.466-471, 2006.
[27] G. S. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pp.466-483, 1970.
[28] K.-H. Wang and C.-M. Chan. Incremental learning approach and SAT model for Boolean matching with don’t cares. In Proc. IEEE/ACM International Con-ference on Computer-Aided Design, pp.234-239, 2007.
Bibliography
[29] B. Wurth, K. Eckl, and K. Antreich. Functional Multiple-Output Decomposi-tion: Theory and an Implicit Algorithm. In Proc. ACM/IEEE Design Automa-tion Conference, pp.54-59, 1995.
[30] B. Wurth, U. Schlichtmann, K. Eckl, and K. Antreich. Functional multiple-output decomposition with application to technology mapping for lookup table-based FPGAs. ACM Trans. on Design Automation of Electronic Systems, 4(3):313-350, 1999.