Advertisement

Numeric Types in Formal Synthesis

  • Viktor Sabelfeld
  • Kai Kapp
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

Abstract

The Formal Synthesis methodology can be considered as the application of the transformational approach to circuit synthesis by logical transformations performed in a theorem prover. Additionally to the implementation of the circuit, the proof that the result is a correct implementation of a given specification is obtained automatically. In this paper, a higher-order formalisation for the arithmetic of bound numeric data types is given. We provide correct transformations implemented in the theorem prover HOL [4], to register-transfer level descriptions of arithmetic operations. For a restricted class of specifications, a correct transformation is described which eliminates the type num and replaces arithmetic operations by its bound variants.

Keywords

formal specification correct hardware synthesis higher-order logic theorem prover arithmetic operations 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Blumenræhr, C., Eisenbiegler, D.: Performing High-Level Synthesis via Program Transformations within a Theorem Prover. In: Digital System Design Workshop at the 24th EUROMICRO 1998 Conference (1998)Google Scholar
  2. 2.
    Blumenræhr, C., Sabelfeld, V.: Formal Synthesis at the Algorithmic Level. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 187–202. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Eisenbiegler, D.: Ein Kalkül für die Formale Schaltungssynthese, Karlsruhe University Dissertation. Logos Verlag, Berlin, p. 150 (1999) (in German)Google Scholar
  4. 4.
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  5. 5.
    Hennessy, J.L., Patterson, D.A.: Computer Architecture — a Quantitative Approach, 2nd edn (1996)Google Scholar
  6. 6.
    Iyoda, J., Sampaio, A., Silva, L.: ParTS: A Partitioning Transformation System. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1400–1419. Springer, Heidelberg (1999)Google Scholar
  7. 7.
    Larsson, M.: An engineering approach to formal digital system design. The Computer Journal 38(2), 101–110 (1995)CrossRefMathSciNetGoogle Scholar
  8. 8.
    O’Leary, J., Zhao, X., Gerth, R., Seger, C.H.: Formally Verifying IEEE Compliance of Floating-Point Hardware. Intel Technology Journal, 14 (1999), http://www.intel.com/technology/itj/q11999/articles/art_5.htm
  9. 9.
    Melham, T.F.: Automating Recursive Type Definitions in Higher Order Logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 341–386. Springer, Heidelberg (1989)Google Scholar
  10. 10.
    Sabelfeld, V., Blumenræhr, C., Kapp, K.: Semantics and Transformations in Formal Synthesis at System Level. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 149–156. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Sharp, R., Rasmussen, O.: The T-Ruby design system. In: IFIP Conference on Hardware Description Languages and their Applications, pp. 587–596 (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Viktor Sabelfeld
    • 1
  • Kai Kapp
    • 1
  1. 1.Institute for Computer Design and Fault Tolerance (Prof. Dr.-Ing. D. Schmid)University of KarlsruheGermany

Personalised recommendations