Dramatically Reduces ASIC Verification Time Compares two designs - RTL to gate for synthesis and ECOs - Gate to gate for layout spins - RTL to RTL for language conversion Highest capacity tool - Verifies multi-million gate ASIC ’s as one Fastest route to correct design - Exact location of errors - Tests fixes within the verification session Where to Use FormalPro : FormalPro is a Regression Testing Tool That verifies all stages of gate-level implementation of a design From synthesis through to tape out Benefits GUI for design entry and initial debug Command line mode for regression testing Constraint language and TCL scripting Incremental Verification Recompile only design that has changed Restart at intermediate points