Abstract
Hardware design is considered one of the traditional areas for formal (property) verification (FPV); in particular for symbolic model checking. Indeed, Intel, SUN, Motorola and IBM all develop and deploy model checking tools to ensure design correctness. On the other hand, hardware design is hostile territory because of the huge effort companies traditionally invest in classical testing and validation techniques which tend to be much more automated, require less sophistication from users and which will, in fact, discover many errors when deployed on such a scale. For these reasons FPV will never fully supplant traditional validation.
The real challenge lies in convincing processor design teams that diverting some of their validation resources to FPV leads to provably higher design quality. Complicating factors include the relatively high quality of traditional validation|at least within Intel|which raises the bar for FPV; and the fact that in high-performance processors design large parts of the RTL tends to remain unstable enough throughout the design to make it very hard to verify suitable micro-architectural abstractions. For these reasons, FPV within Intel traditionally targets the same RTL from which the schematics is derived and on which all traditional validation is performed.
Arguably the biggest (public) FPV success story within Intel is that of floating point hardware verification and it is illustrative to see how FPV is deployed in this area and how tool and methodology development is influenced.
The major challenge that we are now facing is to move formal verification upstream in the design flow. Not only because ever increasing micro- architectural complexity creates a strong demand for early verification on an algorithmic level, but also because the ever shortening design cycle forces formal verification to start much earlier in the design. It is here that hardware FPV and software verification start to merge and there are lessons to be learned for either side.
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.
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 subscriptionsAuthor information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gerth, R. (2001). Model checking if your life depends on it: a view from intel’s trenches. In: Dwyer, M. (eds) Model Checking Software. SPIN 2001. Lecture Notes in Computer Science, vol 2057. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45139-0_2
Download citation
DOI: https://doi.org/10.1007/3-540-45139-0_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42124-5
Online ISBN: 978-3-540-45139-6
eBook Packages: Springer Book Archive