Formal verification with assertions

Hello,

I was reading the advantages of using formal verification (FV)techniques during exhaustive verification.
I found that Questa Formal Verification is the perfect tool for that task.
I have been using QuestaSim tool for functional verification task. My question is this: Is Questa Formal verification a separate tool not included in QuestaSim package?

If so, is there any educational version of Questa Formal Verification tool ?

Thank you

In reply to vico:

Please see Engineering educator and student resources | Siemens Software

In reply to vico:
As a side comment, I strongly recommend the following book on formal verification

  • Formal Verification: An Essential Toolkit for Modern VLSI Design 1st Edition
    by Erik Seligman
    See the reviews and sample pages at Amazon http://goo.gl/TZ640S

Ben SystemVerilog.us