UPGRADE YOUR BROWSER

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# 16563

Synopsys Formality, Virtex-II, Virtex-II Pro, LVPECL, OBUFDS - Post-PAR verification fails on designs with registered LVPECL outputs

Description

When I verify a design that contains registered LVPECL outputs, Match and Verify fail when checking the equivalence between the RTL code and the post-PAR or post-MAP netlist. The following three scenarios can cause these failures:

1. In the Virtex-II hardware, the OBUFDS that is supposed to drive the LVPECL outputs does not have enough drive strength to drive the N side LVPECL output. To fix this, each output must be driven separately. If the LVPECL output is registered, MAP replicates the register. This is done because you might want the register to be in the IOB, and replicating the register is the only way to drive both outputs with IOB registers. This replicated register then causes Match to fail in Formality.

2. No inversion between the IOB register and the output pad. MAP moves the inversion for the N side LVPECL output from the output side of the register to the input side of the replicated register. This causes Verification to fail on the N side LVPECL output.

3. The final scenario involves resets and initial values. Since the inversion was pushed before the register, the INIT value of the replicated register must be opposite of the original register, and the resets on the replicated register must generate the opposite output of the original register. MAP handles this correctly, but if the register has both a CLEAR and a PRESET, the CLEAR always wins. So, although the CLEAR and PRESET have the opposite affect on the replicated register when asserted individually, the output of both LVPECL outputs is 0 if CLEAR and PRESET are asserted at the same time. This also causes verification errors.

Solution

Solution 1

Your design contains registered LVPECL outputs, but the register does not need to be packed into the IOB.

In this case, MAP incorrectly replicates the register since most users would pack this register into the IOB. This problem should be fixed in the Xilinx 6.1i software. Until this is fixed, see Solution 2 and 3.

This will work only in the ISE 6.1i and above release if the constraint IOB = FALSE is applied to the register in question.

Solution 2

Your design uses registered LVPECL outputs, and the register is packed into the IOB and has both a CLEAR and a PRESET.

In this case, all three scenarios described above affect the verification of your design. When both LVPECL outputs are 0 if both CLEAR and PRESET are asserted at the same time, you can add logic to your design to ensure that they are never asserted at the same time. Since the CLEAR has a higher priority, the PRESET is gated with the inverse of the CLEAR signal, as shown in the following example:

always @(CLR or PRE)

begin

NOT_CLRandPRE = ~CLR & PRE;

end

FDCPE FDCPE_dest (

.Q(q_ii),

.C(clk_bufg),

.CE(CE),

.CLR(CLR),

.D(q_i),

.PRE(NOT_CLRandPRE)

);

After you apply this design change, the logic for the replicated register is equivalent to the RTL design, but Formality still fails because the logic was moved. You can use the following assertions to specify to Formality how the logic was moved by MAP (these are the same assertions described in Solution 3):

1. Set a user match between the LVPECL register in the RTL and the two LVPECL registers in the post-PAR or post-MAP netlist, as in the following example:

set_user_match r:/WORK/top/FDCPE_dest/Q_reg i:/WORK/top/FDCPE_dest -type cell

set_user_match r:/WORK/top/FDCPE_dest/Q_reg i:/WORK/top/FDCPE_dest/N -type cell

2. Specify to Formality that the inversion for the output was pushed to the input side of the replicated register, as in the following example:

# QB is the output

# FDCPE_dest/N is the replicated register

# set_inv_push must be applied to both

set_inv_push i:/WORK/top/QB

set_inv_push i:/WORK/top/FDCPE_dest/N

NOTE: Verification is successful only if using Formality 2003.03 or later.

Solution 3

Your design uses registered LVPECL outputs and the register is packed into the IOB and has none or one reset.

Since there is none or one reset, only scenarios one and two described above affect the verification of your design. You can use the following assertions to specify in Formality how MAP moved the logic:

1. Set a user match between the LVPECL register in the RTL and the two LVPECL registers in the post-PAR or post-MAP netlist, as in the following example:

set_user_match r:/WORK/top/FDCPE_dest/Q_reg i:/WORK/top/FDCPE_dest -type cell

set_user_match r:/WORK/top/FDCPE_dest/Q_reg i:/WORK/top/FDCPE_dest/N -type cell

2. Specify in Formality that the inversion for the output was pushed to the input side of the replicated register, as in the following example:

# QB is the output

# FDCPE_dest/N is the replicated register

# set_inv_push must be applied to both

set_inv_push i:/WORK/top/QB

set_inv_push i:/WORK/top/FDCPE_dest/N

NOTE: Verification is successful only with Formality 2003.03 or later.

AR# 16563
Date Created 09/03/2007
Last Updated 12/15/2012
Status Active
Type General Article