Why the model checking technique is successful for HW verification, and failing for SW verification?

Why the model checking technique is successful for HW verification, and failing for SW verification?

• For HW verification, HW like digital circuits are easy to model checking. But for SW, SW is usually so huge, we can only apply MC for abstract model of programs. However, two obstacles there: 1. it is costly to prepare the abstract models and severe cost effectiveness 2. abstract models of programs are not any more programs.