Iam doing formal verification,Iam getting so many signals unitialized.Iam not understanding which signals we should initialize.How to know which signals we should initialize in a module.
This is not a formal only question. What does the designer or spec say about resetting the design? If you are running simulation you have the same concerns.
To initialize the design in IEV, use the tcl force commands to drive the reset signals to their appropriate values and then use the run command to run the clocks.
clock -add clk
force reset_n 0# Run the reset for 5 clocksrun 10# Load formal model with initialization state init -load -current# Display flop valuesinit -show
Hope this helps jumpstart you.
Thanks for the reply,
Its true this question was nothing related to IFV.Actually in any design we need to have some signals initialized as per design after reset process completed.
That we can do by doing signal force. These things need to be discussed with designer of particular block/module.