BackSpace : formal analysis for post-silicon debug