Help: A Formality problem

[janova]

formality problem

I'm using Formality to verify the equivalence between RTL and Netlist.
The top module failed because of some failing points in a sub-module ABC.
However, the sub-module ABC can be successfully verified when run singly.
In the top level netlist, the netlist of ABC just be read in and linked, and have set set_dont_touch property in DesignCompiler.

Have anyone experienced this? Any suggestion about the debugging method?
Tks a lot !

 

[archillios]

formality set_black_box edaboard

set_dont_touch in DC has no effect in Formality, you can set_dont_verify in Formality, or set_black_box.