difference between formal verification and dynamic verification

[badrino]

hello every body,

there is someone which can give me the differece between formal verification and dynamic verification???

thanks in advance.

 

[vikas gupta]

Hi Dynamic verification is when you actually run a testcase and you can see in the waveform of different signals that they are changing their values during the running of the testcase..(they may take a constant value in some exceptional cases). Formal verification ...from what I have encountered by using IFV is that it is assertion based and used for for checking the top level connectivity on an SoC. This takes very less time in comparision to running a testcase. It also finds the connectivity problems very easily. Is SoC is complex, then in IFV ready made scripts are used which can generate and check assertions very effectively.

 

[badrino]

thanks Vikas for your help,
if i understood correctly (according to your answer + some search in inetrnet), when RTL design is ready, it's the functional verification (static + dynamic) which is done at first to ba sure that rtl match correcty with spec, whereas when doing synthese and post loyout simul, its the formal verification which is done at this level, so formal verification come always after functional verification?? can you please confirm this ?

 

[vikas gupta]

Hi Badrino,
I have been in industry for little over 1 year and I have done SoC verification during this time which makes me a relatively a newcomer. So, I can tell you only what I have encountered. In verification (dynamic ) you have to check whether the design is working properly, so when the RTL is ready and there is a testbench release.....we have to write testcases to check different specifications or/and functionalities of Blocks/IP's like UART/I2C/USB/DDR, etc on a system level. If there are any bugs we report it to design team so that appropriate changes in design can be done then again new netlist is relaesed. This process goes on till everything is fine. This is done first on rtl ( dode) and then on GATE level. Here we actually simulate by dynamically applying different inputs and doing different configurations by writing in different registers...consequently different outputs (signals) change dynamically throughout the time till testcase is running. Offcourse there are different phases in test case when we apply these...not right from the word go. You can therefore see the values of different signals, buses, etc during the time when the test case starts till when the testcase ends. That is why it is called dynamic. We can from the waveform of different signals see where and when the problem/error occured and which signal/signals had diffferent value from what they should have and infer what was wrong. Hope this clarifies what is dynamic verification.
I have done formal verification only in one of the projects out all that I have worked on and formal verification is applied in a limited in my company. So further explanation is very specific and you have to see other sources for better explanation. In my comapany, we used a tool called IFV from Cadence which was used for formal verification. When I searched on net after seeing your reply I can clearly there are other types of formal verification apart from this. We apply it in a limited way. Using this we verify the rtl on top level (that it is not concerned with design at block level as the SoC is a very big design and if we apply it to check whole SoC the the tool will just hang.....so this is specific to my case) . Later I did find out that they were planning (only planning or figuring out how) to use it at block level but the tool cannot be used for the whole SoC as the design is very large. So, ( I am taking a guess) if the design is small perhaps it can be applied to whole netlist.
Now let me describe what we did with it. Firstly we used assertions ( so we used assertion based formal verification..there are other types as pointed by me earlier). Using assertions, we checked mainly toplevel design i.e we did not go into the functioning of different blocks like UART/I2C/USB,etc...so regarding your question formal verification was being done simultaneously after 1 or 2 release of netlist or testbench. Here, we first dumped the whole SoC design in the tool and then filled information upto what level / hierarchy we want the tool to check and then using readymade scripts we first generate assertions. Lets say we have a single bit buffer with input as X and output as Y and enable is E. So, using assertions Y will be 1 only when X is one for sometime and during this period E is one for some time similarly you can verify the truth table for Y by considering different combinations. Then we run the tool and it checks all the assertions. If some assertions turn False...i.e. it is an error..it means there is something wrong in design and we have to see which signal and at what level and which functionality is the problem. Mostly, it is result of wrong connectivity and we can correct the design very quickly. So, running and verifying assertions is very very fast in comparing to actually running the testcase. You have to find out more about running and verifying assertions from other sources. But the advantage is most of the the design issues related to connectivity have been take care of so early which might have affected various verification users later and this results in huge time saving.
I am giving an example to illustrate my point. For ex lets say in an SoC muxing of UART is wrong and their are other cases also of different IP's/ Blocks. Then if we actually right a testcase and run it then it will take a lot of time till the whole test case is run..as there are PLL's to be locked and system ready has to be there..then their is configuration of different registers and the error will only be detected when we check for a value in a register...worse lets say the receiver may have to wait endlessly for the transmitter side to actually send the data and test case will keep running until time out occurs. This leads to lot of time wastage. This situation is avoided by IFV.
One more thing, ( I am not sure about this) we use IFV simultanously while we are doing (dynamic) verification may be because we have to complete the project as fast as we can and whole team can't be kept waiting till IFV completes its job ...verify it yourself. If there are other types of dynamic verification...I don't have any idea what they are.

Hope it clears some doubts.