ality使用指南.ppt

1、Formality 使用指南,檢查RTL與GATE網(wǎng)表 檢查GATE網(wǎng)表和插入掃描鏈的GATE網(wǎng)表 檢查帶有掃描鏈和JTAG鏈的GATE網(wǎng)表和插入掃描鏈的GATE網(wǎng)表,提 綱,說 明,FiFo的Tutorial目錄下包含以下幾個子目錄： Rtl： fifo的RTL源代碼；包含fifo.v, gray_counter.v, push_ctrl.v, gray2bin.v, pop_ctrl.v, rs_flop.v。 Lib：門級網(wǎng)表需要的技術庫；包含lsi_10k.db。 Gate：綜合的門級網(wǎng)表；包含fifo.vg 和fifo_mod.vg。 Gate_with_scan：插入掃描鏈的門級網(wǎng)

2、表； 包含fifo_with_scan.v。 Gate_with_scan_jtag：帶有掃描鏈和JTAG鏈的門級網(wǎng)表； 包含fifo_with_scan_jtag.v。,一.檢查RTL與GATE網(wǎng)表,RTL源代碼：fifo.v 門級網(wǎng)表： fifo.vg 檢查文件fifo.v和門級網(wǎng)表fifo.vg的功能一致性 設置RTL源代碼fifo.v為reference design 設置門級網(wǎng)表fifo.vg為Implementation design,（一）圖形用戶界面進行形式驗證,在UNXI提示符下進入tutorial目錄：輸入fm（或formality）。,1.設置reference desi

3、gn,點擊formality圖形界面的reference按鈕，進入Read Design File 點擊Verilog按鈕，出現(xiàn)添加Verilog文件的對話框。如下圖：,1.1讀取源文件,在對話框中選擇：Rtl目錄下的fifo.v文件，點擊Open按鈕,打開fifo.v源代碼。如圖：,1.2設置搜索目錄,點擊option按鈕，出現(xiàn)set verilog read option對話框, 選擇Variable,在DesingWare root directory(hdlin_dwroot)出輸入：echo $SYNOPSYS 或Design Compiler的安裝目錄(本工作站的目錄為/opt/t

4、ools/synopsys)，如下圖：,1.3設置搜索目錄,在Set verilog read option對話框中的VCS Style Option中選擇Library Directory(-y), 在Enter Diectory Name處瀏覽選擇rtl目錄 然后點擊add按鈕添加查找目錄rtl。,選擇Library Extension(-libext)， 在Enter File Extension處填上后綴名.v， 然后點擊add按鈕添加， 點擊OK按鈕。,1.4加載源文件,然后點擊LOAD FILES按鈕，加載源文件fifo.v，如下圖：,1.5設置fifo為reference的頂層,

5、在點擊Set Top Design按鈕，出現(xiàn)下圖。,在choose a library 中選擇WORK， 在choose a design中選擇fifo（頂層設計的模塊名） 在Set and link the top design中點擊Set Top，出現(xiàn)下圖 同時在Reference按鈕上出現(xiàn)綠色的對號符：,2.設置Implementation Design,點擊Implement按鈕，在Read Design Files 中點擊Verilog，出現(xiàn)Add verilog files對話框， 選擇gate目錄下的verlog網(wǎng)表文件fifo.vg， 點擊Load Files加載網(wǎng)表文件fif

6、o.vg，,2.1加載Technology library,選擇Read DB Libraries按鈕，點擊DB按鈕，出現(xiàn)Add DB Files對話框 選擇lib目錄下的lsi_10k.db庫文件，（確保Read as share library被選中）點擊LOAD Files，加載庫文件。,選擇Set Top Design,在Choose a library中選擇WORK (Design Library), 在Choose a design中選擇頂層模塊名fifo， 點擊Set Top按鈕。此時在Implementation出現(xiàn)綠色的對號符。,3.設置環(huán)境(Setup),在這一步主要是設置

7、常量，比如對應一些增加了SCAN掃描鏈和JTAG鏈的設計，需要設置一些常量，使這些SCAN和JTAG等功能的禁止。 由于fifo.v 是源代碼，fifo.vg只是綜合的源代碼，沒有添加SCAN和JTAG鏈。故可以省略這一步,4.Match,檢查reference design 和 Implemention design的比較點是否匹配 點擊Match按鈕，選擇Run Matching按鈕，進行匹配檢查。 出現(xiàn)下圖結(jié)果：沒有不匹配的比較點，可以進入下一步。,5.Verify,點擊OK鍵，完成?，F(xiàn)在你已經(jīng)準備好，可以進行fifo.v和fifo.vg功能是否一致。 選擇Verify按鈕，點擊Veri

8、fy All，進行形式驗證。 驗證結(jié)束，結(jié)果出現(xiàn)“Verify”fail的對話框，提示兩種功能不一致。,6. Debug,由于驗證失敗，系統(tǒng)直接進入DEBUG工作區(qū)。在Failing Points的報告工作區(qū)里顯示兩設計的出不一致的比較點 在Failing Points的報告工作區(qū)內(nèi)點擊鼠標右鍵，選擇Show All Cone Size ,在Size欄里顯示每個compar point所包含的cell的數(shù)目 一般調(diào)試是從cell數(shù)目最小的compare point開始。在這里我們從第一個compare point開始。 選擇r:/WORK/fifo/push_logic/full_flag/q

9、_out_rego, 擊鼠標右鍵，選擇菜單中的view Logic Cones，出現(xiàn)Logic Cones View窗口。,在這個新窗口里顯示的是reference design 和Imeplemention design的原理圖， 觀看這個原理圖我們發(fā)現(xiàn)在Implementation的CLK網(wǎng)線是用紅色標識的 在logic cone view中，用紅色標識的net網(wǎng)線是表示錯誤的 我們觀察發(fā)現(xiàn)在reference design的CLK中表示的logic值為0，而Imeplemention design的CLK中表示的logic值為1。為了找出CLK net值不同的原因，分別選擇referen

10、ce design和Imeplemention design的CLK網(wǎng)線，選擇右鍵菜單里的Isolate Subcone命令，出現(xiàn)下圖。,在圖中可以看出在Imeplemention design中驅(qū)動CLK的邏輯里多了一個反相器，這有可能是綜合工具為了滿足hold-time的要求而增加的反相器。 我們可以修改fifo.vg網(wǎng)表文件和重新綜合一個網(wǎng)表文件，來修改這個錯誤。在gate目錄下有一個fifo_mod.vg文件是修改后的網(wǎng)表文件。 關閉Logic cone View,重新用fifo_mod.vg作為Implementation design。 選擇Implementation，點擊Rea

11、d Design Files中的Verilog，點擊yes來移除當前的Implementation Design設計（fifo.vg）。重新選擇fifo_mod.vg，點擊Load files，加載文件。 Set top Design,選擇WORK和fifo,同樣，跳過Setup 點擊Match,選擇Run Matching，運行完后出現(xiàn)下圖：,點擊Verify，選擇Verify all，運行完出現(xiàn)下圖，提示“Verification Successded!”,點擊OK后，出現(xiàn)下圖，顯示所有compare point都pass。 到此，完成形式驗證。,清理工作,選擇工具欄中的remove re

12、ference 和remove Implementation按鈕，移除reference design 和Implementation design 在formality的命令行輸入：remove_library all命令移除technology library:lsi_10k.db。,（二）命令行方式進行形式驗證,在上一節(jié)不退出formality圖形界面，在formality的命令欄中輸入：history fifo_rtl_gate.fms,生成腳本文件fifo_rtl_gate.fms 退出formality圖形界面,fifo_rtl_gate.fms的內(nèi)容,set hdlin_dwro

13、ot /opt/tools/synopsys_2003.06 read_verilog -container r -libname WORK -vcs -y /home/user/tutorial/rtl/ +libext+.v -01 /home/user/tutorial/rtl/fifo.v set_top r:/WORK/fifo read_verilog -container i -libname WORK -01 /home/user/tutorial/gate/fifo_mod.vg read_db -container i /home/user/tutorial/lib/lsi

14、_10k.db set_top i:/WORK/fifo match verify,命令行方式運行,在unix命令提示行下輸入命令： fm_shell f fifo_rtl_gate.fms unix命令提示行輸入命令fm_shell，進入formality的命令行模式。 在formality的命令行模式fm_shell提示符下輸入命令： source fifo_rtl_gate.fms,檢查RTL與GATE網(wǎng)表 檢查GATE網(wǎng)表和插入掃描鏈的GATE網(wǎng)表 檢查帶有掃描鏈和JTAG鏈的GATE網(wǎng)表和插入掃描鏈的GATE網(wǎng)表,提 綱,二.檢查fifo_mod.vg和 fifo_with_scan

15、.v的功能,設置fifo_mod.vg為reference design 設置fifo_with_scan.v為implementation design,1. set referenc design,點擊reference按鈕，在Read Design Files 中點擊Verilog，選擇gate目錄下的verlog網(wǎng)表文件fifo_mod.vg，點擊Load Files加載網(wǎng)表文件fifo_mod.vg 在Read DB Files 中點擊DB加載lsi_10k.db庫文件，點擊Load Files加載 Set top，設置fifo模塊為頂層。,2. set implementation

16、 design,點擊implementation按鈕，在Read Design Files 中點擊Verilog，選擇gate_with_scan目錄下的verlog網(wǎng)表文件fifo_with_scan.v，點擊Load Files加載網(wǎng)表文件fifo_with_scan.v 可以省略Read DB Libraries這一步，因為在設置fifo_mod.vg時，我們已經(jīng)加載lsi_10k.db為共享庫文件。 Set top，設置fifo模塊為頂層。,3. setup,由于在fifo_with_scan.v網(wǎng)表里加入了掃描鏈（scan）邏輯，在驗證之前，我們必須把這一掃描鏈（scan）邏輯功能禁

17、止（disable）。 進入Setup界面后，選擇Constants，點擊Set按鈕，出現(xiàn)set Constant對話框。,設置SCAN鏈的功能無效,選擇Implementation，選擇Instance的頂層fifo，在頂層fifo的ports目錄下面搜索找到名為test_se（SCAN功能的使能信號）的管腳， 在Constant Value中選擇值0，設置test_se的值為0，點擊OK按鈕。,4. match,點擊match，進入比較點（compare point）匹配步驟。點擊Run Matching,運行 運行結(jié)果：報告一個不匹配的compare point。點擊ok，查看不匹配點。

18、,選擇Unmatched Points，可以看到報告欄里報告Implementation Object的test_se引腳不匹配。這個引腳是Implementation Design中多余的compare point. 我們在前一步驟里，已經(jīng)把它禁止啦。故可以跳過這個不匹配點，進入下一步驟Verification。,5. verify,選擇Verify，點擊Verify All按鈕，進行形式檢查。 運行結(jié)果如圖：,結(jié)果報告如圖：,檢查RTL與GATE網(wǎng)表 檢查GATE網(wǎng)表和插入掃描鏈的GATE網(wǎng)表 檢查帶有掃描鏈和JTAG鏈的GATE網(wǎng)表和插入掃描鏈的GATE網(wǎng)表,提 綱,三.檢查fifo_with_scan_jtag.v和 fifo_with_scan.v一致性,fifo_with_scan_jtag.v是帶有掃描SCAN鏈邏輯和JTAG鏈邏輯的網(wǎng)表文件 上一節(jié)中我們已經(jīng)驗證帶有scan的網(wǎng)表文件fifo_with_scan.v和fifo_mod.vg功能相同 把fifo_with_scan.v作為參考設計，來檢查fifo_with_scan_jtag.v的功能,和前面步驟一樣，分別