Abstract
This chapter presents a summary of the application results obtained by using automatic verification tools in practice. Therefore a summary of the design and verification methodology and a walk through several different applications, which have been treated with formal verifications tools at several different sites of the Siemens AG, is given. For each application we describe the basic functionality and how formal verification technique was used during the design process.
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
J. Bormann (1993a): CVE deckt Fehler im Entwurf eines FiFo-Speichers auf. Siemens Bericht ZFE BT SE 1-93/94-JB-2.
J. Bormann (1993b): Formale Verifikation eines Token Ring Controllers mit CVE. Siemens Bericht ZFE BT SE 1-93/94-JB-1.
J. Bormann, J. Lohse, M. Payer, G. Venzl (1995). Model Checking in Industrial Hardware Design. In Proceedings 32nd DAC, San Francisco, CA.
R. E. Bryant (1986): Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang (1992): Symbolic Model Checking: 1020 States and beyond. Inf. Comput. (USA), vol. 98, no. 2, p. 142–170.
E.M. Clarke, J.R. Burch, O. Grumberg, D.E. Long, K.L. McMillan (1992): Automatic Verification of Sequential Circuit Designs. Philos. Tran. R. Tran. R. Soc. A, Phys. Sci. Eng (UK), vol. 339, no. 1652, page 105–120, April.
J. Lattermann (1995): Model Checking eines V24-Controllers mit CVE Siemens Bericht ÖN TN EC B32, September.
E. Felt, R. Brayton, A. Sangio-Vincentelli, and G. York (1993): Dynamic variable ordering for BDD minimization. In Proc. of the European Design Automation Conference (EURO-DAC’93), September.
R. Herrmann and F. Korf (1995): Formale Verifikation eines Arbiters mit CVE2. Siemens Bericht ZFE T SE 1-94/95-RH-1, ZFE T SE 1, SNI MR PD 151.
R. Rudell (1993): Dynamic variable ordering for ordered binary decision diagrams. In Proc. of the 9th Int. Conference on Computer Aided Design (ICCAD’93), November.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 ECSC-EC-EAEC, Brussels-Luxembourg
About this chapter
Cite this chapter
Herrmann, R., Bormann, J., Filkorn, T., Lohse, J., Schneider, HA. (1997). Siemens Industrial Experience. In: Kloos, C.D., Damm, W. (eds) Practical Formal Methods for Hardware Design. Research Reports Esprit. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-60641-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-60641-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62007-5
Online ISBN: 978-3-642-60641-0
eBook Packages: Springer Book Archive