Skip to main content
Top
Published in:
Cover of the book

2011 | OriginalPaper | Chapter

1. Introduction

Authors : Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta

Published in: High-Level Verification

Publisher: Springer New York

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

search-config
loading …

Abstract

The quantitative changes brought about by Moore’s law in design of integrated circuits (ICs) affect not only the scale of the designs, but also the scale of the process to design and validate such chips. While designer productivity has grown at an impressive rate over the past few decades, the rate of improvement has not kept pace with chip capacity growth leading to the well known design-productivity-gap [105]. The problem of reducing the design-productivity-gap is crucial in not only handling the complexity of the design, but also combating the increased fragility of the composed system consisting of heterogeneous components. Unlike software programs, integrated circuits are not repairable. The development costs are so high that multiple design spins are ruled out, a design must be correct in the one and often the only one design iteration to implementation.

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!

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!

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!

Literature
23.
go back to reference Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1–33. IEEE Computer Society Press, Washington, D.C. (1990). URL citeseer.ist.psu.edu/burch90symbolic.html Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1–33. IEEE Computer Society Press, Washington, D.C. (1990). URL citeseer.​ist.​psu.​edu/​burch90symbolic.​html
29.
61.
go back to reference 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 (1992) 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 (1992)
75.
go back to reference Gordon, M.: HOL: A proof generating system for higher-order logic. In: G. Birtwistle, P. Subrahmanyam (eds.) VLSI Specification Verification and Synthesis, pp. 73–128. Kluwer Academic Publishers (1988) Gordon, M.: HOL: A proof generating system for higher-order logic. In: G. Birtwistle, P. Subrahmanyam (eds.) VLSI Specification Verification and Synthesis, pp. 73–128. Kluwer Academic Publishers (1988)
82.
go back to reference Gupta, R., Brewer, F.: High-Level Synthesis: A Retrospective. In: High-Level Synthesis from Algorithm to Digital Circuit. Springer (2008) Gupta, R., Brewer, F.: High-Level Synthesis: A Retrospective. In: High-Level Synthesis from Algorithm to Digital Circuit. Springer (2008)
120.
go back to reference Kundu, S., Tatlock, Z., Lerner, S.: Proving Optimizations Correct using Parameterized Program Equivalence. In: PLDI ’09: Proceedings of the 2009 ACM SIGPLAN conference on Programming Language Design and Implementation (2009) Kundu, S., Tatlock, Z., Lerner, S.: Proving Optimizations Correct using Parameterized Program Equivalence. In: PLDI ’09: Proceedings of the 2009 ACM SIGPLAN conference on Programming Language Design and Implementation (2009)
142.
go back to reference McFarland, M.C.: Formal verification of sequential hardware: A tutorial. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 12(5), 654–663 (1993)CrossRef McFarland, M.C.: Formal verification of sequential hardware: A tutorial. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 12(5), 654–663 (1993)CrossRef
147.
go back to reference Micheli, G.D.: Guest editorial: High-level synthesis of digital circuits. IEEE Transactions on Design Test 7(5), 6–7 (1990) Micheli, G.D.: Guest editorial: High-level synthesis of digital circuits. IEEE Transactions on Design Test 7(5), 6–7 (1990)
148.
go back to reference Micheli, G.D.: Synthesis and Optimization of Digital Circuits. McGraw-Hill (1994) Micheli, G.D.: Synthesis and Optimization of Digital Circuits. McGraw-Hill (1994)
164.
go back to reference Owre, S., Rushby, J.M.,, Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) Proceedings of 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer-Verlag, Saratoga, NY (1992). DOI http://www.csl.sri.com/papers/cade92-pvs/ Owre, S., Rushby, J.M.,, Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) Proceedings of 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer-Verlag, Saratoga, NY (1992). DOI http://​www.​csl.​sri.​com/​papers/​cade92-pvs/​
165.
go back to reference Paulson, L.C.: Isabelle: A generic theorem prover, Lecure Notes in Computer Science, vol. 828. Springer Verlag (1994) Paulson, L.C.: Isabelle: A generic theorem prover, Lecure Notes in Computer Science, vol. 828. Springer Verlag (1994)
174.
go back to reference Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: CAV ’05: Proceedings of the 17th international conference on Computer Aided Verification, pp. 82–97 (2005) Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: CAV ’05: Proceedings of the 17th international conference on Computer Aided Verification, pp. 82–97 (2005)
201.
go back to reference Vardi, M.Y.: Formal techniques for SystemC verification. In: DAC ’07: Proceedings of the 44th annual conference on Design Automation (2007) Vardi, M.Y.: Formal techniques for SystemC verification. In: DAC ’07: Proceedings of the 44th annual conference on Design Automation (2007)
203.
go back to reference Walker, R., Camposano, R.: A Survey of High-Level Synthesis Systems. Kluwer Academic Publishers, Boston, MA, USA (1991)MATH Walker, R., Camposano, R.: A Survey of High-Level Synthesis Systems. Kluwer Academic Publishers, Boston, MA, USA (1991)MATH
205.
go back to reference Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: TACAS ’08: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 382–396 (2008) Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: TACAS ’08: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 382–396 (2008)
Metadata
Title
Introduction
Authors
Sudipta Kundu
Sorin Lerner
Rajesh K. Gupta
Copyright Year
2011
Publisher
Springer New York
DOI
https://doi.org/10.1007/978-1-4419-9359-5_1