What is the difference between formal verification and functional verification ?

[rahul.achates]

Hi

People more talking about the formal verification , it has gone to advanced level. Can someone help me on that. I am curious to know difference between formal verification and functional verification.

 

[ro9ty]

Functional Verification is writing testbench and test cases to verify what are the different possible cases that a design code could be subjected to and whether it will work as expected.
Formal equivalence and Logic equivalence check are the same thing. Here you verify that after synthesis/placement (basically optimization) whether the tool has maintained the same logic or not.

 

[rahul.achates]

do you know how logic equivalence check happen in tool ? how will a tool knows what functionality I have implemented ?

 

[ro9ty]

Let us assume that you are doing a netlist to netlist LEC. So, in Netlist 1 you have a signal coming in from a port, going through 3 flops and finally emerging from an output port.
In Netlist 2 it gets optimized and the tool somehow finds that one of the inputs to one of the flops is tied to 0 value. It gets optimized and hence deleted. When these two signals are compared a register (key point) is missing from the design and the tool will see this. Hence it shouts uncompared.

How the tool understands the logic :-
Every netlist or RTL that you provide to the LEC tool it has a capability to break it, analyze and elaborate it just like a synthesis tool but it will break and assemble the design according to the key points i.e one of these [Primary inputs, PO DFF, Latches, Black boxes, Z gates and cut gates] because it will make logic cones starting with one of these and ending with the other. Example : Starting from port A and ending at a Flip-Flop. This way it will break the entire design for both the golden and the revised netlist. Then the comparison starts, where the tool checks the logic with every posible combination. Ex: Between two flops if you have an AND and a NAND logic then it will pass stream of 1 and 0 to see if for each combination the output value for that particular logic cone in gol and rev is same or not.

LEC is an extensive and interesting topic. Consult Cadence support site to learn more.

Ro9ty

 

[rahul.achates]

Thanks ro9ty ..