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

7.1i Formality/Conformal/eCheck、Virtex-4 - DCM 自動較正ロジックが含まれたデザインをフォーマル検証ツールで検証する方法

説明

キーワード : Synopsys, Cadence, prover, フォーマル検証

重要度 : 標準

概要 :
DCM クロックが停止したマクロを含むデザインでフォーマル検証を正しく実行させるには、どうしたら良いですか。

ソリューション

1

Synopsys Formality での回避策 :

Synopsys 社が提供している TCL スクリプトを使用すると、デザインのフォーマル検証を正しく実行できます。 ファイルは、次のサイトからダウンロードできます。
http://www.xilinx.com/txpatches/pub/utilities/3rdparty/formality_dcm_autocalib_workaround.tar.gz

ファイルをディレクトリで解凍します。
>gunzip formality_dcm_autocalib_workaround.tar.gz
>tar -xvf formality_dcm_autocalib_workaround.tar.

TCL スクリプトを抽出したら、Formality スクリプト ファイルに次の文を追加してスクリプトを実行します。

source setConstant.tcl

次は、スクリプト ファイルの例です。

read_verilog -r auto_calib_ecn_postngd.v -vcs "-y $env(XILINX)/verilog/formality/simprims +libext+.v"
set_top -auto

read_verilog -i auto_calib_ecn_postpar.v -vcs "-y $env(XILINX)/verilog/formality/simprims +libext+.v"
set_top -auto

source setConstant.tcl

verify

Formality を使用した検証方法については、Synopsys 社にお問い合わせください。

電話番号 : 1-800-245-8005 (米国内フリー ダイアル)
電子メール : support_center@synopsys.com
サポート Web サイト : www.synopsys.co.jp/
FTP サイト : ftp.synopsys.com

2

Cadence Conformal での回避策 :

Cadence 社が提供している TCL スクリプトを使用すると、デザインのフォーマル検証を正しく実行できます。 ファイルは、次のサイトからダウンロードできます。
http://www.xilinx.com/txpatches/pub/utilities/3rdparty/conformal_dcm_autocalib_workaround.tar.gz

ファイルをディレクトリで解凍します。
>gunzip conformal_auto_calib_workaround.tar.gz
>tar -xvf conformal_auto_calib_workaround.tar

TCL スクリプトを抽出したら、Conformal スクリプト ファイルに次の文を追加してスクリプトを実行します。

source cfm_set_constraints.tcl

次に、スクリプト ファイルの例を示します。

set log file lec.log -replace
set undriven signal 0 -both

read design -f $XILINX/verilog/verplex/verilog.vc nbti_ecn_postngd.v -gol
read design -f $XILINX/verilog/verplex/verilog.vc nbti_ecn_postpar.v DCM_STANDBY_ecn.v -rev

tclmode
source ../tcl/cfm_set_constraints.tcl
set_constraints
vpxmode

set sys mode lec
add compare point -all
compare
usage

Conformal を使用した検証方法については、Cadence 社にお問い合わせください。

電話番号 : 1-877-237-4911 (米国内フリー ダイアル)
電子メール : support@cadence.com
サポート Web サイト : sourcelink.cadence.com/JGSL
Web サイト : www.cadence.co.jp
FTP サイト : ftp.cadence.com

3

Prover eCheck での回避策 :

eCheck を使用すると、まず DCM クロックが停止したマクロでエラーが発生します。

ブラック ボックス X_DCM_ADV のインスタンスに対して実行されたゲート間の比較でエラーが発生した場合、このブラック ボックスの RST 入力ピンのカウンタ例を開いてください。

カウンタ例のファンインにあるインプリメンテーション デザイン レジスタの名前を識別します。 たとえば、次のような名前です。
physical_group_locked_OBUF/dcminst1/q/f1/q

Prover eCheck の TCL スクリプトで、次の制約を追加し、上記のレジスタに 0 を設定してください。
constraint -add -reg -custom physical_group_clk_dcmo/dcminst1/q/f1/q 0 impl

比較をもう一度実行し、エラーが発生するブラック ボックス X_DCM_ADV のインスタンスがほかにないかを確認します。

eCheck を使用した検証方法については、Prover Technologies 社にお問い合わせください。

電話番号 : +1-650-722-2750
ファックス : +1-650-347-6284
電子メール : echeck-support@prover.com
Web サイト : www.prover.com
AR# 21484
日付 12/15/2012
ステータス アクティブ
種類 一般
このページをブックマークに追加