Strong Induction in Hardware Model Checking