Advertisement

On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system

  • Naren Narasimhan
  • Ranga Vemuri
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

This paper presents a formal specification and a proof of correctness for the register optimization task in high-level synthesis. A widely implemented register optimization algorithm is modeled in higher-order logic and verified in a theorem prover environment. A rich collection of correctness properties is systematically formulated during the theorem proving exercise. These properties constitute a detailed set of formal assertions that are identified with the invariants at various stages of the algorithm. The formal assertions are then embedded as programming assertions in the implementation of the register optimization algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the high-level synthesis system produced designs with error-free register allocation and, (2) in the event of a failure, help discover and isolate programming errors in the implementation.

We present a detailed example and supporting experimental data to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in discovering a useful set of assertions for embedding in the register optimization implementation and argue that in the absence of using the mechanical proof checking effort it would have been very hard if not impossible to discover a set of assertions so useful and expressed with such precision.

Keywords

Theorem Prove Register Optimization Formal Verification Register Allocation Prototype Verification System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    C.-J Tseng and D. P. Siewiorek. Automated Synthesis of Data Paths in Digital Systems. In IEEE Transactions on CAD, July 1986.Google Scholar
  2. 2.
    D. Eisenbiegler, C. Blumenrohr, and R. Kumar. Implementation Issues about the Embedding of Existing High Level Synthesis Algorithms in HOL. In TPHOL. Springer, 1996.Google Scholar
  3. 3.
    D. Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
  4. 4.
    D. D. Gajski, N. D. Dutt, A. C. Wu and S. Y. Lin. High-level Synthesis, Introduction to Chip and System Design. Kluwer Academic Publishers, 1992.Google Scholar
  5. 5.
    D. L. Springer and D. E. Thomas. Exploiting the Special Structure of Conflict and Compatibility Graphs in High-Level Synthesis. In Proceedings of ICCAD, pages 254–157, 1990.Google Scholar
  6. 6.
    E. M. Mayger and M. P. Fourman. Integration of Formal Methods with System Design. In A. Halaax and P. B. Denyer, editor, International Conference on VLSI, pages 59–70. IFIP Transactions, August 1991.Google Scholar
  7. 7.
    D. E. Thomas et al. Algorithmic and Register Transfer Level Synthesis: The System Architect's Workbench. Kluwer Academic Publishers, 1990.Google Scholar
  8. 8.
    F. K. Hanna, M. Longley and N. Daeche. Formal Synthesis of Digital Systems. In Workshop on Applied Formal Methods for Correct VLSI Design, pages 532–548. IMEC-IFIP, Elsevier Science Publishers B.V., 1989.Google Scholar
  9. 9.
    M. C. Golumbic. Algorithmic Graph Theory and Perfect Graphs. Academic Press, 1980.Google Scholar
  10. 10.
    J. Roy, N. Kumar, R. Dutta and R. Vemuri. DSS: A Distributed High-Level Synthesis System. In IEEE Design and Test of Computers, June 1992.Google Scholar
  11. 11.
    M. Gordon and T. Melham, editor. Introduction to HOL. Cambridge Univ. Press, Cambridge, England, 1993.Google Scholar
  12. 12.
    M. Larsson. An Engineering Approach to Formal System Design. In Thomas F. Melham and Juanito Camilleri, editor, Higher Order Logic Theorem Proving and its Applications, pages 300–315. Springer, September 1994.Google Scholar
  13. 13.
    M. R. Garey and D. S. Johnson. Computers and Intractability. W. H. Freeman and Company, New York, 1979.Google Scholar
  14. 14.
    N. Narasimhan and R. Vemuri. Synchronous Controller Models for Synthesis from Communicating VHDL Processes. In Ninth International Conference on VLSI Design, pages 198–204, Bangalore, India, January 1996.Google Scholar
  15. 15.
    N. Narasimhan, R. Kalyanaraman, and R. Vemuri. Validation of Synthesized Register-Transfer Level Designs Using Simulation and Formal Verification. In High Level Design Validation and Test Workshop, November 1996.Google Scholar
  16. 16.
    R. Camposano and W. Wolf. High-Level VLSI Synthesis. Kluwer Academic Publishers, 1991.Google Scholar
  17. 17.
    R. Vemuri et al. Experiences in Functional Validation of a High Level Synthesis System. In 30th ACM/IEEE Design Automation Conference, pages 194–201, 1993.Google Scholar
  18. 18.
    S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607, pages 748–752. Springer-Verlag, June 1992.Google Scholar
  19. 19.
    S. D. Johnson. Synthesis of Digital Designs from Recursion Equations. MIT, 1984.Google Scholar
  20. 20.
    S. D. Johnson, R. M. Wehrmeister and Bhaskar Bose. On the Interplay of Synthesis and Verification. In Workshop on Applied Formal Methods for Correct VLSI Design, pages 385–404. IMEC-IFIP, Elsevier Science Publishers B.V., 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Naren Narasimhan
    • 1
  • Ranga Vemuri
    • 1
  1. 1.Laboratory for Digital Design Environments Department of ECECSUniversity of CincinnatiCincinnatiUSA

Personalised recommendations