Abstract
In this paper we describe a methodology for the formal verification of a processor using the CTL property language. Processors are important in design and verification of digital systems because they have structures that represent most digital systems. Processors are programmable, have control parts, data parts and are rich in bus structure. Verification of CPU structures requires verification of data components, controllers, datapath and instruction level verification. This work uses a processor to discuss various features of formal verification. Because of generality of processors, we will be able to cover most aspects of property-based verification and properties used for this purpose.
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
E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,” in ACM Transitions on Programming Languages and Systems, 8(2), pp. 244–263, 1986.
Jae-Young Jang, In-Ho Moon, Gary Hachtel, ”Iterative Abstraction-based CTL Model Checking.”,in Design, Automation & Test in Europe, Paris, France, March 27–30, 2000.
Tom Schubert, “High Level Formal Verification of Next-Generation Microprocessors”, 40th Conference on Design Automation Conference (DAC’2003), 2003.
J. R. Burch, “Techniques for Verifying Superscalar Microprocessors”, Proceedings of the 33rd Design Automation Conference (DAC‘96), 1996.
H. Choi, B. Yun, Y. Lee, and H. Roh, “Model Checking of S3C2400X Industrial Embedded SOC Product”, Proceedings of the 38th Conference on Design Automation Conference (DAC‘2001), 2001.
R. Jhala, and K. L. McMillan, “Micro Architecture Verification by Compositional Model Checking”, Proceedings of the 13th International Conference on Computer Aided Verification (CAV’2001), 2001.
Goel, and W. R. Lee, “Formal Verification of an IBM Core Connect Processor Local Bus Arbiter Core”, Proceedings of the 37th Conference on Design Automation Conference (DAC‘2000), 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science+Business Media Dordrecht
About this paper
Cite this paper
Shojai, H., Navabi, Z. (2004). Formal Specification for Hardware Verification. In: Ionescu, A.M., Declercq, M., Kayal, M., Leblebici, Y. (eds) Microelectronics Education. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-2651-5_12
Download citation
DOI: https://doi.org/10.1007/978-1-4020-2651-5_12
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-015-7052-7
Online ISBN: 978-1-4020-2651-5
eBook Packages: Springer Book Archive