the verification idea

what i know is: PSL properties are written and then verified by simulation in modelsim for instance, then accordingly, design can be changed to meet specs correctly

but then, tools like solidify and FoCs and so on...why are they used???
is it because not all assertions or assumptions are verified by simulation??
is it the role of formal verification tools to verify instead of simulation ???
are properties synthesized or not???
do they stop at the simulation level???
when to use simulation and when to use formal verification to verify???

there is just something missing which i don't get???

what are online monitors too ???

can someone clear me up on the flow of verification and its tools
cause i'm getting kind of messed up and confused here

Thanks in advance,
Salma

Salma,
just to clear some things up, ABV (assertion based verification) is based on PSL in which you define the conditions when certain states are valid and in how many cycle times. For example, you can say that when a state changes from A to B after 5 cycles and you define a property for that through PSL language. Now, when you run simulator, it inteprets the PSL property and checks for the condition. If the state changes from A to B in less than 5 cycles, then an error/assertion is raised. You do the simulations ( lets call them functional RTL simulations ) even before you do your logic synthesis. Once the RTL simulations pass, you will do your synthesis and then you will run formal verification ( equivalence checking ) to make sure your gate level matches the RTL you have written. Synthesis tool ignore the PSL properties.

you can check more about formal verification in my blog here

https://www.srikiran.net/blog/2007/01/22/debugging-formal-verification-fv-problems-fv-primer/

Solidfy and other tools use PSL properties to check for the error conditions and flag them . They also do clock domain crossing issues etc. Formal tools like Synopsys Formality, or Cadence Verplex/Conformal or Magma's QuartzFormal all use formal verification ( equivalence checking ) to prove that RTL and synthesis results match.

People still do gate level simualtions (post synthesis) for timing ( SDF backannotation ), to check for timing exceptions ( like false paths ) etc.

I hope this helps.

salma ali bakr said:

what i know is: PSL properties are written and then verified by simulation in modelsim for instance, then accordingly, design can be changed to meet specs correctly

but then, tools like solidify and FoCs and so on...why are they used???
is it because not all assertions or assumptions are verified by simulation??
is it the role of formal verification tools to verify instead of simulation ???
are properties synthesized or not???
do they stop at the simulation level???
when to use simulation and when to use formal verification to verify???

there is just something missing which i don't get???

what are online monitors too ???

can someone clear me up on the flow of verification and its tools
cause i'm getting kind of messed up and confused here

Thanks in advance,
Salma

Click to expand...

so if we look at different types of formal verification

we can say that model checking (by PSL for instance) is before synthesis (RTL level only) and the properties are verified using simulation

and that equivalence checking is after synthesis (between gate netlist and RTL)
to see if the circuit was correctly synthesized or not

so they are both formal verification methods
but in different levels of abstractions in the design flow

thanks alot,
Salma

well yeah u can say that in more abstract sense and as long as you understand the difference between model checking and equiavlence checking...

salma ali bakr said:

so if we look at different types of formal verification

we can say that model checking (by PSL for instance) is before synthesis (RTL level only) and the properties are verified using simulation

and that equivalence checking is after synthesis (between gate netlist and RTL)
to see if the circuit was correctly synthesized or not

so they are both formal verification methods
but in different levels of abstractions in the design flow

thanks alot,
Salma

Click to expand...

What if I want to be a design verification engineer?
What exactly should i know?
Do I have to go deeply starting from CTL, LTL, etc.
What basics should i have, and regarding the tools, which are the market standards?

thanks alot in advance, and your blog is really great

Salma