Synopsys also offers VC Formal, a solution that includes a comprehensive set of formal applications (Apps), including Property Verification (FPV), Automatic Extracted Properties (AEP), Coverage Analyzer (FCA), Connectivity Checking (CC), Sequential Equivalence Checking (SEQ), Register Verification (FRV), X-Propagation Verification (FXP), Testbench Analyzer (FTA), Regression Mode Accelerator (RMA), Datapath Validation (DPV), Functional Safety (FuSa) and a portfolio of Assertion IPs (AIP) for verification of standard bus protocols.
Lastly, Synopsys offers ESP, which is a Custom Design Formal Equivalence Checking Based on Symbolic Simulation. ESP is a formal equivalence checking tool commonly used for full functional verification of custom designs such as embedded memories, custom macros, standard cells and I/O cell libraries. It is used to ensure that two design representations are functionally equivalent. These designs maybe represented as Verilog Behavioral model, RTL, Gate, Switch or SPICE or .db netlist view.