What kind of role the formal verification tool play ?

Just from my point of view:
The typical way to verify the design is (Dynamic) simulation and it's still the mainstream.

The new trend for synchronous design verification is using STA(static timing analysis) + Formal Verification.
STA: For timing check
&
Formal Verification: For functional check.

I have tried $ynopsys' Formality 2002.5 and Verp|ex's LEC(logic equivalence checker) recently.
But I was quite disappointed with these tools' result(s). Because there are always some false mismatch, and it takes time to analyze the reason :?

My question is "Does it worth spending time on formal verification ?"
(Because....
I think although gate-level simulation may take lots of time, it is run by the tool. By contrast, find out the mismatch is real or false need the man power !)

Dear joe2moon

You are starting a very interesting discussion. Formal Verification promises much faster results, especially as design complexity is continuously increasing, while dynamic simulation offers practical applications. Your points are correct. However only time can show what is about to happen. I remember the VHDL International Users Forum in 1997, where an Italian Professor spoke and said that he could not understand how his students used a language (VHDL) and a computer to design circuits and not schematics on a piece of paper. The answer he got from and industry representative was "VHDL is here to stay!" At the moment, IMHO we can not say if formal verification has come to stay or not. It looks like!

We can say many more about the topic but I think I have to stop. joe2moon I would suggest to take a look at the proceedings or attend DAC, ICCAD or DATE conferences! And once again thank you for the nice subject you have put on even if it does not fit exactly with elektroda (IMHO).

Best Formal Verification Tool ?

Maybe I should ask the question in another way

1) Have you ever used the formal verification (or equivalence check) tool in your design phase ?

If yes, then
2.1) Which tool do you ues ? a)$ynopsys' F0rmality 2002.5 b) Verp|ex's LEC 3.0.1(Logic Equivalence Checker) c)C@dence's F0rmalCheck in LDV40, d) Ment0r's FormalPr0 3.1 or e)Others.
2.2) Why you choose this one ? (runtime, accuracy,price,...?)

And
3) In which condition, will you think it is necessary to do the formal verification ?

LEC is now more popular than formality . But both of them look quite similar on its GUI face . It's very convient to use the formal tools to track the ECO netlist change . Image that how you can guarantee everytime the netlist change is functional equalvent to the previous netlist . In every stage we change the minor gates we use the LEC to check it again to make sure they are consistent . There are some points very different from the dynamic sim .
1. They need not the test patterns
2. They cover every register/port fan-in cone , its coverage is higher far from daynamic sim
3. The run-timing/storage is superior than dynamic sim
If u would like to compare ASIC/FPGA , it had better to use the same eda vendor tools . Like synplify_asic/synplify_pro or DC/FPGA_express . The problem often come from the don't care conditions in logic mapping . Top level compare is more easy, the sub-module u should set equals and some constant which it may result unreachable primary output . The add compare points sometimes get wrong compared points , it need handed change . You shall feel comfotable after you know what happen underneath and know how to solve it next time.