VLSI RANDOM

Hi All, This is the 2nd post on the Formal Verification. Here we will discuss about the remaining topics of the Formal Verification through Model Checking. Results of the Model Checking Now that, you know, that Model Checking is all about Properties, Constraints & Tool, we shall examine how tool works. Now the job of the Model Checking tool is to verify User Defined Properties exhaustively, by satisfying the User Defined Constraints. There are basically 3 types of results for any Property, Model Checking tool can give. Conclusive, Proven - Property is exhaustively verified, and you can be assured, that there is no bug in that piece of RTL. Conclusive, Falsified - Property has been failed. In this case, tool will provide you the Falsification Trace (Set of input pattern, which can make the property to fail) Inconclusive (Bounded Proof) - Tool can not confirm the proof or falsification of the property. In this case, tool will provide you the "Bounded Proof

Hi All, Sorry for the delay in the post. But you know, good content takes it's own time ;) Today we will discuss about a relative new technology for verification, Formal Verification through Model Checking. I hope, you guys will know the fundamentals or theory of the Model Checking, by reading this post. What is Formal Verification? Before knowing about Model Checking, we must know about Formal Verification. Formal Verification is an algorithmic based approach, to logic verification, that exhaustively proves functional properties of a design. Focus is not on Stimulus, but rather correctness of the reference. Proves or disapproves, correctness of the design mathematically. Most commonly used algorithms : BDD/ROBDD, SAT Solvers (We may talk about this algorithms in subsequent blog posts) There are 2 types of the Formal Verification : Equivalance Checking  - Verifies Functional Equivalence of 2 designs, which are at smae or different abstraction level. Like R