Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Flexible Composite Galois Field Multiplier Designs Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Translation Validation of Loop Invariant Code Optimizations Involving False Computations

verfasst von : Ramanuj Chouksey, Chandan Karfa, Purandar Bhaduri

Erschienen in: VLSI Design and Test

Verlag: Springer Singapore

Einloggen

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

search-config
loading …

Abstract

Code motion based optimizations are used quite often in electronic design automation (EDA) tools to improve the quality of synthesis results. Ensuring the correctness of such transformation is necessary for reliability of EDA tools. A value propagation (VP) based equivalence checking method of finite state machine with datapaths (FSMD) was proposed in [1] to specifically verify code motion across loops. In this work, we identify some scenarios involving loop invariant code motion where the VP based equivalence checking method fails to establish the equivalence between two actually equivalent FSMDs. We propose an enhancement over the VP based equivalence checking method [1] to overcome this limitation. Experimental results demonstrate that our method can handle the scenario where the VP based equivalence checking method fails.

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 Formal Perspective on Effective Post-silicon Debug and Trace Signal Selection
Nächstes Kapitel A Framework for Automated Feature Based Mixed-Signal Equivalence Checking
Literatur
1.
Banerjee, K., Karfa, C., Sarkar, D., Mandal, C.A.: Verification of code motion techniques using value propagation. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 33(8), 1180–1193 (2014)CrossRef
2.
Camposano, R.: Path-based scheduling for synthesis. IEEE Trans. CAD Integr. Circ. Syst. 10(1), 85–93 (1991)CrossRef
3.
4.
5.
Gajski, D.D., Dutt, N.D., Wu, A.C.H., Lin, S.Y.L.: High-level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, Norwell (1992)CrossRef
6.
Gupta, S., Savoiu, N., Dutt, N.D., Gupta, R.K., Nicolau, A.: Using global code motions to improve the quality of results for high-level synthesis. IEEE Trans. CAD Integr. Circ. Syst. 23(2), 302–312 (2004)CrossRef
7.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefMATH
8.
Karfa, C., Mandal, C.A., Sarkar, D.: Formal verification of code motion techniques using data-flow-driven equivalence checking. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 17(3), 30 (2012)
9.
Karfa, C., Sarkar, D., Mandal, C., Kumar, P.: An equivalence-checking method for scheduling verification in high-level synthesis. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 27(3), 556–569 (2008)CrossRef
10.
Knoop, J., Rüthing, O., Steffen, B.: Lazy code motion. In: Proceedings of the ACM SIGPLAN 1992 Conference on Programming Language Design and Implementation, PLDI 1992, pp. 224–234. ACM, New York (1992)
11.
12.
Kundu, S., Lerner, S., Gupta, R.K.: Translation validation of high-level synthesis. IEEE Trans. CAD Integr. Circ. Syst. 29(4), 566–579 (2010)CrossRef
13.
Lee, C., Shih, C., Huang, J., Jou, J.: Equivalence checking of scheduling with speculative code transformations in high-level synthesis. In: Proceedings of the 16th Asia South Pacific Design Automation Conference, ASP-DAC 2011, PLDI 1992, pp. 497–502. IEEE, Yokohama (2011)
14.
Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst. (TOPLAS) 1(1), 121–141 (1979)CrossRefMATH
15.
Lowry, E.S., Medlock, C.W.: Object code optimization. Commun. ACM 12(1), 13–22 (1969)CrossRef
16.
Rahmouni, M., Jerraya, A.A.: Formulation and evaluation of scheduling techniques for control flow graphs. In: Proceedings of EURO-DAC, European Design Automation Conference, EURO-DAC 1995, pp. 386–391. IEEE, England (1995)
17.
Rüthing, O., Knoop, J., Steffen, B.: Sparse code motion. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2000, pp. 170–183. ACM, New York (2000)
18.
Metadaten
Titel
Translation Validation of Loop Invariant Code Optimizations Involving False Computations
verfasst von
Ramanuj Chouksey
Chandan Karfa
Purandar Bhaduri
Copyright-Jahr
2017
Verlag
Springer Singapore
Buch
VLSI Design and Test

Print ISBN: 978-981-10-7469-1

Electronic ISBN: 978-981-10-7470-7

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-981-10-7470-7_72

Neuer Inhalt

    Bildnachweise