【正文】 91頁 斷言結果查看 — Questasim下 65 共 91頁 代碼斷言結果查看 — Verdi下 Verdi（另外一個軟件，專門用作波形查看和調 試）下查看斷言結果更加直觀，箭頭朝上就表示 斷言通過，朝下表示斷言失敗。 66 共 91頁 代碼覆蓋率查看 67 共 91頁 代碼覆蓋率查看 68 共 91頁 ? 動態(tài)時序仿真：利用仿真器（ Modelsim）和延遲文件 (SDF文件 )，通過反標節(jié)點延遲信息來仿真。 ? 需要的文件： SDF文件 IO庫的 Verilog模型文件 動態(tài)時序仿真（后仿） 69 共 91頁 Testbench，添加布局布線完導出的 SDF文件 Testbench文件 Verilog模型文件 /home/smic/smic_40/SCC40NLL_HS_RVT_V0 p1a/verilog/ IO的 Verilog模型文件 /home/smic/smic_40/SP40NLLD2RN_3P3V_V 0p2/verilog/ 動態(tài)時序仿真（后仿）步驟 70 共 91頁 Testbench中添加 SDF文件 在 Testbench中新建一個 initial 塊， 通過系統(tǒng)函數(shù) $sdf_annotate()來讀入 SDF文件，并反標到網表每個節(jié)點上。具體代碼如下： initial begin $sdf_annotate(“/home/liuxp/class/astro/SDF/top ”, )。 end Testbench 模塊名稱 實例化的頂層模塊名稱 71 共 91頁 后仿真波形 整體功能波形： 延遲信息： 72 共 91頁 靜態(tài)驗證工具 ? 靜態(tài)時序分析 — Prime Time ? 形式驗證 Formality 73 共 91頁 靜態(tài)時序分析 — PrimeTime ? PrimeTime是 Synopsys的靜態(tài)時序分析軟件，常被用來分析大規(guī)模、同步、數(shù)字 ASIC。 ? PrimeTime適用于門級的電路設計。 74 共 91頁 PrimeTime流程 ； ； PVT和線上負載模型； ； 。 75 共 91頁 PrimeTime工具啟動 ? source /opt/demo/ ? pt_shell（無圖形界面） 或者 ? primetimeamp。 76 共 91頁 命令輸入區(qū) 77 共 91頁 PrimeTime腳本 — source set lib_path /home/smic/smic_65/SCC65NLL_HS_RVT_V1p1a set smic_stdlib_path ${lib_path}/synopsys/set smic_diolib_path /home/smic/smic_65/SP65NLLD2RP_OV3_TTM_V0p2a/syn/3p3v/ set smic_aiolib_path /home/smic/smic_65/SP65NLLD2RP_OV3_ANALOG_TTM_V0p2a/syn/3p3v/ set smic_stdsymlib_path ${lib_path}/symbol/ set smic_iosymlib_path ${lib_path}/symbol/ set search_path $smic_stdlib_path $smic_aiolib_path \ $smic_diolib_path $smic_stdsymlib_path $smic_iosymlib_path“ set link_library * “ set symbol_library [list ] remove_design –all read_verilog ../syn/list/“ link_design dac current_design dac list_designs report_cell 78 共 91頁 PrimeTime腳本 — source set_operating_conditions min_library scc65nll_hs_rvt_ff_v1p32_40c_basic min ff_v1p32_40c max_library scc65nll_hs_rvt_ss_v1p08_125c_basic max ss_v1p08_125c analysis_type bc_wc //set_operating_conditions library scc65nll_hs_rvt_ff_v1p32_40c_basic //ff_v1p32_40c create_clock name clk period 300 waveform [list 0 150] clk_in_pad set_clock_latency [all_clocks] set_clock_uncertainty setup clk set_clock_transition 2 [get_clocks clk] set_drive 0 [list clk clk_in_pad ] set_load 5 [all_outputs] set_input_delay 5 clock clk max [remove_from_collection [all_inputs] [get_ports {clk_in_pad}] ] set_output_delay 5 clock clk max [all_outputs] report_constraint report_timing 79 共 91頁 形式驗證 Formality ? 所謂形式驗證，就是通過比較兩個設計在邏輯功能是否等同的方法來驗證電路的功能。 ? Formality是 Synopsys公司的產品，與PrimeTime結合起來使用。 80 共 91頁 形式驗證 Formality Logic Cone BB BB Inputs ? Outputs from Registers ? Primary Input Ports ? Outputs from Black Boxes Compare Points ? Inputs to Registers ? Primary Output Ports ? Inputs to Black Boxes Compare Point A design contains Logic Cones and Compare Points 81 共 91頁 形式驗證 Formality D Q BB Determining Compare Points ? Breaks the two logic circuits up into logic cones: ? End points (pare points) are primary outputs, registers, and black box inputs 82 共 91頁 形式驗證 Formality D Q BB Reference Design D Q BB Implementation Design CP CP CP ? Compare points are then aligned: ? This process is called “pare point matching” ? End points of logic cones (pare points) are primary outputs, registers, and black box inputs 83 共 91頁 形式驗證 Formality Verify Design ? For each matched pair of pare points Formality tries to : Either ? Confirms same response for all possible input binations. ? Marks point as “passed” Or ? Finds a “counter example” that shows different response ? Marks point as “failed” 84 共 91頁 Formality流程 container 85 共 91頁 Formality工具啟動 ? source /opt/demo/ ? fm_shell （無圖形界面） 或者formality amp。 86 共 91頁 命令輸入區(qū) 87 共 91頁 Formality— source set lib_path /home/smic/smic_65/SCC65NLL_HS_RVT_V1p1a set smic_stdlib_path ${lib_path}/synopsys/set smic_diolib_path /home/smic/smic_65/SP65NLLD2RP_OV3_TTM_V0p2a/syn/3p3v/ set smic_aiolib_path /home/smic/smic_65/SP65NLLD2RP_OV3_ANALOG_TTM_V0p2a/syn/3p3v/ set search_path “ $smic_stdlib_path $smic_aiolib_path $smic_diolib_path create_container ref read_db [list \ \ ] read_verilog {../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/ \ ../rtl/dac_haf_cic/} 88 共 91頁 Formality— source set_reference_design ref:/WORK/total link $ref create_container icmp read_verilog list ../syn/list/ set_implementation_design icmp:/WORK/total set_top icmp:/WORK/total save_session replace fm_shell_session exit formalityamp。 restore_session verify report_failing_points diagnose 89 共 91頁 作業(yè) 后仿布局布線導出的網表文件（帶 SDF文件）。 90 共 91頁 輸入一個 564KHz的鍵控信號，（這里為了簡化描述，使用 564 KHz來描述鍵控信號的速率，正常情況下是用 kbps。） 當鍵控信號為 1時，模塊產生并輸出 (8倍 ) 當鍵控信號為 0時，模塊產生并輸出 (7倍 ) 附錄 FSK電路基本功能 91 共 91頁