Provably-correct hardware compilation tools based on pass separation techniques - McKeever, S; Luk, W (FORMAL ASPECTS OF COMPUTING, 2006)