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