A memory-efficient canonical data structure for decimal floating point arithmetic systems modeling and verification

Decimal floating point (DFP) number representation was proposed in IEEE-754-2008 in order to overcome binary floating point inaccuracy. Neglecting binary floating point verification has resulted in significant validity and economic losses. Formal verification can be a solution to similar DFP design problems. Verification techniques aiming at DFP are limited to functional methods whereas formal approaches have been neglected and traditional decision diagrams cannot model DFP representation complexity. In this paper, we propose an efficient canonical data structure that can model DFP properties. Our novel data structure models coefficient, exponent, sign, and bias of a DFP number. We will prove mathematically that our data structure is canonical. We will also show that the size of the proposed data structure will grow linearly for a DFP number for all format lengths, so our data structure can be built with a reasonable amount of memory and run time. Experimental results support our mathematical discussion for linear growth of the DFP data structure. Moreover, comparison of our data structure with integer decision diagrams reveals that our model is also efficient for modeling integer functions when utilized as an integer level diagram.

Keywords:

Formal verification decision diagrams, decimal floating point,

PDF

___

Price D. Pentium FDIV flaw-lessons lLearned. IEEE Micro 1995; 15: 86-88.
Sharangpani HP, Barton ML. Statistical Analysis of Floating Point Flaw in the Pentium Processor. Santa Clara, CA, USA: Intel Technical Report, 1994.
IEEE Computer Society. IEEE Std 754-1985: IEEE Standard for Binary Floating-Point Arithmetic. New York, NY, USA: IEEE, 1985.
IEEE Computer Society. IEEE Std 754-2000: IEEE Standard for Floating-Point Arithmetic. New York, NY, USA: IEEE, 2008.
Duale AY, Decker MH, Zipperer HG, Aharoni M, Bohizic TJ. Decimal floating-point in z9: an implementation and testing perspective. IBM J Res Dev 2007; 51: 217-227.
Lipetz D, Schwarz E. Self checking in current floating-point units. In: IEEE 2011 20th Symposium on Computer Arithmetic; 25–27 July 2011; Tubingen, Germany. New York, NY, USA: IEEE. pp. 73-76.
Corena M. IEEE 754-2008 decimal floating-point for Intel architecture processors. In: IEEE 2009 19th Symposium on Computer Arithmetic; 8–10 June 2009; Portland, OR, USA. New York, NY, USA: IEEE. pp. 225-228.
Gao S, Al-Khalili D, Langlois JMP, Chabini N. Decimal floating-point multiplier with binary-decimal compression based fixed-point multiplier. In: IEEE 2017 30th Canadian Conference on Electrical and Computer Engineering; 30 April–3 May 2017; Windsor, Canada. New York, NY, USA: IEEE. pp. 1-6.
Ray S. Scalable Techniques for Formal Verification. Berlin, Germany: Springer, 2010.
Camilleri A, Gordon M, Melham T. Hardware Verification Using Higher-Order Logic. Technical Report UCAM- CL-TR-91. Cambridge, UK: University of Cambridge, 1986.
Bryant RE. Graph-based algorithms for Boolean function manipulation. IEEE T Comput 1986; C-35: 677–691.
Fujita M, McGeer PC, Yang JCY. Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form Method Syst Des 1997; 10: 149-169.
Drechsler R, Theobald M, Becker B. Fast OFDD-based minimization of fixed polarity Reed-Muller expressions. IEEE T Comput 1994; 45: 1294-1299.
Kebschull U, Schubert E, Rosenstiel W. Multilevel logic synthesis based on functional decision diagrams. In: Proceedings of the European Conference on Design Automation; 16–19 March 1992; Brussels, Belgium. New York, NY, USA: IEEE. pp. 43-47.
Drechsler R, Sarabi A, Theobald M, Becker B, Perkowski MA. Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams. In: Proceedings of 31st Design Automation Conference; 6–10 June 1994; San Diego, CA, USA. New York, NY, USA: IEEE. pp. 415-419.
Drechsler R, Becker B. Ordered Kronecker functional decision diagrams, a data structure for representation and manipulation of Boolean functions. IEEE T Comput Aid D 1998; 17: 965-973.
Lai YT, Sastry S. Edge-valued binary decision for multi-level hierarchical verification. In: Proceedings of 29th ACM/IEEE Design Automation Conference; 8–12 June 1992; Anaheim, CA, USA. New York, NY, USA: IEEE. pp. 608-613.
Lai YT, Pedram M, Vrudhula SBK. Formal verification using edge-valued binary decision diagrams. IEEE T Comput 1996; 45: 247-255.
Bryant RE, Chen YA. Verification of arithmetic circuits with binary moment diagrams. In: 32nd Design Automation Conference; 12–16 June 1995; San Francisco, CA, USA. New York, NY, USA: IEEE. pp. 535-541.
Bryant RE, Chen YA. Verification of Arithmetic Functions with Binary Moment Diagrams. Technical Report CMU- CS-94-160. Pittsburgh, PA, USA: Carnegie Mellon University, 1994.
Drechsler R, Becker B, Ruppertz S. K*BMDs: a new data structure for verification. In: Proceedings of European Design and Test Conference; 11–14 March 1996; Paris, France. New York, NY, USA: IEEE. pp. 2–8.
Clarke EM, Fujita M, Zhao X. Hybrid decision diagrams, overcoming the limitations of MTBDDs and BMDs. In: Proceedings of IEEE International Conference on Computer-Aided Design; 5–9 November 1995; San Jose, CA, USA. New York, NY, USA: IEEE. pp. 159-163.
Ciesielski M, Kalla P, Zhihong Z, Rouzeyre B. Taylor expansion diagrams: a new representation for RTL verification. In: IEEE 6th International High-Level Design Validation and Test Workshop; 9 November 2001; Monterey, CA, USA. New York, NY, USA: IEEE. pp. 70-75.
Ciesielski M, Kalla P, Askar S. Taylor expansion diagrams: a canonical representation for verification of data flow designs. IEEE T Comput 2006; 55: 1188–1201.
Lotfi-Kamran P, Massoumi M, Mirzaei M, Navabi Z. Enhanced TED: a new data structure for RTL verification. In: 21st International Conference on VLSI Design; 4–8 January 2008; Hyderabad, India. pp. 481-486.
Lotfi-Kamran P, Hosseinabady M, Shojaei H, Massoumi M, Navabi Z. TED+: A data structure for microprocessor verification. In: Proceedings of Asia and South Pacific Design Automation Conference; 21 January 2005; Shanghai, China. New York, NY, USA: IEEE. pp. 567-572.
Alizadeh B, Fujita M. Modular datapath optimization and verification based on modular-HED. IEEE T Comput Aid D 2010; 29: 1422–1435.
Alizadeh B, Fujita M. Modular equivalence verification of polynomial datapaths with multiple word-length operands. In: IEEE 2011 International High Level Design Validation and Test Workshop; 9–11 November 2011; Napa Valley, CA, USA. New York, NY, USA: IEEE. pp. 22–40.
Chen YA, Bryant RE. *PHDD: An efficient graph representation for floating point circuit verification. In: Proceed- ings of IEEE International Conference on Computer Aided Design; 9–13 November 1997; San Jose, CA, USA. New York, NY, USA: IEEE. pp. 2-7.
Chen YA, Bryant RE. An efficient graph representation for arithmetic circuit verification. IEEE T Comput Aid D 2001; 20: 1443-1454.
Sayed-Ahmed AAR, Fahmy HAH, Kuhne U. Verification of the decimal floating-point square root operation. In: IEEE 2014 19th European Test Symposium; 26–30 May 2014; Paderborn, Germany. New York, NY, USA: IEEE. pp. 1-2.
Sayed-Ahmed AAR, Fahmy HAH, Samy R. Verification of the decimal floating-point fused-multiply-add operation. In: 9th IEEE/ACS International Conference on Computer Systems and Applications; 27–30 December 2011: Sharm El-Sheikh, Egypt. New York, NY, USA: IEEE. pp. 255-262.
Sayed-Ahmed AAR, Fahmy HAH, Hassan MY. Three engines to solve verification constraints of decimal Floating- Point operation. In: Conference Record of the 44th Asilomar Conference on Signals, Systems and Computers; 7–10 November 2010; Pacific Grove, CA, USA. New York, NY, USA: IEEE. pp. 1153-1157.

Turkish Journal of Electrical Engineering and Computer Science-Cover

ISSN: 1300-0632
Yayın Aralığı: Yılda 6 Sayı
Yayıncı: TÜBİTAK

Arşiv