Questa Formal verification

请问一下这个基于断言的工具大家在公司里用的多不呢.userguiad上说在设计的早期可以用来进行验证不用写太复杂的testbench，dut的输入来指sequence或者波形文件，然后用assertion去检查功能点。个人感觉没啥必要呢，testbench写完了再挂上assertion验证就一步到位了，为什么还要分成两个阶段，一般在那种设计中需要这样的formal verification?
请问各位，不是很明白啊

formal验证的效率更高吧，输入sequence有时候需要很多输入才能验证，这样很慢

啊啊啊啊

有点意思啊