Formality使用指南專業(yè)知識講座

Formality使用指南第1頁檢查RTL與GATE網(wǎng)表檢查GATE網(wǎng)表和插入掃描鏈GATE網(wǎng)表檢查帶有掃描鏈和JTAG鏈GATE網(wǎng)表和插入掃描鏈GATE網(wǎng)表提綱第2頁說明FiFoTutorial目錄下包括下列幾個子目錄：Rtl：fifoRTL源代碼；包括fifo.v,gray_counter.v,push_ctrl.v,gray2bin.v,pop_ctrl.v,rs_flop.v。Lib：門級網(wǎng)表需要技術(shù)庫；包括lsi_10k.db。Gate：綜合門級網(wǎng)表；包括fifo.vg和fifo_mod.vg。Gate_with_scan：插入掃描鏈門級網(wǎng)表；包括fifo_with_scan.v。Gate_with_scan_jtag：帶有掃描鏈和JTAG鏈門級網(wǎng)表；包括fifo_with_scan_jtag.v。第3頁一.檢查RTL與GATE網(wǎng)表RTL源代碼：fifo.v門級網(wǎng)表：fifo.vg檢查文獻fifo.v和門級網(wǎng)表fifo.vg功能一致性設(shè)置RTL源代碼fifo.v為referencedesign設(shè)置門級網(wǎng)表fifo.vg為Implementationdesign第4頁（一）圖形顧客界面進行形式驗證在UNXI提醒符下進入tutorial目錄：輸入fm（或formality）。第5頁第6頁1.設(shè)置referencedesign點擊formality圖形界面reference按鈕，進入ReadDesignFile點擊Verilog按鈕，出現(xiàn)添加Verilog文獻對話框。如下列圖：第7頁1.1讀取源文獻在對話框中選擇：Rtl目錄下fifo.v文獻，點擊Open按鈕,打開fifo.v源代碼。如圖：第8頁1.2設(shè)置搜索目錄點擊option按鈕，出現(xiàn)setverilogreadoption對話框,選擇Variable,在DesingWarerootdirectory(hdlin_dwroot)出輸入：echo$SYNOPSYS或DesignCompiler安裝目錄(本工作站目錄為/opt/tools/synopsys)，如下列圖：

第9頁第10頁1.3設(shè)置搜索目錄在Setverilogreadoption對話框中VCSStyleOption中選擇LibraryDirectory(-y),在EnterDiectoryName處瀏覽選擇rtl目錄然后點擊add按鈕添加查找目錄rtl。第11頁選擇LibraryExtension(-libext)，在EnterFileExtension處填上后綴名.v，然后點擊add按鈕添加，點擊OK按鈕。第12頁1.4加載源文獻然后點擊LOADFILES按鈕，加載源文獻fifo.v，如下列圖：第13頁1.5設(shè)置fifo為reference頂層在點擊SetTopDesign按鈕，出現(xiàn)下列圖。第14頁在choosealibrary

中選擇WORK，在chooseadesign中選擇fifo（頂層設(shè)計模塊名）在Setandlinkthetopdesign中點擊SetTop，出現(xiàn)下列圖同步在Reference按鈕上出現(xiàn)綠色對號符：第15頁2.設(shè)置ImplementationDesign點擊Implement按鈕，在ReadDesignFiles

中點擊Verilog，出現(xiàn)Addverilogfiles對話框，選擇gate目錄下verlog網(wǎng)表文獻fifo.vg，點擊LoadFiles加載網(wǎng)表文獻fifo.vg，第16頁2.1加載Technologylibrary選擇ReadDBLibraries按鈕，點擊DB…按鈕，出現(xiàn)AddDBFiles對話框選擇lib目錄下lsi_10k.db庫文獻，（確保Readassharelibrary被選中）點擊LOADFiles，加載庫文獻。第17頁選擇SetTopDesign,在Choosealibrary中選擇WORK(DesignLibrary),在Chooseadesign中選擇頂層模塊名fifo，點擊SetTop按鈕。此時在Implementation出現(xiàn)綠色對號符。第18頁3.設(shè)置環(huán)境(Setup)在這一步主要是設(shè)置常量，例如對應(yīng)某些增加了SCAN掃描鏈和JTAG鏈設(shè)計，需要設(shè)置某些常量，使這些SCAN和JTAG等功能嚴禁。由于fifo.v是源代碼，fifo.vg只是綜合源代碼，沒有添加SCAN和JTAG鏈。故能夠省略這一步第19頁4.Match檢查referencedesign和Implementiondesign比較點是否匹配點擊Match按鈕，選擇RunMatching按鈕，進行匹配檢查。

出現(xiàn)下列圖成果：沒有不匹配比較點，能夠進入下一步。

第20頁5.Verify點擊OK鍵，完成。目前你已經(jīng)準備好，能夠進行fifo.v和fifo.vg功能是否一致。選擇Verify按鈕，點擊VerifyAll，進行形式驗證。驗證結(jié)束，成果出現(xiàn)“Verify”fail對話框，提醒兩種功能不一致。

第21頁6.Debug由于驗證失敗，系統(tǒng)直接進入DEBUG工作區(qū)。在FailingPoints報告工作區(qū)里顯示兩設(shè)計出不一致比較點在FailingPoints報告工作區(qū)內(nèi)點擊鼠標右鍵，選擇ShowAllConeSize,在Size欄里顯示每個comparpoint所包括cell數(shù)目一般調(diào)試是從cell數(shù)目最小comparepoint開始。在這里我們從第一種comparepoint開始。選擇r:/WORK/fifo/push_logic/full_flag/q_out_reg[o],擊鼠標右鍵，選擇菜單中viewLogicCones，出現(xiàn)LogicConesView窗口。

第22頁第23頁在這個新窗口里顯示是referencedesign和Imeplementiondesign原理圖，觀看這個原理圖我們發(fā)覺在ImplementationCLK網(wǎng)線是用紅色標識在logicconeview中，用紅色標識net網(wǎng)線是表達錯誤我們觀測發(fā)覺在referencedesignCLK中表達logic值為0，而ImeplementiondesignCLK中表達logic值為1。為了找出CLKnet值不一樣原因，分別選擇referencedesign和ImeplementiondesignCLK網(wǎng)線，選擇右鍵菜單里IsolateSubcone命令，出現(xiàn)下列圖。第24頁第25頁在圖中能夠看出在Imeplementiondesign中驅(qū)動CLK邏輯里多了一種反相器，這有也許是綜合工具為了滿足hold-time要求而增加反相器。我們能夠修改fifo.vg網(wǎng)表文獻和重新綜合一種網(wǎng)表文獻，來修改這個錯誤。在gate目錄下有一種fifo_mod.vg文獻是修改后網(wǎng)表文獻。關(guān)閉LogicconeView,重新用fifo_mod.vg作為Implementationdesign。選擇Implementation，點擊ReadDesignFiles中Verilog，點擊yes來移除目前ImplementationDesign設(shè)計（fifo.vg）。重新選擇fifo_mod.vg，點擊Loadfiles，加載文獻。

SettopDesign,選擇WORK和fifo第26頁第27頁第28頁同樣，跳過Setup點擊Match,選擇RunMatching，運行完后出現(xiàn)下列圖：

第29頁點擊Verify，選擇Verifyall，運行完出現(xiàn)下列圖，提醒“VerificationSuccessded!”第30頁點擊OK后，出現(xiàn)下列圖，顯示所有comparepoint都pass。到此，完成形式驗證。第31頁清理工作選擇工具欄中removereference

和removeImplementation按鈕，移除referencedesign和Implementationdesign在formality命令行輸入：remove_library–all命令移除technologylibrary:lsi_10k.db。第32頁（二）命令行方式進行形式驗證在上一節(jié)不退出formality圖形界面，在formality命令欄中輸入：history>fifo_rtl_gate.fms,生成腳本文獻fifo_rtl_gate.fms退出formality圖形界面第33頁fifo_rtl_gate.fms內(nèi)容sethdlin_dwroot/opt/tools/synopsys_2023.06read_verilog-containerr-libnameWORK-vcs"-y/home/user/tutorial/rtl/+libext+.v"-01{/home/user/tutorial/rtl/fifo.v}set_topr:/WORK/fiforead_verilog-containeri-libnameWORK-01{/home/user/tutorial/gate/fifo_mod.vg}read_db-containeri{/home/user/tutorial/lib/lsi_10k.db}set_topi:/WORK/fifomatchverify第34頁命令行方式運行在unix命令提醒行％下輸入命令：

fm_shell–ffifo_rtl_gate.fms

unix命令提醒行％輸入命令fm_shell，進入formality命令行模式。

在formality命令行模式fm_shell>提醒符下輸入命令：

sourcefifo_rtl_gate.fms

第35頁檢查RTL與GATE網(wǎng)表檢查GATE網(wǎng)表和插入掃描鏈GATE網(wǎng)表檢查帶有掃描鏈和JTAG鏈GATE網(wǎng)表和插入掃描鏈GATE網(wǎng)表提綱第36頁二.檢查fifo_mod.vg和

fifo_with_scan.v功能設(shè)置fifo_mod.vg為referencedesign設(shè)置fifo_with_scan.v為implementationdesign第37頁1.setreferencdesign點擊reference按鈕，在ReadDesignFiles

中點擊Verilog，選擇gate目錄下verlog網(wǎng)表文獻fifo_mod.vg，點擊LoadFiles加載網(wǎng)表文獻fifo_mod.vg在ReadDBFiles

中點擊DB加載lsi_10k.db庫文獻，點擊LoadFiles加載Settop，設(shè)置fifo模塊為頂層。第38頁第39頁第40頁第41頁2.setimplementationdesign點擊implementation按鈕，在ReadDesignFiles

中點擊Verilog，選擇gate_with_scan目錄下verlog網(wǎng)表文獻fifo_with_scan.v，點擊LoadFiles加載網(wǎng)表文獻fifo_with_scan.v能夠省略ReadDBLibraries這一步，由于在設(shè)置fifo_mod.vg時，我們已經(jīng)加載lsi_10k.db為共享庫文獻。

Settop，設(shè)置fifo模塊為頂層。第42頁第43頁3.setup由于在fifo_with_scan.v網(wǎng)表里加入了掃描鏈（scan）邏輯，在驗證之前，我們必須把這一掃描鏈（scan）邏輯功能嚴禁（disable）。進入Setup界面后，選擇Constants，點擊Set按鈕，出現(xiàn)setConstant對話框。

第44頁第45頁設(shè)置SCAN鏈功能無效選擇Implementation，選擇Instance頂層fifo，在頂層fifoports目錄下面搜索找到名為test_se（SCAN功能使能信號）管腳，在ConstantValue中選擇值0，設(shè)置test_se值為0，點擊OK按鈕。

第46頁第47頁第48頁4.match點擊match，進入比較點（comparepoint）匹配步驟。點擊RunMatching,運行運行成果：報告一種不匹配comparepoint。點擊ok，查看不匹配點。第49頁第50頁選擇UnmatchedPoints，能夠看到報告欄里報告ImplementationObjecttest_se引腳不匹配。這個引腳是ImplementationDesign中多出comparepoint.我們在前一步驟里，已經(jīng)把它嚴禁啦。故能夠跳過這個不匹配點，進入下一步驟Verification。

第51頁5.verify選擇Verify，點擊VerifyAll按鈕，進行形式檢查。運行成果如圖：第52頁成果報告如圖：第53頁檢查RTL與GATE網(wǎng)表檢查GATE網(wǎng)表和插入掃描鏈GATE網(wǎng)表檢查帶有掃描鏈和JTAG鏈GATE網(wǎng)表和插入掃描鏈GATE網(wǎng)表提綱第54頁三.檢查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作為參照設(shè)計，來檢查fifo_with_scan_jtag.v功能

第55頁和前面步驟同樣，分別設(shè)置fifo_w