Kiran Bulusu’s Blog

Folks who wants to read my part I of the formal verification series , click this link :

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

I wont be elaborating much on points when they are self explanatory and some have been already covered in part I ( setting up the FV env section )

1. Check for unmapped points. Naming rules/mapping issues. Unless you all Seq elements and Black Box I/O’s in Reference and Implementation has been matched, the formal verif results are meaningless. Some tools report mapping failures when they see  some objects in Reference (Golden) doesnt exists on Implementation (revised). This is one exception to this as it is quite possible that synthesis tool might have optimized them out. But if you see that Objects in Implementation netlist doesnt exists in Reference, then it means your formal tool is doing more optimization than necessary or something is worng.

2. Blackbox (BB) issues : If there is formal failure, check if BB’s are same in both the netlists are same and number of BB should be equal.

3. Debugging using hierarchical and flat approach : When hierarchical approach lists failures, dont jump to conclusions immediately. May be the context is not propagated correctly and hence the tool propagated wrong values and hence failure. Do a flat level verification either at the same failing module level or one level up the hierarchy.

4. Spare Cells :check for spare cells getting removed .

5. Port information: check if ports are getting removed like DFT test mode etc

6. Overlay/Feed Throughs : If you are loading your Implementation (Revised) netlist from your physical synthesis flow, check if there are any ovelay cells or feed throughs . Normally these dont exist in the original (RTL) or logic synthesis netlist. These are added by the physical synthesis tools during the top-down chip/block routing or integration stage. Overlay cells change the netlist by adding a hierarchy while logically/functionally the design is still same.

7. Cloning during CTS : Again in physical synthesis flow, during CTS, the place and route tool might have cloned some ports ( for example reset pin/port)  and you need to tell your formal tool somehow that the cloned reset port is just an alias of original reset port .

8. Clock Gate Cloning :Another common issue is, the clock gates are cloned in physical synthesis flow and so you need to tell your FV tool about all the different clock-gates being used .

9. Power Connectivity : Some synthesis tools dont write power connectivity information of non standard cells by default , for example analog power information ( like AVDD or AVSS etc) and sometimes they write empty power connections for all blocks . This can cause formal failures tool.

Lastly , FAILURES are different from UNSOLVED points. FAILURES means the netlists differ and UNSOLVED means they are certain datapath elements like multipliers or for example ECC etc which are not verified. They can be still be verified if you can afford to wait for real looooooong times ( perhaps years..decades )

I was recently talking to couple of design engineers at various companies and most of them want to have push button RTL-Placed Gates or RTL-GDSII flows. Though this sounds like a reasonable expectation, but in reality as many experienced designers know, this is often not practical. The issue here is right set of expectations.

We can develop a push button flow if we have a good design methodology with reasonable and manageable expectations. A designer or CAD design engineer need to understand that there are certain things they have to do like setting the synthesis env or constraints, providing good quality timing constraints etc . I have seen in numerous cases where the designers blame the tool for poor timing results , but when analyzed, they have a messed up their timing constraints or has specified timing exceptions where not necessary . Simply put, they might have over constrained their designs. While it is reasonable to expect the tool do a good job for a classical physical synthesis problems where the designers has very little to do, but it is not for a logic synthesis issues where a lot depends on the quality of RTL, constraints , DFT methodology etc.

Each chip is unique ( I’m not talking about the revisions of the same chip here) and the requirments differe from chip to chip in terms of complexity of the design, design size, number of macros used , number and freq of clock domains, DFT logic ( along with JTAG etc) , clock latencies, skew balancing ,cross-talk etc . Clearly OOTB Flow ( out of the tool box) might not always deliver the best QOR (ofcourse it means its a enhancement time for R&D ) and some amount of playing with different knobs/options is necessary to give the best QOR.