15/08/2016
LEC vs FV
Almost every VLSI engineer will be using them to verify their design and whats the difference ?
LEC : Uses Binary design diagrams there are variants like ZBDD Zero-Suppressed Binary Decision Diagrams , FDD free binary decision diagrams, PDD parity decision diagrams etc and each one is used to specify a piece of logic in a more efficient way but these BDD a.k.a ROBDD have exponential growth for multiplier and adder circuits , it is an actual representation of boolean network if your FANIN cone of test-point is huge you will see awkward BDD
Open source tools : CUDD , PyEDA etc , you can also visualize them using Graphviz software
FV : This is an SAT-solver , which proves that both the circuits are equivalence by indirectly checking revised and golden circuit output for all input values and proves that there is no input combination of 1,0 to make both the circuits differ if there is one set of values solver will return them and engineer can debug the cause of failure ,
Open Source tools : MiniSAT , PicoSAT , CryptoSaT
More at http://edatools.blogspot.com/2016/08/tesla-fvlec.html
