数字集成电路验证方法学ppt课件.ppt

《数字集成电路验证方法学ppt课件.ppt》由会员分享，可在线阅读，更多相关《数字集成电路验证方法学ppt课件.ppt（91页珍藏版）》请在三一办公上搜索。

1、数字集成电路验证方法学,浙江大学ICLAB实验室2016-12-26,主要内容,验证的必要性验证方法学介绍验证工具介绍演示,2,共91页,主要内容,验证的必要性验证方法学介绍验证工具介绍演示,3,共91页,验证的必要性,验证的概念，验证与测试的区别。经验表明，验证已经占到整个产品开发周期的70%以上，它已经成为复杂SOC（System on-Chip）开发中的重要壁垒。制造、设计和验证能力之间存在鸿沟,4,共91页,典型流程,Verification is not just very hard,it is very,very hard没有一个简单的工具可以解决你所有的验证问题。(VSIA,Vi

2、rtualSocketInterfaceAlliance),5,共91页,主要内容,验证的必要性验证方法学介绍验证工具介绍演示,6,共91页,验证方法学,方法学：又称方法论，是一门学问采用的方法、规则与公理；一种特定的做法或一套做法。验证方法学：指完成验证过程中的一系列方法、技术和规范。1.仿真技术 2.静态技术 3.物理验证,7,共91页,仿真技术,基于事件的仿真-任何一个输入的变化都被标记为事件，即常说的功能仿真，精度高，速度慢。比如Modelsim,VCS。基于周期的仿真-单周期内只检查一次输入并计算设计的输出逻辑值。速度快，无时序、毛刺。比如Cyclone。事务级仿真-一堆事件的集合即

3、为事务，即常说的验证平台。软硬件协同验证-需要专门的硬件，成本高。,8,共91页,验证方法比较,9,共91页,传统验证系统,DUT：Design Under Test适用于基于事件的仿真和基于周期的仿真。适用于简单的设计。,缺点：1.可扩展性差2.可重用性差,10,共91页,层次化的验证系统,适用于事务级仿真优点：1.可扩展性好2.可重用性好,11,共91页,为什么要用事务级仿真？,基于事件的仿真与事务级仿真的比较,12,共91页,事务级仿真,RVM：ReferenceVerificationMethodology,Synopsys公司。VMM：VerificationMethodology

4、Manual,ARM公司和 Synopsys公司。AVM：Advanced Verification Methodology,Mentor公司。OVM：Open Verification Methodology,Cadence和Mentor公司。UVM：Universal Verification Methodology,Cadence、Mentor和Synopsys公司。,13,共91页,为什么选用OVM？,各种验证方法学比较,14,共91页,OVM介绍,OVM是一种基于SystemVerilog的验证方法或者策略，已经实现了一个基本的层次化验证平台，大大简化验证工程师的工作量。OVM可以验

5、证HDL代码或者网表文件OVM特点：1.开放性：支持所有验证工具 2.开源：OVM库都是基于SystemVerilog实现的，可以在网上下载。3.可靠性：两大公司共同开发维护,15,共91页,OVM结构,ovm_envovm_sequencerovm_agentovm_scoreboardovm_driverovm_monitor,16,共91页,SystemVerilog介绍,SystemVerilog结合了Verilog和C+的概念，具有如下新功能：1.面向对象编程(OOP)、2.随机约束(Constraint Random)、3.断言(Assertion)、4.功能覆盖率(Functio

6、nal Coverage)。,17,共91页,OOP：Object-oriented programming对象：对象(Object)是一个现实实体的抽象，对象可被认为是一个把数据（属性）和程序（方法）封装在一起的实体，这个程序产生该对象的动作，属性反映了对象当前的状态。面向对象编程：主要是将我们实际生活中的对象经过抽象，将它定义成为一个类，通过类的属性和方法来模拟生活中的这个对象。这样使得程序更容易结构化、抽象起来更方便。传统的编程结构和设计方法以过程为中心进行功能组合，代码的扩充和复用能力很差。对象是对现实世界实体的模拟，因面能更容易地理解需求，即使用户和分析者之间具有不同的教育背景和工作

7、特点，也可很好地沟通。,SystemVerilog介绍-面向对象编程,18,共91页,类：定义实物的抽象特点，包含方法和属性。对象：类的实例。方法：类的行为。继承：子类包含类的特性。,SystemVerilog介绍-面向对象编程,19,共91页,CRT:Constraint Random Test class my_transaction extends ovm_transaction;rand int data_i;constraint c_data_i data_i=0;data_i 262144;endclassmy_transaction tr=new();tr.randomize()

8、;/tr.data_i大于0小于262144,SystemVerilog介绍-随机约束,20,共91页,SystemVerilog介绍-随机约束,class transcation;rand bit 1:0 src;rand bit 31:0 data;bit 31:0 low,high;constraint cons src dist 0:=40,1:3:=60;data inside low:high;endclass,21,共91页,SystemVerilog介绍-断言,断言：属于验证方法中的一种，是对设计属性(行为)的描述，如果一个属性不是我们期望的那样，那么断言就会失败。assert

9、ions与verilog相比：verilog是一种过程性语言。它的设计目的是硬件描述，它可以很好的控制时序，但是描述复杂的时序关系，代码较为冗长。assertions是一种描述性语言，设计目的为仿真验证，可以有很多内嵌的函数来测试特定的时序关系和自动收集覆盖率数据。,22,共91页,SystemVerilog介绍-断言,Assertion 示例property p10;(posedge clock)(io.data_check_o=data_out_design_for_check-2);endpropertya10:assert property(p10);,23,共91页,SystemVe

10、rilog介绍-断言,property pr1;(posedge clock)start|-req#2(gnt=1,24,共91页,SystemVerilog介绍-功能覆盖率,功能覆盖率:衡量哪些设计特征已经被程序验证过的一个指标代码覆盖率 1.语句覆盖(StatementCoverage)2.判定覆盖(DecisionCoverage)3.条件覆盖(ConditionCoverage)4.路径覆盖(PathCoverage),25,共91页,语句覆盖,语句覆盖(StatementCoverage)：度量被测代码中每个可执行语句是否被执行到了。intfoo(inta,intb)returna/

11、b;TeseCase:a=10,b=5 语句覆盖率：100%代码的bug:b=0,26,共91页,判定覆盖&条件覆盖,判定覆盖(DecisionCoverage)：度量程序中每一个判定的分支是否都被测试到了。条件覆盖(ConditionCoverage)：度量判定中的每个子表达式结果true和false是否被测试到了。intfoo(inta,intb)if(a10|b10)/判定return0;/分支一elsereturn1;/分支二,TestCaes1:a=5,b15覆盖了分支一TestCaes2:a=15,b=15 覆盖了分支二,TestCase1:a=5,b=5true,trueTest

12、Case2:a=15,b=15false,false,TestCase1:a=5,b=15true,false分支一TestCase2:a=15,b=5false,true分支一,判定覆盖率：100%，条件覆盖100%,条件覆盖率：100%判定覆盖率：100%,条件覆盖率：100%，判定覆盖100%,27,共91页,路径覆盖,路径覆盖(PathCoverage)：度量了是否函数的每一个分支都被执行了。,intfoo(inta,intb)intnReturn=0;if(a10)/分支一nReturn+=1;if(b10)/分支二nReturn+=10;returnnReturn;,TestCas

13、e1 a=5,b=5 nReturn=11TestCase2 a=15,b=5 nReturn=10TestCase3 a=5,b=15 nReturn=1TestCase4 a=15,b=15 nReturn=0路径覆盖率：100%,28,共91页,SystemVerilog介绍-功能覆盖率,29,共91页,Functional Coveragecovergroup：覆盖率模型coverpoint:覆盖点sample()：采样函数bins:仓,SystemVerilog介绍-功能覆盖率,30,共91页,SystemVerilog介绍-功能覆盖率,covergroup Covkind;cove

14、rpoint tr.kind/kind为4位数据 bins zero=0;bins hi=8:$;endgroupCovkind cov=new();Cov.sample();,31,共91页,SystemVerilog介绍-功能覆盖率,covergroup group(posedge clk);ca:coverpoint a;/a为1bit cb:coverpoint b;/b为1bit cab:cross ca cb;endgroupgroup grp=new();/不需要调用grp.sample();,32,共91页,静态技术,语法检查-用户可以自由控制需要检查的规则，如代码风格，可综合

15、检查，DFT检查。nlint工具。静态时序分析-检查建立、保持时间以及其他延时信息是否满足设计时序要求。Prime Time。形式验证等价性检查：不考虑时序信息，通常用于验证两个设计是否在功能上等效（有golden design）。Formality 工具。模型检查：验证设计的功能（没有golden design）。JasperGold,33,共91页,语法检查,用户可以自由控制需要检查的规则代码风格检查：命名规范等可综合检查：设计的代码是否满足可综合要求DFT检查：代码是否会影响后端DFT的设计跨时钟域设计检查：亚稳态传播检查等常用工具为：nlint工具。,34,共91页,一般来说，要分析或

16、检验一个电路设计的时序方面的特征有两种主要手段：动态时序仿真（Dynamic Timing Simulation）和静态时序分析（Static Timing Analysis）1.动态时序仿真：利用仿真器和延迟文件，通过反标节点延迟信息来仿真。优点：可直观查看波形；缺点：速度慢，看不到关键路径。2.静态时序分析：分析每条时间路径上的延迟，来查看是否存在setup/hold违反。优点：分析速度比较快，全面；缺点：不能查看功能是否正确。,静态时序分析,35,共91页,静态时序分析,针对建立时间、保持时间的检查，分为四种情况输入端口到寄存器寄存器到寄存器寄存器到输出输入到输出针对周期个数，分为：单周

17、期检查多周期检查,36,共91页,所谓等价性检查，就是通过比较两个设计在逻辑功能是否等同的方法来验证电路的功能。优点：1.不依赖于测试矢量，因此能提供更完全的验证；2.可以实现RTL-to-RTL、RTL-to-gate、gate-to-gate两者之间的验证；3.有定位功能，可以帮助你找出两个设计之间功能不等同的原因；4.可以使用的文件格式有VHDL、Verilog、Synopsys 的.db格式,以及EDIF网表等；5.可以实现自动的分层验证；,形式验证之等价性检查,37,共91页,形式验证之等价性检查,#set reference(RTL)read_verilog-r-libname W

18、ORK ABC.vread_db tcb018gbwp7twc.dbset_top ABC#set implentation(Gate)read_verilog-i-libname WORK ABC_mapped.vset_top ABCmatchverify,38,共91页,所谓模型检查，就是通过SystemVerilog中的断言来描述DUT的特性，通过穷举法产生随机激励，判断设计是否满足设计需求。是仿真的补充。优点：1.不需要人为产生激励，产生的激励更完整；2.对于某些模块，用模型检查比仿真验证速度更快 3.得到的波形很短(主要是断言失败的波形)，几十个周期，方便定位问题缺点：只能适合用于

19、模块级别的验证,形式验证之模型检查,39,共91页,物理验证-版图级,电源电压降串扰 Astro/ICC 布局布线工天线效应 具中完成电迁移,40,共91页,物理验证-版图级,电迁移 EM(electrical mobility)概念：金属线在电流和温度的作用下产生的金属迁移的现象原因：电子沿着电压梯度漂移，与组成导线的金属粒子发生碰撞，若能量很高，会使金属导体的某些部位产生空洞或小丘，从而引起导线失效。失效模式:主要包括短路、断路以及参数退化和时序违规等,41,共91页,主要内容,验证的必要性验证方法学介绍验证工具介绍演示,42,共91页,如何利用OVM完成验证？,43,共91页,基于OVM

20、的数字滤波器验证平台,数模转化器（DAC）中的数字插值滤波器作为此验证平台的DUT数字插值滤波器的功能：1.提高采样频率 2.滤除带外（带宽20KHz）噪声,44,共91页,传统的滤波器验证平台仿真结果,传统的验证平台：基于定向测试矢量+波形查看的方式,45,共91页,传统验证平台没找到BUG的原因,1.仿真时间没有足够长 2.借助波形来判断 3.没有与理想参考模型比较 基于OVM的验证平台,46,共91页,OVM验证平台验证步骤,1.利用OVM库完成平台代码2.启动验证工具3.创建编译库4.编译验证平台代码5.启动仿真,47,共91页,利用OVM库完成平台代码,扩展OVM类逐层完成：1.接口

21、 2.数据产生 3.驱动器 4.验证环境 5.比较器,48,共91页,OVM平台-接口,interface io_if();logic 17:0 data_i;logic 17:0 data_o;logic 17:0 data_check_o;modport dut_if(input data_i,output data_o);/DUT接口modport check_if(input data_i,output data_check_o);/比较器模块接口 Endinterfaceio_if my_io();/装载接口module check(io_if.check_if io,input c

22、lock,rst,en);dut dut(.io(my_io),.clock(clock),.rst(rst),.en(rst_check);check check(.io(my_io),.clock(clock),.rst(rst),.en(rst_check);,49,共91页,OVM平台数据产生,class my_transaction extends ovm_transaction;rand int data_i;function new(string name=);super.new(name);endfunction:new/产生随机事件的约束条件 constraint c_dat

23、a_i data_i=0;data_i 262144;virtual function void randomize_();data_i=$random endfunctionovm_object_utils_begin(my_transaction)/在程序中 ovm_field_int(data_i,OVM_ALL_ON+OVM_DEC)ovm_object_utils_end endclass:my_transaction,50,共91页,OVM平台驱动器,class my_driver extends ovm_driver;/ovm_component_utils(my_driver)

24、/注册本类，这个宏的结尾没有符号；virtual io_if v_io;/装载虚拟接口 ovm_get_port#(my_transaction)get_port;/装载与激励发生器通信的通道接口：function new(string name,ovm_component parent);super.new(name,parent);/建议验证程序中可写一些ovm_report_info的语句供提示用：ovm_report_info(,Called my_driver:new);/在测试结果显示此函数被调用 endfunction:new,51,共91页,function void buil

25、d;super.build();ovm_report_info(,Called my_driver:build);get_port=new(get_port,this);/初始化 endfunction:build virtual task run;ovm_report_info(,Called my_driver:run);forever begin my_transaction tx;#1600 get_port.get(tx);/从通道中取一个事件 ovm_report_info(,$psprintf(data_i=%2h,tx.data_i);v_io.dut_if.data_i=tx

26、.data_i;end endtask:run endclass:my_driver,52,共91页,OVM平台验证环境,class my_env extends ovm_env;/ovm_component_utils(my_env)/注册本类 ovm_random_stimulus#(my_transaction)env_stimulus;/装载激励器 tlm_fifo#(my_transaction)env_fifo;/装载通道 my_driver env_driver;/装载驱动器 function new(string name=my_env,ovm_component parent

27、=null);super.new(name,parent);ovm_report_info(,Called my_env:new);endfunction:new,53,共91页,virtual function void build;super.build();ovm_report_info(,Called my_env:build);env_stimulus=new(env_stimulus,this);/初始化激励器 env_fifo=new(env_fifo,this);/初始化通道 env_driver=new(env.driver,this);/初始化驱动器 endfunction

28、:build virtual function void connect;/设定连接关系 ovm_report_info(,Called my_env:connect);env_stimulus.blocking_put_port.connect(env_fifo.put_export);/激励器侧接口-放事件 env_driver.get_port.connect(env_fifo.get_export);/驱动器侧接口-取事件 endfunction:connect,54,共91页,virtual function void configure;/ovm_report_info(,Call

29、ed my_env:configure);env_stimulus.set_report_id_action(stimulus generation,OVM_NO_ACTION);/限制显示信息 endfunction:configure/你可删除上一行，看看有什么变化？task run();ovm_report_info(,Called my_env:run);endtask:run virtual function void report;ovm_report_info(,Called my_env:report);endfunction:report/在运行下面的run_test()函数

30、时，以上函数将自动依次运行 endclass:my_env,55,共91页,module check(io_if.check_if io,input clock,rst,en,input 17:0 data_out_design_for_check);wire 17:0 hcic_out;/参考模型Hcic_full Hcic_full(clock,en,rst,io.data_i,hcic_out,);assign io.data_check_o=hcic_out;property p10;(posedge clock)(io.data_check_o=data_out_design_for

31、_check-2)|io.data_check_o=0;endpropertya10:assert property(p10);endmodule,OVM平台比较器,56,共91页,timescale 1ns/10ps module top;import ovm_pkg:*;import my_pkg:*;parameter clock_cycle=100;bit clock;bit rst;bit rst_check;io_if my_io();/装载接口 dut dut(.io(my_io),.clock(clock),.rst(rst),.en(rst_check);/装载DUT che

32、ck check(.io(my_io),.clock(clock),.rst(rst),.en(rst_check),.data_out_design_for_check(my_io.dut_if.data_o);/建议在验证程序顶级模块中一般采用继承ovm_test的类包装继承 ovm_env的类,OVM平台顶层模块,57,共91页,class my_test extends ovm_test;ovm_component_utils(my_test)/注册本类 my_env top_env;/装载环境-top_env function new(string name=my_test,ovm_

33、component parent=null);super.new(name,parent);ovm_report_info(,Called my_test:new);endfunction:new virtual function void build;super.build();ovm_report_info(,Called my_test:build);top_env=new();/初始化/建议在验证程序中可设定看门狗 set_global_timeout(1000000us);endfunction:build,58,共91页,virtual function void connect;

34、ovm_report_info(,Called my_test:connect);top_env.env_driver.v_io=my_io;/连接虚拟接口到驱动器的物理接口 endfunction:connect task run;my_transaction tx;tx=new();ovm_report_info(,Called my_test:run);top_env.env_stimulus.generate_stimulus(tx,2000000);/激励器产生20个事件 endtask:run endclass:my_test,59,共91页,initial begin run_t

35、est(“my_test”);clock=0;rst=0;rst_check=0;#(32*clock_cycle)rst=1;end always#(clock_cycle/2)clock=clock;initial begin$fsdbDumpfile(top.fsdb);$fsdbDumpSVA;$fsdbDumpvars(0,top,+all);end endmodule:top,60,共91页,启动验证工具,利用mentor的questasim，界面和操作类似于modelsim环境变量source/opt/demo/questasim.env启动命令vsim&,61,共91页,脚本方

36、式完成验证,vlib dac_hcic/创建库vlog+acc-f./rtl/ovm_rtl/compile_questa_sv.f-work dac_hcic-sv+cover/编译整个验证平台vsim-c dac_hcic.top-sv_seed 100-coverage-assertcover-assertdebug-sva-voptargs=“+acc”-pli/opt/springsoft/verdi/share/PLI/MODELSIM/LINUX/novas_fli.so/启动仿真view assertions/查看断言run-all/开始运行quit-sim/结束仿真,62,共

37、91页,compile_questa_sv.f,+incdir+/home1t/opt/questasim/questasim/verilog_src/ovm-2.1.2/src/home1t/opt/questasim/questasim/verilog_src/ovm-2.1.2/src/ovm_pkg.sv+incdir+/home/liuxp/dac/rtl/ovm_rtl+incdir+/home/liuxp/dac/rtl/dac_balise/dac_haf_cic/home/liuxp/dac/rtl/ovm_rtl/ovm_start.sv,63,共91页,结果查看,断言结果

38、查看代码覆盖率查看,64,共91页,断言结果查看Questasim下,65,共91页,代码断言结果查看Verdi下,Verdi（另外一个软件，专门用作波形查看和调试）下查看断言结果更加直观，箭头朝上就表示断言通过，朝下表示断言失败。,66,共91页,代码覆盖率查看,67,共91页,代码覆盖率查看,68,共91页,动态时序仿真：利用仿真器（Modelsim）和延迟文件(SDF文件)，通过反标节点延迟信息来仿真。需要的文件：1.布局布线完的网表文件2.布局布线后生成的SDF文件3.标准单元库和IO库的Verilog模型文件4.Testbench文件,动态时序仿真（后仿）,69,共91页,1.修改T

39、estbench，添加布局布线完导出的SDF文件2.创建新的工程3.添加修改好的Testbench文件top_tb.v4.添加布局布线完导出的网表文件fsk_layout.sv5.添加标准单元的Verilog模型文件/home/smic/smic_40/SCC40NLL_HS_RVT_V0p1a/verilog/SCC40NLL_HS_RVT_V0p1.v6.添加输入输出IO的Verilog模型文件/home/smic/smic_40/SP40NLLD2RN_3P3V_V0p2/verilog/SP40NLLD2RNP_3P3V_V0p1.v7.编译及仿真,动态时序仿真（后仿）步骤,70,共9

40、1页,Testbench中添加SDF文件,在Testbench中新建一个initial 块，通过系统函数$sdf_annotate()来读入SDF文件，并反标到网表每个节点上。具体代码如下：initial begin$sdf_annotate(“/home/liuxp/class/astro/SDF/top_pad.sdf”,top_tb.top_pad);end,Testbench 模块名称,实例化的顶层模块名称,71,共91页,后仿真波形,整体功能波形：延迟信息：,72,共91页,静态验证工具,静态时序分析Prime Time形式验证-Formality,73,共91页,静态时序分析Pri

41、meTime,PrimeTime是Synopsys的静态时序分析软件，常被用来分析大规模、同步、数字ASIC。PrimeTime适用于门级的电路设计。1.逻辑综合后网表 2.自动布局布线后网表,74,共91页,PrimeTime流程,1.设置查找和链接路径；2.读入并链接所要分析的设计；3.设置PVT和线上负载模型；4.设置基本的时序约束；5.检查所设置的约束以及该设计的结构。,75,共91页,PrimeTime工具启动,source/opt/demo/synopsys.envpt_shell（无图形界面）或者primetime&,76,共91页,命令输入区,77,共91页,PrimeTime

42、脚本 source pt.scr,set lib_path/home/smic/smic_65/SCC65NLL_HS_RVT_V1p1aset smic_stdlib_path$lib_path/synopsys/1.2v/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

43、/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*scc65nll_hs_rvt_ss_v1p08_125c_basic.db scc65nll_hs_rvt_ff_v1p32_-40c_basic.db SP65NLLD2RP_OV3_TTM_V0p2_ss_V1p08_125C.db SP65NLLD2R

44、P_OV3_TTM_V0p2_ff_V1p32_-40C.db“set symbol_library list SCC65NLL_HS_RVT_V1p1.sdbremove_design allread_verilog./syn/netlist/dac.sv“link_design daccurrent_design daclist_designsreport_cell,78,共91页,PrimeTime脚本 source pt.scr,set_operating_conditions-min_library scc65nll_hs_rvt_ff_v1p32_-40c_basic-min ff

45、_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 2.0 all_clocksset_clock_uncertainty-s

46、etup 2.0 clkset_clock_transition 2 get_clocks clkset_drive 0 list clk clk_in_pad set_load 5 all_outputsset_input_delay 5-clock clk-max remove_from_collection all_inputs get_ports clk_in_pad set_output_delay 5-clock clk-max all_outputsreport_constraintreport_timing,79,共91页,形式验证-Formality,所谓形式验证，就是通过比

47、较两个设计在逻辑功能是否等同的方法来验证电路的功能。Formality是Synopsys公司的产品，与PrimeTime结合起来使用。,80,共91页,形式验证-Formality,LogicCone,BB,BB,InputsOutputs from RegistersPrimary Input PortsOutputs from Black Boxes,Compare PointsInputs to RegistersPrimary Output PortsInputs to Black Boxes,Compare Point,A design contains Logic Cones an

48、d Compare Points,81,共91页,形式验证-Formality,Breaks the two logic circuits up into logic cones:End points(compare points)are primary outputs,registers,and black box inputs,82,共91页,形式验证-Formality,Compare points are then aligned:This process is called“compare point matching”End points of logic cones(compar

49、e points)are primary outputs,registers,and black box inputs,83,共91页,形式验证-Formality,Verify Design,For each matched pair of compare points Formality tries to:EitherConfirms same response for all possible input combinations.Marks point as“passed”OrFinds a“counter example”that shows different responseMa

50、rks point as“failed”,84,共91页,Formality流程,1.添加工艺库2.创建container3.读入参考库文件4.读入设计文件5.定义参考库和设计库6.连接7.开始比较,85,共91页,Formality工具启动,source/opt/demo/synopsys.envfm_shell（无图形界面）或者formality&,86,共91页,命令输入区,87,共91页,Formality source fm.scr,set lib_path/home/smic/smic_65/SCC65NLL_HS_RVT_V1p1aset smic_stdlib_path$lib