Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification