Abstract
We consider the problem of test generation for Boolean combinational circuits. We use a novel approach based on the idea of treating tests as a proof encoding rather than as a sample of the search space. In our approach, a set of tests is complete for a circuit N, and a property p, if it “encodes” a formal proof that N satisfies p. For a combinational circuit of k inputs, the cardinality of such a complete set of tests may be exponentially smaller than 2k. In particular, if there is a short resolution proof, then a small complete set of tests also exists. We show how to use the idea of treating tests as a proof encoding to directly generate high-quality tests. We do this by generating tests that encode mandatory fragments of any resolution proof. Preliminary experimental results show the promise of our approach.
This research was funded in part by NASA Cooperative Agreement NNX08AE37A.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramovici, M., Breuer, M., Friedman, D.: Digital Systems Testing and Testable Design. John Wiley & Sons, Chichester (1994)
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch.2, pp. 19–99. North-Holland, Amsterdam (2001)
Budd, T.A., DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Theoretical and empirical studies on using program mutation to test the functional correctness of programs. In: 7th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, Las Vegas, Nevada, pp. 220–233 (1980)
Engel, C., Hähnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169–188. Springer, Heidelberg (2007)
Goldberg, E.: Boundary points and resolution. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 147–160. Springer, Heidelberg (2009)
Goldberg, E.: On bridging simulation and formal verification. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 127–141. Springer, Heidelberg (2008)
Marques-Silva, J., Sakallah, K.: Grasp - a new search algorithm for satisfiability. In: International conference on computer-aided design, Washington, DC, USA, pp. 220–227 (1996)
Satpathy, M., Butler, M.J., Leuschel, M., Ramesh, S.: Automatic testing from formal specifications. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 95–113. Springer, Heidelberg (2007)
Tseitin, G.S.: On the complexity of derivation in the propositional calculus. In: Zapiski nauchnykh seminarov LOMI, vol. 8, pp. 234–259 (1968)
Alloy system, http://alloy.mit.edu/community
CProver, http://www.cprover.org/cbmc
JavaPathfinder, http://babelfish.arc.nasa.gov/trac/jpf
SAT 2009 competition, http://www.satcompetition.org/2009
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goldberg, E., Manolios, P. (2010). Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding. In: Fraser, G., Gargantini, A. (eds) Tests and Proofs. TAP 2010. Lecture Notes in Computer Science, vol 6143. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13977-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-13977-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13976-5
Online ISBN: 978-3-642-13977-2
eBook Packages: Computer ScienceComputer Science (R0)