Portal de Periódicos da CAPES

Formal verification methods

2002; Association for Computing Machinery; Linguagem: Inglês

10.1145/514063.514064

0738-100X

David L. Dill, Nate James, Shishpal Rawat, Gérard Berry, Limor Fix, Harry Foster, Rajeev Ranjan, Gunnar Stålmarck, Curt Widdoes,

Embedded Systems Design Techniques

Do formal verification tools and methodologies require a drastic overhaul to move beyond equivalence checking? Equivalence checking catches errors in synthesis and local hand-modifications to designs. However, powerful formal verification technologies are emerging to combat "behavioral" errors, which represent today's biggest verification problems. Nonetheless, formal verification experts are split on how formal tools should adapt to this challenge. Some of our panelists feel that designers can sufficiently benefit from new formal verification technologies by making incremental changes to current methodologies. Others, however, argue that major changes are required to reap meaningful benefits from these new technologies. Just how much change is enough, what is the capacity of our current tools and what is limiting the full deployment of FV technology.Our panel of experts, consisting of users, tool providers, and core engine builders, will answer these challenging questions. The panel will debate these issues while discussing real life examples from the user base. They will provide a perspective of how the progression of technology will bring the real promise of formal verification to the user base.