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

SystemVerilog
, , , , ,
1

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?

2

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

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) http://goo.gl/u20Om2
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
3

In reply to ben@SystemVerilog.us:

Are Model Checking & Assertion Based Formal Verification same?

4

In reply to Karan:
From Model checking - Wikipedia
model checking or property checking refers to the following problem: Given a model of a system, exhaustively and automatically check whether this model meets a given specification.

5

In reply to ben@SystemVerilog.us:

Ok So from that article, I understand that Assertion Based Formal Verification and Model Checking, both are same.

Correct me, if I am wrong.

6

In reply to Karan:
From Formal verification overview
I believe that there is an implicit understanding that “model checking” means “Model-checking formal verification” done with assertions using an assertion language like PSL or SVA. This would contract to checking a model with simulation, which is then referred to as “simulation verification”

I did a search on “model checking formal verification onespinsolutions” (OneSpin is vendor of formal verification tools).
I also did a search on “model Checking formal verification mentor graphics”
(Mentor is also a vendor of formal verification tools).
They both referred to articles on the Use of Formal Model Checking in SoC Design Verification
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448