1.1.2 Let's blame logic synthesis

why does an Equivalence Checker (EC) abort?
Because the left hand (EC) does not know what the right hand (logic synthesis) is doing. In a situation where Equivalence checking is not able to prove some of the compare points right or wrong, it has the tendency to create abort points.

How deep is the rabbit hole?

Equivalence checkers solve problems like BDD isomorphism and Boolean SATisfiability. They are inherently tough problems to crack. 20-30 years of research in this area (most active since 1986 ROBDD paper!) has made life less difficult. Data path verification and sequential checking are still major challenges which the industry faces today.

The equivalence checker goes through iterations of BDD isomorphism (comparing BDD's) -> SATisfiability checking -> ATPG -> Random Simulation to generate a proof of correctness or failure. In the event that one particular algorithm is not able to solve a problem instance, the problem instance seeps through to the other solver during the comparison process. Life gets only more complex in (Sequential Logic equivalence checking) SLEC.

lets us now assume that we have some problems which take extremely long run time or tremendous amounts of computer memory for computation. In the event of not being able to solve the problem within the given memory/run time requirement and after going through the sequence of solver iterations, the equivalence checker returns an abort to make "designer's life" miserable.

This still does not prove the compare point to be right or wrong :). In this situation the best thing to do is to move forward by generating functional vectors for simulating the cone of logic under consideration. (The formal tool did help you verify 90-95% or more of your logic :)), so dont worry, be happy!

If the cone of logic ends up being pre-verified IP (like Designware components and if confidence with these components is very high)these modules can be black boxed and formal verification can still be used on the remaining cones of logic.

As designers, we can do a couple of things to make life miserable for Formal verification engineers:

1. Sharing, Merging and Expression synthesis of (data path) operators.
2. Hierarchical vs flat comparison.
3. Dont care optimization.

What can synthesis guys do the alleviate the problem?
Sacrifice QOR :)