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:

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 ( by searching for the keywords "xilinx mapper".
AR# 13052
Date 10/01/2008
Status Archive
Type General Article
People Also Viewed