Is Formal Verification Bound to Remain a Junior Partner of Simulation?

  • Wolfram Büttner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


After decades of research the late eighties and the nineties have produced a number of “checkers” verifying complex aspects of industrial designs and thus raising the attention of early adopters. These achievements, however, have not led to wide adoption. The generally accepted explanation of this resistance is the required methodology change and the lacking ease of use. We see a more fundamental reason in the difficulty to set up a compelling value proposition based on isolated proven theorems.

With the advent of assertion-based verification the first two of the above obstacles are being successfully tackled. In this framework formal verification is piggybacking on advanced and established simulation platforms.

We foresee as a next step in the evolution of formal verification fully formal solutions for important functional verification tasks. Similar to formal equivalence checking these solutions will excel by extreme quality and improved productivity. This claim is exemplified by reporting about the formal verification of an industrial embedded processor within a large national initiative involving industry and academia.


Mathematical Logic Software Engineer Formal Solution Formal Language Proven Theorem 
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.

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Wolfram Büttner
    • 1
  1. 1.OneSpin Solutions GmbHMunichGermany

Personalised recommendations