Abstract
Commercial competition is forcing computer companies to get better products to market more rapidly, and therefore the time for validation is shrinking relative to the complexity of microprocessor designs. Improving time-to-market performance cannot be solved by just growing the size of design and validation teams. Design process automation is increasing, and the adoption of more rigorous methods, including formal verification, is unavoidable because for achieving the quality demanded by the marketplace.
Intel is one of the strongest promoters of the use of formal methods across all phases of the design development. Intel’s design teams use high-level modeling of protocols and algorithms, formal verification of floating-point libraries, design exploration systems based on formal methods, full proofs and property verification of RTL specifications, and equivalence checking to verify that transistor-level schematics correspond to their RTL specifications. Even with the best effort to adopt the progress in formal methods quickly, there is a large gap between an idea published at a conference and a development of a tool that can be used on industrial-sized designs. These tools and methods need to scale well, be stable during a multi-year design effort, and be able to support efficient debugging. The use of formal methods on a live design must allow for ongoing changes in the specification and the design. The methodology must be flexible enough to permit new design features, such as scan and power-down logic, soft error detection, etc. In this paper, I will share my experience with the formal verification of the floating-point unit on an Itanium(R) microprocessor design and point out how it may influence future microprocessor-design projects.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aagaard, M., Jones, R., Seger, K.-J.: Formal Verification Using Parametric Representations of Boolean Constraints. In: Proc. of the 36th ACM/IEEE conference on Design Automation, pp. 402–407. IEEE Computer Society Press, Los Alamitos (1999)
Aagaard, M., Jones, R., Kaivola, R.: Formal Verification of Iterative Algorithms in Microprocessors. In: ACM/IEEE Proc. of Design Automation Conference, pp. 201–206. IEEE Computer Society Press, Los Alamitos (2000)
Aagaard, M., Seger, K.-J.: The Formal Verification of a Pipelined Double-Precision IEEE Floating-Point Multiplier. In: ACM/IEEE Proc. of the International Conference on Computer-Aided Design, pp. 7–10. IEEE Computer Society Press, Los Alamitos (1995)
Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)
Coe, T.: Inside the Pentium FDIV bug. Dr. Dobbs Journal, 129-135 (April 1996)
Chen, Y.-A., Bryant, R.: Verification of Floating-Point Adders. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 488–499. Springer, Heidelberg (1998)
Fisher, L.M.: Flaw reported in a new Intel chip. New York Times, May 6, D 4:3 (1997)
Flatau, A., Kaufmann, M., Russinoff, D., Smith, E., Sumners, R.: Formal Verification of Microprocessors at AMD. In: Designing Correct Circuits (2002)
Harrison, J.: Formal Verification of Floating-point Trigonometric Functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 217–233. Springer, Heidelberg (2000)
Harrison, J.: Formal Verification of IA-64 Division Algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 234–251. Springer, Heidelberg (2000)
Harrison, J.: Formal Verification of Square Root Algorithms. Formal Methods in System Design 22, 143–153 (2003)
Harrison, J.: Floating-Point Verification. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 529–532. Springer, Heidelberg (2005)
Formal Verification of a Fully IEEE Compliant Floating Point Unit. Dissertation, University of Saarbruecken (April 2002)
Jacobi, C., Weber, K., Paruthi, V., Baumgartner, J.: Automatic Formal Verification on Fused-Multiply-Add FPUs. In: Proc. of the conference on Design, automation and test in Europe (DATE) (2005)
Koren, I.: Computer Arithmetic Algorithms, 2nd edn. A.K.Peters, Wellesley (2002)
Kaivola, R., Aagard, M.: Divider Circuit Verification with Model Checking and Theorem Proving. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 338–355. Springer, Heidelberg (2000)
Kaivola, R., Kohatsu, K.: Proof Engineering in the Large: Formal Verification of Pentium(R) Floating-Point Divider. Software Tools for Technology Transfer 4(Issue 3), 323–335 (2003)
Kaivola, R., Narasimhan, N.: Formal Verification of the Pentium(R) Floating-Point Multiplier. In: Proc. of the conference on Design, automation and test in Europe (DATE) (2002)
Nievergelt, Y.: Scalar Fused Multiply-Add Instructions Produce Floating-Point Matrix Arithmetic Provably Accurate to the Penultimate Digit. ACM Transactions on Mathematical Software (TOMS) 29(Issue 1), 27–48 (2003)
O’Leary, J., Zhao, X., Gerth, R., Seger, C.-J.: Formally Verifying IEEE Compliance of Floating-point Hardware. Intel Technology Journal, Q1 1999 (1999)
Russinoff, D., Flatau, A.: Mechanical Verification of Register-Transfer Logic: A Floating-Point Multiplier. In: Kaufmann, M., Manolios, P., Moore, J. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, Dordrecht (2000)
Russinoff, D.: A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD-K7 Floating-Point Multiplication, Division, and Square Root Instructions. LMS Journal of Computation and Mathematics 1, 148–200 (1998)
Russinoff, D.: A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon(TM) Processor. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 3–36. Springer, Heidelberg (2000)
Schubert, T.: High Level Formal Verification on Next-Generation Microprocessors. In: ACM/IEEE Proc. of Design Automation Conference, pp. 1–6. IEEE Computer Society Press, Los Alamitos (2003)
Seger, C.-J.H., Bryant, R.E.: Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods in System Design 6(2), 147–189 (1995)
Slobodová, A., Nagalla, K.: Formal Verification of Floating-Point Multiply-Add on Itanium(R) Processor. In: Designing Correct Circuits (Unpublished Proc.), Barcelona, March (2004)
Paulson, L.: ML for the Working Programmer. Cambridge University Press, Cambridge (1996)
IEEE Standard for Binary Floating-Point Arithmetic. ANSI/IEEE Std 754-1985
Intel(R) Itanium(R) Architecture Software Developer’s Manual. Revision 2.1, Document numbers: (245317-245319)-004, Intel Corporation (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Slobodová, A. (2007). Challenges for Formal Verification in Industrial Setting. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds) Formal Methods: Applications and Technology. PDMC 2006. Lecture Notes in Computer Science, vol 4346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70952-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-70952-7_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70951-0
Online ISBN: 978-3-540-70952-7
eBook Packages: Computer ScienceComputer Science (R0)