formality简介

精品文档 1欢迎下载 Formality 简介 Formality synopsis 的工具 我们常说的形式验证 formal check 都是用它做的 作用就是比较两者 r i 在功能上是 否一致 跟时序一点儿关系都没有 在数字 ic 的 flow 中 一般会做两次 formal check 一 rtl 对 DC netlist 做一次 二 DC netlist 对 PR 后的 netlist 做一次 先看个 rtl 对 DC netlist 的脚本 Formal check for Capture vhd rtl vs dc nlist set TOP REF Capture set TOP IMP Capture set REF NAME Capture vhd set IMP NAME Capture v set REF PATH home project 9602 360 100 Dig d1 work jh synop199 rtl set IMP PATH home project 9602 360 100 Dig d1 work jh synop199 dc1 nlist 精品文档 2欢迎下载 set RPT home project 9602 360 100 Dig d1 work jh synop199 fm rpt set hdlin dwroot edatools synopsys syn vX 2008 9 SP4 set verification failing point limit 2000 set synopsys auto setup true set svf home project 9602 360 100 Dig d1 work jh synop199 dc1 default svf set search path home project 9602 360 100 Dig d1 synop199 edatools synopsys syn vX 2008 9 SP4 libraries syn read db chrt35 ss 75 1pt3 SYNOPSYS2 MMSIM db dw foundation sldb read vhdl r REF PATH REF NAME l work RPT read design rpt set top TOP REF RPT set top rpt report hdlin mismatch RPT rpt hdlin mismatch rpt read verilog i IMP PATH IMP NAME l work RPT read design rpt set top TOP IMP RPT set top rpt set constant type port r 0 set constant type port i 0 match RPT match rpt 精品文档 3欢迎下载 report matched points RPT matched point rpt report unmatched points RPT unmatched point rpt report loops limit 0 unfold RPT loops rpt verify 以上内容可以放在一个文件里作为脚本 调用方法就是在 fm work 下 fm shell f scripts fm rtl2dc tcl 如果成功要看详细信息或者失败要 debug 的话 再输入 start gui 进入 GUI 模式 下面是 DC netlist 对 PR netlist 的 formal check Formal check for Capture vhd DC vs PR set TOP REF Capture set TOP IMP Captureture setset REF NAMEREF NAME C Capture v set IMP NAME Capture postlayout v set REF PATH home project 9602 360 100 Dig d1 work jh synop199 dc1 nlist set IMP PATH home project 9602 360 100 Dig d1 work jh synop199 astro 精品文档 4欢迎下载 set RPT home project 9602 360 100 Dig d1 work jh synop199 fm rpt n2n set hdlin dwroot edatools synopsys syn vX 2008 9 SP4 set verification failing point limit 2000 set synopsys auto setup true set svf home engineer gump work jh capture dc default svf set search path home project 9602 360 100 Dig d1 synop199 edatools synopsys syn vX 2008 9 SP4 libraries syn read db chrt35 ss 75 1pt3 SYNOPSYS2 MMSIM db dw foundation sldb read verilog r REF PATH REF NAME l work RPT read design rpt set top TOP REF RPT set top rpt report hdlin mismatch RPT rpt hdlin mismatch rpt read verilog i IMP PATH IMP NAME l work RPT read design rpt set top TOP IMP RPT set top rpt set constant type port r 0 set constant type port i 0 match RPT match rpt report matched points RPT matched point rpt 精品文档 5欢迎下载 report unmatched points RPT unmatched point rpt report loops limit 0 unfold RPT loops rpt verify 以上内容可以放在一个文件里作为脚本 调用方法就是在 fm work 下 fm shell f scripts fm dc2pr tcl 如果成功要看详细信息或者失败要 debug 的话 再输入 start gui 进入 G