Hi, In my design there are say two signals apart from other signals. req_val, req_cntl. The req_cntl is only valid if the req_val is asserted or say high. For some assertion say I don't want req_val to get asserted. Hence I constrain it to 0 (low). So does it make sense to leave req_cntl unconstrained especially if the width of req_cntl is high(say 5). Or to be specific leaving req_cntl unconstrained, will IFV try to explore the assertions for the different values of req_cntl (i.e. 2 ** 5) values?thanks,Rajendra
Hi Rajendra,Yes, IFV will consider every possible value for any input or undriven net, i.e. 2**5 different values for req_cntl.Regards,Joerg.
thanks Joerge. So you mean better constrain req_cntl as well, don't you?
Hi,No. You say "The req_cntl is only valid if the req_val is asserted", so if it is invalid it should not matter what value you see on req_cntl, since your design should not consume it. I would leave it unconstrained.Joerg.
Hi Joerge, You are correct my design will not consume it. However IFV tool will unnecessarily try these redundant 2**5 possibilities for converging to proof of the property. In short if IFV tries 2000 different possibilities for design then it will try 2000 * (2**5) possibilities because of these false scenarios which anyway will not affect the verification. Am I correct? And if the design is complex enough then the properties that would have converged with constrained req_cntl may not converge to any proof at all.thanks,Rajendra
Hi Rajendra,no, formal algorithms do not work that way. Leaving req_cntl unconstrained makes it to a "don't care", which is an easier to satisfy requirement for the tool than an explicit constraint on the same signal. And it does not do 2**5 operations, but only one which considers 2**5 values.Having said that, constant pin constraints can lead to removal of logic, which can improve performance in some cases as well.Joerg.