Incisive Formal Verifier

Hi all,

 Blackboxing a module in ifv will allow tool to drive different possible values on the pins of that module. So is it necessary for assertions to pass for all the values that are driven on that pin or any one will suffice? 

Thank You.