Abstract
In the VAMP (verified architecture microprocessor) project we have designed, functionally verified, and synthesized a processor with full DLX instruction set, delayed branch, Tomasulo scheduler, maskable nested precise interrupts, pipelined fully IEEE compatible dual precision floating point unit with variable latency, and separate instruction and data caches. The verification has been carried out in the theorem proving system PVS. The processor has been implemented on a Xilinx FPGA.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
Brock, B., Hunt, W.A., Kaufmann, M.: The FM9001 microprocessor proof. Technical Report Technical Report 86, Computational Logic Inc. (1994)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessors control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Chen, Y.-A., Clarke, E.M., Ho, P.-H., Hoskote, Y., Kam, T., Khaira, M., O’Leary, J.W., Zhao, X.: Verification of all circuits in a floating-point unit using word-level model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 19–33. Springer, Heidelberg (1996)
Damm, W., Pnueli, A.: Verifying out-of-order executions. In: Charme IFIP WG10.5, Montreal, Canada, pp. 23–47. Chapman & Hall, Boca Raton (1997)
Eiriksson, A.P.: The formal design of 1M-gate ASICs. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 49–63. Springer, Heidelberg (1998)
Hennessy, J.L., Patterson, D.A.: Computer Architecture:A Quantitative Approach, 2nd edn. Morgan Kaufmann, San Mateo (1996)
Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 47–59. Springer, Heidelberg (1999)
Institute of Electrical and Electronics Engineers. ANSI/IEEE standard 754–1985, IEEE Standard for Binary Floating-Point Arithmetic (1985)
Jacobi, C.: Formal verification of complex out-of-order pipelines by combining modelchecking and theorem-proving. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 309. Springer, Heidelberg (2002)
Jacobi, C.: Formal Verificaton of a fully IEEE compliant floating point unit. PhD thesis, Saarland University, Germany (2002)
Kroening, D.: Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Computer Science Department (2001)
Kröning, D., Müller, S., Paul, W.: Proving the correctness of pipelined micro-architectures. In: 3ITG-/GI/GMM-Workshop Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und System, pp. 89–98. VDE Verlag (2000)
Kröning, D., Müller, S., Paul, W.: Proving the correctness of processors with delayed branch using delayed PCs. pp. 579–588 (2000)
Kröning, D., Paul, W.: Automated pipeline design. In: Proc. of the 38th Design Automation Conference, pp. 810–815. ACM Press, New York (2001)
McMillan, K.: Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
McMillan, K.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 179. Springer, Heidelberg (2001)
Mueller, S.M., Paul, W.J.: Computer Architecture. Complexity and Correctness. Springer, Heidelberg (2000)
O’Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal Q1 (1999)
Owre, S., Shankar, N., Rushby, J.M.: PVS:A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Russinoff, D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS Journal of Computation and Mathematics 1, 148–200 (1998)
Russinoff, D.M.: A case study in formal verification of register-transfer logic withACL2: 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)
Sawada, J., Hunt, W.A.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
Shen, X., Arvind, Rudolph, L.: CACHET: an adaptive cache coherence protocol for distributed shared-memory systems. In: International Conference on Supercomputing (1999)
Stoy, J., Shen, X., Arvind: Proofs of correctness of cache-coherence protocols. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 43. Springer, Heidelberg (2001)
Velev, M.N., Bryant, R.E.: Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 37–53. Springer, Heidelberg (1999)
Velev, M.N., Bryant, R.E.: Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. In: DAC, ACM, New York (2000)
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
Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.J. (2003). Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive