Abstract
Here we first introduce Quantified Boolean Formula (QBF) based approaches to logic synthesis and testing in general including automatic corrections of designs. It is formulated as: If some appropriate values are assigned to what we call programmable variables, the resulting circuits behaves as our intentions for all possible input values, that is, they become the ones whose logic functions are the intended ones. In this paper we only target combinational circuits and sequential circuits which are time-frame expanded by fixed times. The QBF problems are solved by repeatedly applying SAT solvers, not QBF solvers, with incremental additions of new constraints for each iteration which come from counter examples for the SAT problems. The required numbers of iterations until solutions are obtained are experimentally shown to be pretty small (in the order of tens) even if there are hundreds of inputs, regardless of the fact that they have exponentially many value combinations. Then the applications of the proposed methodology to logic synthesis, logic debugging, and automatic test pattern generations (ATPG) for multiple faults are discussed with experimental results. In the case of ATPG, a test pattern is generated for each iteration, and programmable variables can represent complete sets of functional and multiple faults, which are the most general faults models.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Mangassarian, H., Yoshida, H., Veneris, A.G., Yamashita, S., Fujita, M.: On error tolerance and engineering change with partially programmable circuits. In: The 17th Asia and South Pacific Design Automation Conference (ASP-DAC 2012), pp. 695–700 (2012)
Jo, S., Matsumoto, T., Fujita, M.: SAT-based automatic rectification and debugging of combinational circuits with LUT insertions. In: Asian Test Symposium (ATS), pp. 19–24, November 2012
Fujita, M., Jo, S., Ono, S., Matsumoto, T.: Partial synthesis through sampling with and without specification. In: International Conference on Computer Aided Design (ICCAD), pp. 787–794, November 2013
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_10
Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_5
Ling, A., Singh, D.P., Brown, S.D.: FPGA logic synthesis using quantified boolean satisfiability. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 444–450. Springer, Heidelberg (2005). doi:10.1007/11499107_37
Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS 2006, pp. 404–415 (2006)
Jain, J., Mukherjee, R., Fujita, M.: Advanced verification techniques based on learning. In: The 32nd Annual ACM/IEEE Design Automation Conference, pp. 420–426 (1995)
Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230–244. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21581-0_19
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Fujita, M. (2016). Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-46520-3_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46519-7
Online ISBN: 978-3-319-46520-3
eBook Packages: Computer ScienceComputer Science (R0)