Difference between Formal Verification through Model Checking & Assertion Based Formal Verification

In reply to Karan:

What are the different types of Formal Verification?
I know only 2 types :

  • Logic Equivalence Checking (Checks equivalence between various designs like RTL & Synthesized Netlist or Synthesized Netlist & Post Layout Netlist)
  • Property Checking / Assertion Based Checking (Checks Functional Correctness of any RTL)
    Please let me know, if there are more types of Formal Verification.
    Is Model Checking is same as Assertion Based Checking?

You’re correct on all of what you stated.
On formal verification, see
https://verificationacademy.com/forums/systemverilog/what-do-after-inconclusive-assertion-assertion-based-formal-verification#reply-51721

Also, see my recommendations for the book
Formal Verification: An Essential Toolkit for Modern VLSI Design 1st Edition by Erik Seligman (Author), Tom Schubert (Author), M V Achutha Kiran Kumar (Author) Formal Verification: An Essential Toolkit for Modern VLSI Design: Seligman MS, Erik, Schubert, Tom, Kumar M.Tech, M V Achutha Kiran: 9780128007273: Amazon.com: Books
Also, read the reviews at Amazon.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115