Hi
I’m wondering which approach is better to verify a design functionality, doing simulations using a SV or UVM testbench, or otherwise performing a formal verification of the design? I don’t know much about formal verification, but if I understand correctly, it is much easier to setup and it can cover the corner cases more easily and more thoroughly. If that is the case, why should anyone take the trouble and develop an SV or UVM testbench and try so hard to maximize functional coverage? I think I’m missing some important point here, I would be grateful if I get some guidance on the subject.
Thanks
In reply to Farhad:
In my personal opinion having a SV uvm testbench simplifies the point to point test scenario which would take longer and much more effort with formale due to the lots of assumes to be used. Give you a practical example: formal register verification is amazing which helps you to quickly verify power on reset value of many registers in 1 run. Nevertheless if you wanna just test 1 reg (a special one for instance whit some logic around it ) formal is still capable but not faster and effortless as the simple uvm test.
Hence a sv or uvm environment would still be required to test out directly some scenarios (just gave you one example) without the heavy duty of exploring all the possibilities like formal does. Anyway formal has been steadily becoming more adopted in my opinion and easy to setup.
Regards
In reply to Farhad:
Each verification technology has its strengths and weaknesses. When talking about formal you hear the term state space used. This is primarily based on the number of state bits in the design. Obviously this is a large number. Briefly, think of simulation as a depth first methodology where you can carve very targeted/specific paths through the state space, ideally tied to a testplan. The downside is it is impossible to cover every scenario so corner case bugs can slip through. Simulation of course is vector based requiring a testbench of some sort (directed, UVM etc.)
Think of formal as a breadth first verification. It is using mathematical methods (no vectors) hence for every cycle of analysis it is covering all input and next state possibilities. You do need to write a property to make use of formal techniques. The great thing about this is it can find the corner case bugs you might miss in simulation. The down side is the analysis is exponential in nature so the algorithms either bog down or you run out of memory potentially on the machine you are running on (not as common for most of today’s servers)
Ideally you use both where each is strong. Chip/SoC level requires simulation/emulation, block level you can leverage formal generally speaking.
There are a number of excellent classes in Verification Academy. Maybe start with the “Getting started with formal verification” course.
In reply to Farhad:
another difference is that with SV/UVM, you could modeling/checking the DUT at transaction level. And the reason for going with transaction level modeling is because things gets too complicated at lower level, we want to abstract out the information we are not interested.
while with formal/SVA, you normally focus on the temporal property of the DUT. This means it’s really hard to do formal at transactional level. you prob do not want to try formal at subsystem/system level verification I guess.
Thank you very much for your complete answers rsignori, Mark Eslinger_2 and Jeff_Li_90.