Formal Semantics and Proof Techniques for Optimizing VHDL Models - Kothanda Umamageswaran, Sheetanshu L. Pandey et Philip A. Wilsey