Simulation and formal methods are vital and complementary components
of IBM's hardware design process. IBM Research has a long history of
innovation in hardware verification that includes high performance
hardware simulation engines as well as Boolean equivalence checking
and advanced model checking. For a comprehensive view of the
verification program in IBM Research see:
http://www.research.ibm.com/pics/verification/.
Within the Design
Automation group, there are four efforts in the area of verification:
Verification Methodology For The Blue Gene Project
Formal Design Of Hardware
High-Performance BDD Package
Software Analysis