Formal Verification

Basic Terminology

Mostly Used Formal Methods:

1. Equivalence Checking
2. Model Checking
3. Theorem  Provoking.

•  Theorem Proving: Relationship between a specification and an implementation is regarded as a theorem in a logic, to be proved within the framework of a proof calculus 
• Used for verifying arithmetic circuits in industry
• 
  
• Model Checking: The specification is in the form of a logic formula, the truth of which is determined with respect to a semantic model provided by an implementation Starting to be used to check small modules in industry 
• 
  
• Equivalence Checking: The equivalence of a specification and an implementation checked Most common industry use of formal verification
• 
  
•  Symbolic Trajectory Evaluation: Properties specified as assertions about circuit state (pre- and post- conditions), verified using symbolic simulation 
• Used to verify embedded memories in industry