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

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 Depth", number of the cycles, for which tool was not able to find any input pattern, which can fail the assertion.
Check the image of the [1/2] of the Model Checking Blog or you can check it here  : 

Now, you might think that, it is right, if I have "Proven" property, then I can party ;) . Also, it is helpful, if I have"Falsified" property, then I can analyse it and if proper, raise that bug to the design team. BUT, WHAT IS THE SIGNIFICANCE OF AN "INCONCLUSIVE" PROPERTY?

This is the place, where most of the Formal Engineers, are afraid of and that's why they don't adopt formal also. But you should not afraid from the Inconclusive Assertions. 

Inconclusive Assertions are "Natuaral Part" of the Model Checking. Generally, all real application assertions are "Inconclusive" assertions, as it becomes too difficult for the tool to prove it exhaustively. All assertions are starting as "Inconclusive" Assertions only.

Verification Sign-Off is still possible with the Inconclusive Assertion, if "Bounded Proof Depth" of that assertion is greater than "Required Proof Depth". So it is similar to Coverage metrix in Simulation based Verification. (Like, in coverage, you may not achieve it 100%, but still, you can sign-off the verification process, if you have got the "Required" coverage goals. Similarly, in Inconclusive Assertions also, you can sign-off the verification process, if you have got the "Required Proof Bound')

In Inconclusive, Bounded Proof Depth > Required Proof Depth => Equivalent to Full Proof

Now, we should discuss the possible reasons of the Inconclusive assertion.
  • State Space (Combination of all possible input patterns) and/or Complexity of the Design and/or Assertion (Complexity can be found by issuing tool specific commands)
  • Tool Options (Effort Level, Run Time, Memory Constraint, Algorithm)

To get the "Required Proof Bound":

  • Tool Options - Increase Run Time and/or Memory Constraint and/or Effort Level. Change Algorithm, to be used by the tool
  • Modify/Add Constraints - Constraints limits the possible input patterns. (Because tool needs to satisfy that constraint, similar like randomization constraint). So modification or addition of the constraint may reduce the state space of the design
  • Blackboxing - Blackbox helps tool to reduce complexity of the formal model, which it builds internally, considering the RTL, assertions and constraints. Outputs of the blackboxed modules/cells are driven by the formal tool. So one should put constraints on those inputs also.
  • Cut-points - In this, nets are cut from it's source and driven by the tool. So constraints can be applied on such nets.
  • Modify Assertion - Make assertion, as simple as possible. Also reduce, usage of the reference model.
  • Simulation Based Reset State - Through this way, one can run a normal simulation to reach upto certain state in the RTL, and then it can provide this data as the Reset State data to the tool, from which tool will start it's operation.
  • Guided Proof - Similar to the Simulation Based Reset State, in this case, an assertion can be used to trigger the evaluation of the other assertions.
  • Abstraction - Convert complex design elements into simple ones for use by the tool. Blackboxing, Cut-points can be used to abstract the design. Like, suppose you have 32 bit register, but you require only some states of that register, then you can cut that register and apply constraints on it according to your requirement.

When Model Checking can be used?


State Space of a Design

Model Checking is useful for the design, which does not have deep states, as deep states can increase the state space of the design drastically. 

 As shown in the above figure, the number of possible paths to reach to a state, increases exponentially as we go far from the initial states. And so the effort/time used by tool to exhaustively check those states, also increases exponentially. 

Pros & Cons of the Model Checking


Advantage - 

Simulation Path in Dark Black vs Exhaustive Formal Search (Image taken from Verification Academy)
  • Reduces Risk - Gives 100 % Surety 
  • More Efficient - Can reduce Verification Time & Effort, Eliminates Scenario Identification, Testbench Generation, Fully Automated Process
  • Exhaustive Nature
  • Can supplement Simulation, to get the coverage.

Disadvantage - 

  • State Explosion for Larger Designs (Many possible paths for each states)
  • Resource Limitation (May require impractical resources for larger designs)
  • End to End Checking expensive, because of Sequential Depth
  • Yet not a Mature Technology
---------------
This is the end of the Formal Verification through Model Checking blog series.

Hope you guys have at least got the basic idea about the Model Checking, how it's done, what are the required inputs for the tool, how tool works, advantages & disadvantages of the Model Checking.

Feel free to ask any question.

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