During hardware design process, an "English" description of hardware
is refined into a formal specification model and a collection of
temporal assertions that the formal logic model must satisfy. This
specification model is further refined into an implementation model
to meet timing, area and power requirements. Therefore, in order to
prove the "correctness" of the implementation model, one proves that
the specification model satisfies the temporal logic assertions and
that the implementation and specification models are "functionally"
equivalent.

I will give a brief overview of some of the concepts of hardware
equivalence developed in the literature, and I will report on work at
Intel's Formal Technologies group in Haifa on designing
compositional, formal verification methods to cope with the
verification complexity of Intel designs.

See papers in <a href="FMCAD06.pdf">FMCAD06</a> and <a
href="iccad04.pdf">ICCAD04</a>.