What is Formal Verification through Model Checking? [1/2]

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 :

  1. Equivalance Checking  - Verifies Functional Equivalence of 2 designs, which are at smae or different abstraction level. Like RTL to RTL, RTL to Gate Level, Gate Level to Gate Level, Gate Level to Post Layout. (Already used in Industry, with stable Tool Support)
  2. Model Checking - Verifies whether the implementation satisfies property of the design or not.


Model Checking Basics

Model Checking Block Diagram

As shown in the above image, there are primarily 3 basic elements of the Model Checking : User Defined Property, User Defined Constraint, RTL Design. 

All 3 elements are provided to the Model Checking Tool and tool builds a model, from this data and tries to prove all the properties exhaustively, on Formal engines.

There are basically 2 parts of the Model Checking :

  • Simulation Based Reset State - Most sequential designs do not operate properly without a reset procedure which establishes a valid starting state. We need to apply the same sort of initialization when running formal analysis in order to get valid results. If no initial state is specified, the default is to start with an initial state where all the state holding elements are of value X. This may produce false failures because the formal analysis was based on an initial state that can never occur in the real design. 
  • Tool Driven Formal State - In this state, tool evaluates the assertion. This state is not Simulation driven.

Properties & Constraints

Properties - 

  • Assertions, which will be checked exhaustively by the Model Checking Tool.
  • Can be written in many languages like SVA, PSL or TCL also.
Basic 2 types of properties for Model Checking Tool - 
  • Safety Property - "Something will never happen" or "Something always happens" type of property. So these type of properties can be violated in finite run and hence they are comparatively easy for tool to verify. 
  • Liveness Property - "Something will eventually happen" type of properties. So these type of properties can be violated in infinite run, and hence they are comparatively complex for tool to verify.

Example of the Safety Property - 
"grant signal will always be asserted exactly after 2 clock cycles of assertion of request signal"
assert property (@ (posedge clk) (req -> ##2 grant));

Example of the Liveness Property - 
"red traffic signal will eventually be converted into green traffic signal"
assert property (@ (posedge clk) (red_traffic |-> ##[1:$] green_traffic));

Constraints - 

  • Properties, which must be true for design to be operated properly.
  • Can be written in many languages like SVA, PSL or TCL also.
  • Tool will always try to generate those input stimulus, which satisfies the constraints.
  • Constraints can be written on the cut-points, input of the design and output of the blackboxed modules only.
Over & Under Constrained Scenarios

It is very important to identify valid & required constraints, as otherwise, we may get errorneous scenario like : 
  • Over Constrained - Some legal input patterns are not applied to the design, which may lead to false proofs of the assertion and may miss some bugs.
  • Under Constrained - Some illegal input patterns are applied to the design, which may lead to false failure of the assertion and wastage on debugging time. 

Example of the Valid Constraint : 
"Valid Register addresses are only from 8'h0 to 8'hff. And those registers are connected to the APB interface"
assume property (@(posedge PCLK) (PADDR inside {[32'h0000:32'h00ff]}));

-----------------
So guys, we will end this post, at this point. I believe this information is sufficient to get the basic idea on the Model Checking. 

Do visit the blog, as in the next post, I will give you the idea on Model Checking Advantages, Limitations & It's Outputs

Feel free to comment any question, if you have.


Comments

Post a Comment

Popular posts from this blog

SystemVerilog Event Regions

Image
Hi All, In the last post, we had discussed the Verilog Event Regions. Today we'll discuss the event regions in SystemVerilog, which are somewhat similar to the Verilog Event regions only, plus there are some additional regions as well. Similar to Verilog, in Systemverilog also the event queue is divided into 5 different regions. A SystemVerilog simulator, shall maintain some form of data structure that allows events to be dynamically scheduled, executed, and removed as the simulator advances through time. Simulation proceeds by executing and removing all events in the current simulation time slot before moving on to the next nonempty time slot, in time order. And in that given simulation timeslot, it is necessary to execute events of all of the above mentioned regions. Most important thing is that these regions encompass the Verilog Event Regions and hence the legacy Verilog code should run correctly without any modification in SystemVerilog simulator. Prepone Region
Read more

Standard Cell Based ASIC Design Flow

Image
Hi All,  Today we will discuss about ASIC Design Flow, as it is one of the most important and crucial thing to understand. ASIC Design Flow Now, we will try to get brief idea about each steps in the above image. Specification  - Specification of the system, like what is the functionality of system, what is the desired speed of the system, area constraint of the system, whether it has any power constraint or not, tolerances of various constraints, operative conditions of the system. RTL Description  - Generally after specification, the system is partitioned into various blocks and RTL description (HDL Code like Verilog or VHDL), mostly in behaviour form is written. Sometimes Higher Level Language Code like C/C++ is also written, and in that case, a High Level Synthesis Tool is used, which converts the Higher Language Code into RTL Level Code. After RTL Coding, Functional Verification is done to check the correctness of the functionality. Logic Synthesis  - Now, wh
Read more

How to implement more than 1 Analysis Implementation Ports in a Class in UVM

Hi All, In this post, we will discuss about how to include more than 1 Analysis Implementation Port in a Class in UVM. Analysis Ports are used for many purposes like Coverage Collection, Received/Transmitted Packet Checking. And sometimes, you may need to take coverage on different packets (so you will require different analysis implementation ports) and you do not want to define 2 different class, just for coverage. So if there are more than 1 (suppose 2) analysis implementation ports in a class, then obvious (and the first also !!!) question arises in the mind is that, how to implement 2 write methods in the same class. Well, in UVM, we have 2 different methods to address the problem. Method - 1 : Use "imp" Suffix defined via Macro Declare Macro `uvm_analysis_imp_decl(<Postfix>) outside of the component. This macro adds post-fix to the analysis implementation port class name and associated write method. Instantiate Analysis Implementation Port with u
Read more