Formal Verification of Complex Data Paths: An Industrial Experience

• 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.

Subject headings

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)

Keyword

Circuit visualization

Symbolic trajectory evaluation

Functional languages

Model checking

Formal verification

Publication and Content Type

kon (subject category)

ref (subject category)