yuanpin318的个人空间 http://blog.eetop.cn/13812 [收藏] [复制] [分享] [RSS]

日志

Formality basic

已有 90 次阅读2019-6-26 15:59 |个人分类:Misc|系统分类:芯片设计

1. 为什么要formal verification
   比较两个design的function是否一致
   RTL 功能正确: function verifiation:  UVM testbench + simulation
       工具: systemverilog, UVM, VCS, NCSim
   1.1 比较对象
       RTL Vs Prelayout_Netlist,
       prelayout_netlist Vs post_p&R _netlist
       post_p&R_netlist Vs detail_route_netlist
   1.2 术语
       reference design: 功能正确,作为比对正确的参照物,又称在golden
       implementation design: 设计过程中改变过的design,是检查的对象
       container: design和libraries的database, 包括了Hard macro,综合用的标准库
                  默认的reference container的名字是r
                  默认的implementation container的名字是i
                  design的信息可以保存在container里面,下次可以直接读入container
    1.3 reference design假定是功能正确的
        formality用来检查implemation design是否和reference design一致
        是采用数学方法进行穷尽检查的一种比对的方法,没有corner case
        不需要test vector, design转化成logic cones的连接
        通过算法在每个logic cone的输入加上激励,比较输出是否一致,并不需要test vector
    1.4 compare points: primary output, Register或latch的输出,bbox的input
                  还有一些其它的不常用的比对点: 多驱动的net,组合逻辑环的cutpoint
    1.5 logic cone:
             输入可以时Primary Input, 寄存器或锁存器的输出, BBOX的Output pin
             输出是compare points
             formality把design分割成logic cone
            
2. Flow Overview
   2.1 Partition: 把reference和implementation design分割成logic cones和compare points
       Read Reference design(REF), implementate design(IMP) and libary(LIB)
   2.2 Match: 把REF和IMP中的compare points建立映射关系
              实际操作中,大多数的comare points是通过名字来match的,例如a_reg[31] Vs a_reg_31_
                         否则,需要guidance information, 手动指定match或比对的规则(rule)
               所以,match的结果是: 紫色代表matched cone, 绿色代表用户定义的matched cone,红色代表unmatched cone
              
   2.3 verify: 检查每对compare points的逻辑功能是否一致
                    结果: 黑色代表passing cone, 红色代表failing cone, 蓝色代表unmatched cone
                   
                    对于unmatched cone,可以设成不要比对(但结果可能不正确)
   2.4 Debug: 有GUI方式和report的方式
                     在match或verify的阶段,如果有unmatched或failed cone,就要进行debug
                     一种是使用GUI的方式,打开对应的unmatched或failed cone,检查是否一致
                                                        也可以在input pattern list中选择pattern,加到logic cone的input pin上,检查逻辑是否一致
                     
3. 使用formality
   3.1 启动
       a. batch mode: fm_shell -gui -f runme.fms | tee runme.log
       b. gui: formality
       c. 在batch mode启动GUI: fm_shell(setup) > start_gui
       d. 查看帮助文件: fm_shell -help
   3.2 加载guidance
       综合时,DC会自动生成一个svf文件,其中记录了一些优化后的信息,例如被去除的逻辑,被改名的寄存器
       formality可以通过svf获得更好的match
       "set_svf default.svf"
   3.3 读入reference design + libs + "set_top",使用"-r"的选项
       set_top可以设置要检查的最顶层,并且进行elaborate把top level下的design自动构建起来
       "read_verilog -r alu.v"
       "set_top alu"
   3.4 读入implementation design + libs + "set_top",使用"-i"的选项
       "read_db -i lsi_10k.db"
       "read_verilog -i alu.fast.vg"
       "set_top -auto"
   3.5 setup
       做一些setting. 例如,implementation中会包含DFT的信息,而RTL并没有这一部分,必须mask,不对这部分进行比对
       例如JTAG, SCAN的逻辑
   3.6 match & verify
       a.
       b. 可以省略match, 直接"verify",这个命令可以做match+verify
   3.8 debug

评论 (0 个评论)

facelist

您需要登录后才可以评论 登录 | 注册

关闭

站长推荐上一条 /2 下一条

关于我们|联系我们|ET创芯网 ( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2019-8-23 02:09 , Processed in 0.058017 second(s), 9 queries , Gzip On, Redis On.

Powered by Discuz! X3.4

© 2001-2017 Comsenz Inc.

返回顶部