Top

Published in:

2017 | OriginalPaper | Chapter

Matching Multiplications in Bit-Vector Formulas

Authors : Supratik Chakraborty, Ashutosh Gupta, Rahul Jain

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true when multiplication operators are decomposed and represented in alternative ways in the formula. We present a pre-processing heuristic that identifies certain types of decomposed multipliers, and adds special assertions to the input formula that encode the equivalence of sub-terms and word-level multiplication terms. The pre-processed formulas are then solved using an SMT solver. Our experiments with three SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Structuring Abstract Interpreters Through State and Value Abstractions

next chapter Independence Abstractions and Models of Concurrency

https://github.com/rahuljain1989/Bit-vector-multiplication-pattern.

Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of DAC 2003, pp. 368–371. ACM Press (2003)

Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Berlin (2009). doi:10.1007/978-3-642-00768-2_16 CrossRef

EBMC. http://www.cprover.org/ebmc/

Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Berlin (2004). doi:10.1007/978-3-540-24730-2_15 CrossRef

Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_32 CrossRef

Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). doi:10.1007/11804192_17 CrossRef

Naveh, Y., Emek, R.: Random stimuli generation for functional hardware verification as a CP application. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, p. 882. Springer, Heidelberg (2005). doi:10.1007/11564751_120 CrossRef

Naveh, Y., Rimon, M., Jaeger, I., Katz, Y., Vinov, M., Marcus, E., Shurek, G.: Constraint-based random stimuli generation for hardware verification. In: Proceedings of AAAI, pp. 1720–1727 (2006)

Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, 12–15 June 2005, pp. 213–223 (2005)

10.

Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, Lisbon, Portugal, 5–9 September 2005, pp. 263–272 (2005)

11.

Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885 (2009)

12.

Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15–44. Springer, Berlin (2013). doi:10.1007/978-3-642-36675-8_2 CrossRef

13.

Chakraborty, S., Khasidashvili, Z., Seger, C.-J.H., Gajavelly, R., Haldankar, T., Chhatani, D., Mistry, R.: Word-level symbolic trajectory evaluation. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 128–143. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21668-3_8 CrossRef

14.

Long multiplication. https://en.wikipedia.org/wiki/Multiplication_algorithm#Long_multiplication

15.

Booth’s multiplication algorithm. https://en.wikipedia.org/wiki/Booth’s_multiplication_algorithm

16.

Wallace, C.S.: A suggestion for a fast multiplier. IEEE Trans. Electron. Comput. 13(1), 14–17 (1964)CrossRefMATH

17.

Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 CrossRef

18.

Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14 CrossRef

19.

Stoffel, D., Kunz, W.: Equivalence checking of arithmetic circuits on the arithmetic bit level. IEEE Trans. CAD Integr. Circuits Syst. 23(5), 586–597 (2004)CrossRef

20.

Yu, C., Ciesielski, M.J.: Automatic word-level abstraction of datapath. In: IEEE International Symposium on Circuits and Systems, ISCAS 2016, Montréal, QC, Canada, 22–25 May 2016, pp. 1718–1721 (2016)

21.

Kölbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: Design, Automation and Test in Europe, DATE 2009, Nice, France, 20–24 April 2009, pp. 196–201 (2009)

22.

Subramanyan, P., Tsiskaridze, N., Pasricha, K., Reisman, D., Susnea, A., Malik, S.: Reverse engineering digital circuits using functional analysis. In: Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18–22, 2013, pp. 1277–1280 (2013)

23.

Li, W., Gascón, A., Subramanyan, P., Tan, W.Y., Tiwari, A., Malik, S., Shankar, N., Seshia, S.A.: Wordrev: Finding word-level structures in a sea of bit-level gates. In: 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2013, Austin, TX, USA, 2–3 June 2013, pp. 67–74 (2013)

24.

Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008)MATH

25.

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org

26.

Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRef

27.

Bayardo, R.J., Jr., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 1997, IAAI 1997, 27–31 July 1997, Providence, Rhode Island, pp. 203–208 (1997)

28.

Chakraborty, S., Gupta, A., Jain, R.: Matching multiplications in bit-vector formulas. https://arxiv.org/abs/1611.10146

29.

Bryant, R.E., Chen, Y.-A.: Verification of arithmetic circuits with binary moment diagrams. In: DAC, pp. 535–541 (1995)

30.

Sayed-Ahmed, A., Große, D., Kühne, U., Soeken, M., Drechsler, R.: Formal verification of integer multipliers by combining gröbner basis with logic reduction. In: 2016 Design, Automation & Test in Europe Conference & Exhibition, DATE 2016, Dresden, Germany, 14–18 March 2016, pp. 1048–1053 (2016)

31.

HECTOR. http://www.synopsys.com/Tools/Verification/FunctionalVerification/Pages/hector.aspx

Title: Matching Multiplications in Bit-Vector Formulas
Authors: Supratik Chakraborty
Ashutosh Gupta
Rahul Jain
Publisher: Springer International Publishing
Book: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-52234-0_8

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner