Sökning: onr:"swepub:oai:research.chalmers.se:389d5a75-3c37-45d9-aa81-b74908011830" >
Formal Verification...
Formal Verification of Complex Data Paths: An Industrial Experience
-
- Seger, Carl-Johan, 1961 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2021-11-10
- 2021
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 13047 LNCS, s. 697-716
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- After caches, most transistors in a modern microprocessor are devoted to wide data-paths. Due to performance and power requirements, these data-paths often use complex implementations of sophisticated algorithms. As Intel experienced in 1994, a bug in a data-path can be extremely expensive and thus needs to be avoided at almost any cost. At the same time, simulation based verification is extremely poor at verifying data-paths due to the vast data space and thus formal verification is almost a requirement. In this paper a retrospective is given of the formal verification of complex data-paths that took place at Intel from the mid 1990 s until very recently. The technology that made the effort possible, the tools developed that made it feasible, and the methodology created that made it practical will all be discussed. Finally, a few examples that illustrates the approach will be presented as well as a concluding discussion on what the goal of using formal verification should be.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Annan data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Other Computer and Information Science (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Nyckelord
- Circuit visualization
- Symbolic trajectory evaluation
- Functional languages
- Model checking
- Formal verification
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas