Features

Supports all sequential optimizations in FPGA synthesis, including stuck-at (constant) registers, register duplication and merging, net/instance name modifications, FSM optimizations, retiming and pipelining
Works with established FPGA synthesis tools, such as Synplicity© Synplify Pro©
Supports all major FPGA product families from Altera and Xilinx, for both post-synthesis netlists and post-place-and-route netlists:
- Altera : Stratix, Stratix II, Stratix GX, Stratix II GX, Stratix III, Cyclone
- Xilinx: Virtex-4, Virtex-II, Virtex E, Spartan 3, Spartan-II
Verifies flat netlists and imposes no restrictions on netlist size
Deploys a high degree of automation and simple scripting to accomplish complex tasks
Eliminates need for synthesis side files such as 'Verification Interchange Format' (.vif)
Integrates with the design team's existing FPGA design flow 'as is'
Focuses debug with logic cone extraction and highlighting
Automatically generates a comprehensive set of RTL consistency checks and proves then exhaustively:

Synthesis full_case	Division by zero	Function without return
Synthesis parallel_case	Negative divisor, exponent or remainder	Array boundary violations
Bus contention	Don't care and X assignment	Range overflow
Bus floating	Read/write, write/write race conditions	Stuck-at
Initialization errors	Dead code	User defined assertions