Abstract
We present the formal verification of a gate-level computer system, in which a complex processor and external devices run in parallel. The system specification is an instruction set architecture with concurrently running visible devices. To the best of our knowledge this is the first formal treatment of integrating devices into a gate-level computer system.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Nuseibeh, B.: Ariane 5: Who dunnit? IEEE Softw. 14, 15–16 (1997)
The Verisoft Consortium: The Verisoft Project (2003), http://www.verisoft.de/
Moore, J.S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 161–172. Springer, Heidelberg (2003)
Alkassar, E., Hillebrand, M.A., Leinenbach, D.C., Schirmer, N.W., Starostin, A., Tsyban, A.: Balancing the load: Leveraging semantics stack for systems verification. JAR: Special Issue on Operating Systems Verification (to appear, 2009)
Dalinger, I., Hillebrand, M., Paul, W.: On the verification of memory management mechanisms. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 301–316. Springer, Heidelberg (2005)
Beyer, S., Jacobi, C., Kroening, D., Leinenbach, D., Paul, W.: Putting it all together: Formal verification of the VAMP. International Journal on Software Tools for Technology Transfer 8, 411–430 (2006)
Tverdyshev, S., Alkassar, E.: Efficient bit-level model reductions for automated hardware verification. In: TIME 2008, pp. 164–172. IEEE, Los Alamitos (2008)
Bevier, W.R., Hunt, W.A., Moore, S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5, 411–428 (1989)
Berry, G., Kishinevsky, M., Singh, S.: System level design and verification using a synchronous language. In: ICCAD, pp. 433–440 (2003)
ALDEC – The Design Verification Company: UART nVS (2006), http://www.aldec.com/products/ipcores/_datasheets/nSys/UART_nVS.pdf
Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I/O devices in the context of pervasive system verification. In: ICCD 2005, pp. 309–316. IEEE, Los Alamitos (2005)
Alkassar, E., Hillebrand, M., Knapp, S., Rusev, R., Tverdyshev, S.: Formal device and programming model for a serial interface. In: Beckert, B. (ed.) VERIFY 2007. CEUR Workshop Proceedings, vol. 259, pp. 4–20. CEUR-WS.org (2007)
Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 225–239. Springer, Heidelberg (2008)
Mueller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)
Beyer, S.: Putting It All Together: Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbrücken (2005)
Tomasulo, R.M.: An efficient algorithm for exploiting multiple arithmetic units. IBM Journal of Research and Development 11, 25–33 (1967)
Kröning, D.: Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Saarbrücken (2001)
Smith, J.E., Pleszkun, A.R.: Implementing precise interrupts in pipelined processors. IEEE Trans. Comput. 37, 562–573 (1988)
Brüss, R.J.: RISC Die MIPS-R3000-Familie. Architektur, Systembausteine, Compiler, Tools, Anwendungen. Siemens (1991)
Dalinger, I.: Formal Verification of a Processor with Memory Management Units. PhD thesis, Saarland University, Saarbrücken (2006)
Hillebrand, M.: Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, Saarland University, Saarbrücken (2005)
Tverdyshev, S.: Formal Verification of Gate-Level Computer Systems. PhD thesis, Saarland University, Saarbrücken (2009)
Alekhin, A.: The VAMP memory unit: Hardware design and formal verification effort. Master’s thesis, Saarland University, Saarbrücken, Germany (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hillebrand, M., Tverdyshev, S. (2009). Formal Verification of Gate-Level Computer Systems. In: Frid, A., Morozov, A., Rybalchenko, A., Wagner, K.W. (eds) Computer Science - Theory and Applications. CSR 2009. Lecture Notes in Computer Science, vol 5675. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03351-3_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-03351-3_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03350-6
Online ISBN: 978-3-642-03351-3
eBook Packages: Computer ScienceComputer Science (R0)