The necessities of VLSI design by formal method lead to consider the feasibility of specifying hardware behavior using temporal logic language XYZ/E which is the basis of the CASE tool system XYZ. A microprocessor based fault tolerant computer system is described behaviorally, simulated by executing the description on XYZ system, and the intended properties have been formally verified by using the XYZ/VERI. The comparison between XYZ/E and VHDL(VHSIC hardware description language) has been made. The results have shown that XYZ/E is promising for the research of formal method for hardware design.