Preverify in Formality. When to use it?

[TonyLS]

Hi,

Is it best to always use the preverify command in Formality? I've seen scripts with and without it.

Is there a rule of thumb on when to use it?

Thanks

 

[D.A.(Tony)Stewart]

"the datapath solver uses a particular algorithm to solve multipliers in the preverification stage that can significantly reduce the entire verification runtime. When the solver successfully preverifies a multiplier in your design, Formality converts it to a black box for the rest of verification. If the datapath solver is unable to
preverify your multiplier, Formality returns an inconclusive result in the transcript.

For suggestions about preparing your designs for successful verification, see “Handling Designs When Verification Is Incomplete” on page 7-4. search p. 283, 284

https://silo.tips/queue/formality-user-guide?&queue_id=-1&v=1711048315&u=MjYwNzpmZWE4OjNmZGM6YTY3MDozMDIyOmRjMWI6ODRjZTo2MjMx