nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

A Correct-by-Decision Solution for Simultaneous Place and Route

verfasst von : Alexander Nadel

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

To reduce a problem, provided in a human language, to constraint solving, one normally maps it to a set of constraints, written in the language of a suitable logic. This paper highlights a different paradigm, in which the original problem is converted into a set of constraints and a decision strategy, where the decision strategy is essential for guaranteeing the correctness of the modeling. We name such a paradigm Correct-by-Decision. Furthermore, we propose a Correct-by-Decision-based solution within a SAT solving framework for a critical industrial problem that shows up in the physical design stage of the CAD process: simultaneous place and route under arbitrary constraints (design rules). We demonstrate the usefulness of our approach experimentally on industrial and crafted instances.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT

Nächstes Kapitel Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification

Neighbor constraints are cardinality constraints, which can easily be translated to CNF (see [5] for a review).

Let \(r_i\) be a potential root of a device \(D_i\) that is about to be placed by the decision strategy. The engagement variable \(e(r_i)\) can already be assigned 1 at this point if Boolean Constraint Propagation (BCP) has been able to conclude that \(r_i\) is the only potential root of \(D_i\) where the device can be placed.

The center is the vertex \((R_x/2,R_y/2)\), if available, or, otherwise, the vertex whose Manhattan distance from \((R_x/2,R_y/2)\) is as small as possible.

Abboud, N., Grötschel, M., Koch, T.: Mathematical methods for physical layout of printed circuit boards: an overview. OR Spectr. 30(3), 453–468 (2008)MathSciNetCrossRefMATH

Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_23 CrossRef

Barrett, C., Donham, J.: Combining SAT methods with non-clausal decision heuristics. Electr. Notes Theor. Comput. Sci. 125(3), 3–12 (2005)CrossRefMATH

Bayless, S., Bayless, N., Hoos, H.H., Hu, A.J.: SAT modulo monotonic theories. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 25–30 January 2015, Austin, Texas, USA, pp. 3702–3709. AAAI Press, New York (2015)

Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) [20], pp. 285–301

Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. JSAT 6(1–3), 165–201 (2009)MathSciNetMATH

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_37 CrossRef

Erez, A., Nadel, A.: Finding bounded path in graph using SMT for automatic clock routing. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 20–36. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_2 CrossRef

Hadarean, L.: An efficient and trustworthy theory solver for bit-vectors in satisfiability modulo theories. Dissertation, New York University (2015)

10.

Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 66–79. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34188-5_9 CrossRef

11.

Nadel, A.: A correct-by-decision solution for simultaneous place and route: benchmarks and detailed results. https://goo.gl/MNl1PE

12.

Nadel, A.: Routing under constraints. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3–6 October 2016, pp. 125–132. IEEE, Washington, D.C. (2016)

13.

Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242–255. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_19 CrossRef

14.

Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) [20], pp. 206–218

15.

Nag, S., Rutenbar, R.A.: Performance-driven simultaneous place and route for row-based FPGAs. In: DAC, pp. 301–307 (1994)

16.

Nag, S.K., Rutenbar, R.A.: Performance-driven simultaneous place and route for island-style FPGAs. In: Rudell, R.L., (eds.) Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, 5–9 November 1995, pp. 332–338. IEEE Computer Society/ACM, Washington, D.C. (1995)

17.

Ramalingam, G., Reps, T.W.: An incremental algorithm for a generalization of the shortest-path problem. J. Algorithms 21(2), 267–305 (1996)MathSciNetCrossRefMATH

18.

Sabharwal, A.: Symchaff: a structure-aware satisfiability solver. In: Veloso, M.M., Kambhampati, S. (eds.) Proceedings of the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, 9–13 July 2005, Pittsburgh, Pennsylvania, USA, pp. 467–474. AAAI Press/The MIT Press, Austin (2005)

19.

Sherwani, N.A.: Algorithms for VLSI Physical Design Automation, 3rd edn. Kluwer, Dordrecht (1998)MATH

20.

Sinz, C., Egly, U. (eds.): SAT 2014. LNCS, vol. 8561. Springer, Cham (2014)MATH

Titel: A Correct-by-Decision Solution for Simultaneous Place and Route
verfasst von: Alexander Nadel
Verlag: Springer International Publishing
Buch: Computer Aided Verification
Print ISBN: 978-3-319-63389-3

Electronic ISBN: 978-3-319-63390-9

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-63390-9_23

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner