Description

Using an OBUFTDS causes the register to be duplicated, and the equivalency checking might fail.

Solution

Formality does not merge these registers automatically. The registers being merged are inverted, and the outputs of the flops feedback to the input to hold when CE is Low. 

To work around this issue, add the following to the formality script: 

set_inv $impl/\<imst_name>/N 

Additionally, the following line will need to be typed in the TCL command line as well: 

guide 

guide_reg_duplication -design EXP_OBUFDS_IFLOP -from { <inst_name> } -to { <inst_name><inst_name>\/N } 

setup 

To find the instance name <inst_name>, you must parse through the equivalency netlist written out by NetGen to find the instance names of the X_FF. This is a problem only in the post-MAP and post Place and Route equivalency netlist. 

Future releases of Formality might support this automatically.