An easy approach to formal verification

Author

Schlipf, T. ; Büchner, T. ; Fritz, R. ; Helms, M.

Author_Institution

IBM Deutschland Entwicklung GmbH, Boeblingen, Germany

fYear

1997

fDate

7-10 Sep 1997

Firstpage

120

Lastpage

124

Abstract

Formal verification suffers from the image that it is complicated and requires a lot of mathematical background to be applied successfully. In this paper a methodology is described that adds formal verification (FV) to the verification process without requiring any knowledge of FV languages. It solely uses the finite state machine notation, which is familiar and intuitive to designers. Another problem of FV is state space explosion. If this occurs we can switch to random simulation within an hour without losing any effort. The results show that FV is at least as fast as random simulation and it is superior in terms of verification quality because it is exhaustive

Keywords

application specific integrated circuits; circuit CAD; finite state machines; formal verification; integrated circuit design; state-space methods; exhaustive process; finite state machine notation; formal verification; random simulation; state space explosion; verification quality; Automata; Circuit simulation; Circuit testing; Error analysis; Error correction; Formal verification; Logic testing; State-space methods; Switches; System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

ASIC Conference and Exhibit, 1997. Proceedings., Tenth Annual IEEE International

Conference_Location

Portland, OR

ISSN

1063-0988

Print_ISBN

0-7803-4283-6

Type

conf

DOI

10.1109/ASIC.1997.616990

Filename

616990