【正文】 module top。 bit clock。//裝載接口 dut dut(.io(my_io), .clock(clock), .rst(rst), .en(rst_check))。//裝載環(huán)境 top_env function new(string name = my_test, ovm_ponent parent = null)。 ()。 endfunction: build 58 共 91頁 virtual function void connect。 my_transaction tx。//激勵器產(chǎn)生20個事件 endtask: run endclass: my_test 59 共 91頁 initial begin run_test(“my_test”)。 (32*clock_cycle) rst=1。 $fsdbDumpvars(0,top,+all)。 ? 需要的文件： SDF文件 IO庫的 Verilog模型文件 動態(tài)時序仿真（后仿） 69 共 91頁 Testbench，添加布局布線完導(dǎo)出的 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文件，并反標(biāo)到網(wǎng)表每個節(jié)點上。 74 共 91頁 PrimeTime流程 ； ； PVT和線上負(fù)載模型； ； 。 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。） 當(dāng)鍵控信號為 1時，模塊產(chǎn)生并輸出 (8倍 ) 當(dāng)鍵控信號為 0時，模塊產(chǎn)生并輸出 (7倍 ) 附錄 FSK電路基本功能 91 共 91頁 。 restore_session verify report_failing_points diagnose 89 共 91頁 作業(yè) 后仿布局布線導(dǎo)出的網(wǎng)表文件（帶 SDF文件）。 76 共 91頁 命令輸入?yún)^(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 ? 所謂形式驗證，就是通過比較兩個設(shè)計在邏輯功能是否等同的方法來驗證電路的功能。 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。 61 共 91頁 腳本方式完成驗證 ? vlib dac_hcic //創(chuàng)建庫 ? vlog +acc f ../rtl/ovm_rtl/ work dac_hcic sv +cover // 編譯整個驗證平臺 ? vsim c sv_seed 100 coverage assertcover assertdebug sva voptargs=“+acc” pli /opt/springsoft/verdi/share/PLI/MODELSIM/LINUX/ //啟動