Formality problem: top/sub module issue

[valxiao]

fomality problem

hi,all guys,
i encounter problem with formality.

A is top module
B,C,D is sub module

when i run formality to only B module alone, B is set as top module,and no failing with result

but when i run formality to all module and A is set as top module,and have failing register in B module
and this unmatch register in B module have no input from other modules.
why have this result?hope your help,thanks!!

 

[stevepre]

Re: fomality problem

check the constraint.

for example, when you do formal for B alone, you set the scan enable signal to 0. But when you do A+B+...., you forgot the set the scan enable to 0.

The above is just one example that could cause the problem. Your case might be different. But just double check the constraint to see if everything propagates from Top to bottom well.

 

[papertiger]

fomality problem

it looks like a real error.
floating input is not allowed in IC

 

[zyphor]

Re: fomality problem

You must pay attention to the constant register that be removed by DC. The removed registers may cause many failing points, but in the module level it is easy for the tool to analysis RTL code and no error occurs

 

[jitendra]

Re: fomality problem

Hi,
You can run Formal on Top module A with B as black box.
If this is clean and you have already checked module B, I think this is fine. Error can be because of some pin constraints for instantiating module B in top module A.

Regards,
Jitendra

 

[foster_cn]

fomality problem

additionally, you may need to look into the B module to see the umatch register logic.

 

[patrickli]

Re: fomality problem

you can use hier-flow to do formal.

 

[archillios]

fomality problem

i think the gui debug utility of formality can help you to focus on the error cause.