9.6 Advanced research 561 ` ð x ^ :x Þ _ ð x ^ ð y ¼ ? Þ Þ _ ð ð > ¼ y Þ ^ :x Þ _ ð ð > ¼ y Þ ^ ð y ¼ ? Þ Þ ` ð ? Þ _ ð x ^ ð y ¼ ? Þ Þ _ ð ð > ¼ y Þ ^ :x Þ ð ? Þ ` ð x ^ ð y ¼ ? Þ Þ _ ð ð > ¼ y Þ ^ :x Þ f apply Boolean simplification ` y ¼ ð :x Þ f if x ¼ > ) ð y ¼ ? Þ and if x ¼ ? ) ð y ¼ > Þ g ` IMPL ð x; y Þ ) SPEC ð x; y Þ g Q.E.D. Theorem proving has been successfully applied to the verification of hardware designs, such as the TAMARACK microprocessor [Joyce 1986] and the Viper microprocessor [Cohn 1988]. Its strength is its ability to support the expressive- ness of higher order logics, to relate circuit behaviors at different levels of abstraction [Melham 1988], and to provide many effective reasoning utilities. Moreover, the design hierarchy and regularity can be exploited by theorem pro- vers, which enable users to be in full control of the verification process. Higher order logics can specify and verify generic and parameterized hardware designs.