problems about formality constant reg

[eddsos]

formality problem

I have one register in netlist, whose data input enable is always invalid.
So, this register should be 0 after reset, which is a redundant logic.
How can i let formality know this when compare downstream logics?

 

[hawk_chenbo]

formality constant

I wonder why you don't remove this redundant register.

 

[jackson_peng]

just set constant value on the reg out, before you start verify

 

[spauls]

try synthesis again with set_case_analysis , and then do formality your problem will be olved.