We have detected your current browser version is not the latest one. Xilinx.com uses the latest web technologies to bring you the best online experience possible. Please upgrade to a Xilinx.com supported browser:Chrome, Firefox, Internet Explorer 11, Safari. Thank you!

AR# 13052

Synopsys Formality - Formality does not recognize registers with constant inputs


Keywords: Synopsys, Formality, Formal, Verification, MAP, registers, constant, optimization

Urgency: Standard

General Description:
MAP optimizes registers with a constant input (VCC or GND). Therefore, when the RTL design is compared to the post-PAR design, Formality is unable to compare these points.


A work-around to this problem is provided via a tactical patch available from the Xilinx FTP site at: http://www.xilinx.com/txpatches/pub/swhelp/synopsys/fm_const_reg.zip

This file contains scripts that will parse the design netlist and create Synopsys Formality constraints, instructing Formality to correctly handle registers with constant inputs. The usage for the script is provided in the README provided in the patch zip file.

Synopsys also provides a work-around for this problem, which is documented in Solv-Net article "Formality-94.htm". This can be found on the SolvNet online database (http://solvnet.synopsys.com) by searching for the keywords "xilinx mapper".
AR# 13052
Date Created 08/29/2007
Last Updated 10/01/2008
Status Archive
Type General Article