Abstract
SystemC is a new C-based system level design language whose ultimate objective is to enable System-on-a-Chip (SoC) design and verification. Fixed-point design based on the SystemC data types is rapidly becoming the standard for optimizing DSP systems. In this paper, we propose to create a formalization of SystemC fixed-point arithmetic in the HOL theorem proving environment. The SystemC fixed-point number representation which contains a new generalized format and different rounding and overflow modes is described, and then it is formalized in higher-order logic. This formalization is then compared with the formalization of IEEE standard based floating-point arithmetic in HOL. A set of theorems are proved to bound the error in fixed-point rounding and to verify the fixed-point arithmetic operations against their abstract mathematical counterparts. Finally, we show by an example how this formalization can be used in verification of the translation from floating-point and fixed-point algorithmic, down to register transfer and netlist gate levels in the design flow of SoC systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aagaard, M.D., Seger, C.-J.H.: The Formal Verification of a Pipelined Double- Precision IEEE Floating-Point Multiplier. In: International Conference on Computer Aided Design, San Francisco, CA, USA, November 1995, pp. 7–10 (1995)
Akbarpour, B., Tahar, S., Dekdouk, A.: Formalization of Cadence SPW Fixed- Point Arithmetic in HOL. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 185–204. Springer, Heidelberg (2002)
Barrett, G.: Formal Methods Applied to a Floating Point Number System. IEEE Transactions on Software Engineering SE-15(5), 611–621 (1989)
Berg, C., Jacobi, C.: Formal Verification of the VAMP Floating Point Unit. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 325–339. Springer, Heidelberg (2001)
Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van-Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Theorem Provers in Circuit Design, pp. 129–156. North-Holland, Amsterdam (1992)
Carreno, V.A.: Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System. NASA Technical Memorandum 110189 (September 1995)
Chang, H., et al.: Surviving the SoC Revolution. A Guide to Platform-Based Design. Kluwer Academic Publishers, Boston (1999)
Cornea-Hasegan, M.: Proving the IEEE Correctness of Iterative Floating-Point Square Root, Divide, and Remainder Algorithms. Intel Technology Journal Q2, 1–11 (1998)
Chen, Y.-A., Bryant, R.E.: Verification of Floating Point Adders. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 488–499. Springer, Heidelberg (1998)
Daumas, M., Rideau, L., Thry, L.: A Generic Library for Floating-Point Numbers and its Application to Exact Computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 169–184. Springer, Heidelberg (2001)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Harrison, J.R.: Theorem Proving with the Real Numbers. Technical Report 408, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK (December 1996)
Harrison, J.R.: Floating-Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design 16(3), 271–305 (2000)
Harrison, J.R.: A Machine-Checked Theory of Floating-Point Arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)
IEEE, Standard for Binary Floating-Point Arithmetic, ANSI/IEEE Standard 754- 1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)
IEEE, Standard for Radix-Independent Floating-Point Arithmetic, ANSI/IEEE Std 854-1987, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1987)
Inacio, C., Ombres, D.: The DSP Decision: Fixed Point or Floating? IEEE Spectrum, 0018-9234 (September 1996)
Intel Inc., Pentium Processors, Statistical Analysis of Floating-Point Flaw, Intel White Paper, Sec. 3 (November 1994)
Kern, C., Greenstreet, M.: Formal Verification in Hardware Design: A Survey. ACM Transactions on Design Automation of Electronic Systems 4, 123–193 (1999)
Leeser, M., O’Leary, J.: Verification of a Subtractive Radix-2 Square Root Algorithm and Implementation. In: International Conference on Computer Design, Cambridge, MA, USA, October 1995, pp. 526–531 (1995)
O Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally Verifying IEEE Compliance of Floating-Point Hardware. Intel Technology Journal Q1, 1–14 (1999)
Melham, T.F.: The HOL pred sets Library. University of Cambridge, Computer Laboratory (February 1992)
Melham, T.: Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science 31. Cambridge University Press (1993)
Miner, P.S., Leathrum, J.F.: Verification of IEEE Compliant Subtractive Division Algorithms. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 64–78. Springer, Heidelberg (1996)
Miner, P.S.: Defining the IEEE-854 Floating-Point Standard in PVS. Technical Memorandum 110167, NASA, Langley Research Center, Hampton, VA 236810001, USA (June 1995)
Moore, J.S., Lynch, T., Kaufmann, M.: A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm. IEEE Transactions on Computers 47, 913–926 (1998)
Mueller, S.M., Paul, W.J.: Computer Architecture. Complexity and Correctness. Springer, Heidelberg (2000)
Russinoff, D.M.: A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating-Point Adder of the AMD Athlon Processor. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 3–36. Springer, Heidelberg (2000)
Signal Processing WorkSystem (SPW) User’s Guide, Cadence Design Systems, Inc. (July 1999)
Swan, S.: An Introduction to System Level Modeling in SystemC 2.0, Cadence Design Systems, Inc. (May 2001)
CoCentric TM System Studio User’s Guide, Synopsys, Inc., USA (August 2001)
CoCentric Fixed-Point Designer User’s Guide, Synopsys, Inc., USA (August 2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Akbarpour, B., Tahar, S. (2003). Modeling SystemC Fixed-Point Arithmetic in HOL. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-39893-6_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20461-9
Online ISBN: 978-3-540-39893-6
eBook Packages: Springer Book Archive