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 - レジスタを付けた LVPECL 出力を使用したデザインで PAR 後の検証が実行できない

説明

キーワード : Synopsys, Formality, formal, verification, equivalency, checking, LVPECL, OBUFDS, fail, Virtex-II Pro, フォーマル, 検証, 等価性, チェック

レジスタを付けた LVPECL 出力を使用したデザインを検証する際に、RTL コードと PAR 後または MAP 後のネット リストの等価性チェックを行うと、Match と Verify (検証) が停止してしまいます。この問題は、次に示す 3 つの状況で発生します。

1. Virtex-II で、2 つの LVPECL 出力を駆動するはずの OBUFDS に、N 側の LVPECL 出力を駆動するだけの強度がない場合。この問題を修正するには、2 つの出力を別々に駆動する必要があります。LVPECL 出力にレジスタが付いている場合、MAP によりレジスタが複製されます。この複製は、IOB 内にレジスタを配置するために行われます。IOB レジスタが付いた出力を 2 つとも駆動するには、レジスタを複製するしか方法なないのですが、 この結果、Formality の Match で問題が発生します。

2. IOB レジスタと出力パッド間にインバータがない場合。N 側の LVPECL 出力のインバータは、レジスタの出力側から複製されたレジスタの入力側に移動されます。このため、N 側の LVPECL 出力で検証が停止してしまいます。

3. リセットと初期値。インバータはレジスタの前にプッシュされるため、複製されたレジスタの初期値はオリジナルのレジスタとは反対になり、複製されたレジスタのリセットはオリジナルのレジスタとは逆の出力を生成する必要があります。この処理は MAP で適正に行われますが、レジスタに CLEAR と PRESET があった場合、CLEAR が先に使用されます。したがって、CLEAR と PRESET が別々にアサートされた場合、複製レジスタに逆の影響を与えます。CLEAR と PRESET が同時にアサートされた場合は、LVPECL 出力は 0 のままです。このような動作により検証が停止します。

ソリューション

ソリューション 1

デザインにはレジスタ付きの LVPECL 出力が含まれますが、このレジスタは IOB にパックする必要はありません。

ユーザーは通常、このレジスタを IOB にパックするため、MAP によりレジスタが複製されてしまいます。この問題は、6.1i ソフトウェア リリースで修正される予定です。修正されるまでは、ソリューション 2 または 3 を参照してください。

このソリューションは、ISE 6.1i およびそれ以降のバージョンで、問題のレジスタに IOB 制約が FALSE に設定されている場合のみに適用されます。

ソリューション 2

デザインにレジスタ付きの LVPECL 出力が使用されます。このレジスタは IOB にパックされていて、CLEAR と PRESET が設定されています。

この場合、上記の 3 つのシナリオがデザイン検証に影響を与えます。CLEAR および PRESET を同時にアサートしたときに両方の LVPECL 出力が 0 である場合、デザインにロジックを追加して同時にアサートされないようにできます。CLEAR の方が優先順位が高いため、次のコードに示されるように、PRESET には CLEAR 信号を反転したものを使用します。

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)
);

このデザイン変更を適用した後、複製されたレジスタのロジックは RTL デザインと同じものになりますが、ロジックが移動されたため、Formality は停止します。MAP によりロジックが移動されていることを Formality に指定するため、次のアサートを使用できます (ソリューション 3 で記載したのと同じアサート)。

1. 次のように RTL の LVPECL レジスタと PAR 後または MAP 後のネットリストの 2 つの LVPECL レジスタ間でユーザー マッチを設定します。
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. 次の例のように、Formality で、出力のインバータが複製されたレジスタの入力側にプッシュされたことを指定します。
# 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

メモ : Formality 2003.03 またはそれ以降を使用すると、検証を問題なく実行できます。

ソリューション 3

デザインにレジスタ付きの LVPECL 出力を使用してこのレジスタを IOB にパックし、RESET を 0 か 1 にします。

RESET が 0 または 1 であるため、上記のシナリオ 1 または 2 のみがデザイン検証に影響を与えます。MAP でロジックがどのように移動されたかを Formality に指定するため、次のようなアサートを使用します。

1. 次の例のように、RTL の LVPECL レジスタと PAR 後または MAP 後のネットリストの 2 つの LVPECL レジスタ間でユーザー マッチを設定します。
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. 次の例のように、Formality で、出力のインバータが複製されたレジスタの入力側にプッシュされたことを指定します。
# 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

メモ : Formality 2003.03 またはそれ以降を使用すると、検証は問題なく実行できます。

AR# 16563
日付 12/15/2012
ステータス アクティブ
種類 一般
このページをブックマークに追加