Synopsys Formality Workshop 2013

四月底忙里偷闲去参加了为期两天的Formality的workshop。讲师还是那个讲师，不过相比于2010年底的听的那次Formalityworkshop2005，内容有很大的调整和更新，尤其是使用Formality的策略和debug的各种方法技巧，都总结的比较清晰、可操作。推荐有机会去的同学们再去听一下。
有个小道消息是，Synopsys也正在开发测试他们的自动ECO方案，与LEC的类似。回来之后提炼了一下笔记，很粗略，供大家和自己参考。被我们部门的总监看到了，笑称Formality是个屌丝才用的软件，不值得花力气在上面。我问为啥，说之前有个项目用LEC发现了Formality没有发现的不同。好吧，综合和Formalcheck用同一家的软件，确实有点自圆其说的意思。大家有没有遇到Formality发现不了的问题呢？

-Possible results: succeeded/failed/inconclusive/not run

-Two types of failure: Flase Negative/True Negative

-Complete Formality scripts can be generated automaticallyfrom SVF

fm_mk_scriptmydesign.svf -o fm.tcl

fm_shell -ffm.tcl

-Synplify can generate SVF

-Logic Cone

Inputs:Registers/Primary Input Ports/Black Box Ouput Pins

Compare Points:Registers/Primary Output Ports/Black Box Input Pins

-set synopsys_auto_setup true

Can usesynopsys_auto_setup_filter to limit effect ofsynopsys_auto_setup

set synopsys_auto_setup_filter{hdlin_ignore_parallel_case}

-SVF is verified and applied since the phaseMatch

-Automatically determines multiple SVF file processing order(timestamp)

-Saved containers are portable across Formality releases

-Probe points allow one to compare nets in failing logic cones(self-defined compare points)

set_probe_points

verify-probe

-Multiple StageVerification

The fewer the designtransforms the eaiser to debug

When bringing up adesign it always easiest to debug each stage in turn

You can do this providedyou write a netlist and SVF for each step

-The guidance summary is the best place to start debug

report_svf_operation-status rejected -command reg_constant

report_setup_status

-Hard(inconclusive) Verification

set_verification_priority(SVP) [get_designs {*crc*}] # inDC

setsimplified_verification_mode true

-Get to failing points fast

setverification_effort_level super_low

-Multicore support

Up to 4 cores with asingle license

set_host_options-max_core

-RTL Hardware vs. Simulation mismatch

sethdlin_error_on_mismatch_message false

lappendhdlin_warn_on_mismatch_message FMR_ELAB-116

report_hdlin_mismatches

-Examples of mismatch

case pragmas

//synopsys full_case

//synopsys parallel_case

One can instructFormality to have same interpretation as DC

set hdlin_ignore_parallel_case false

set hdlin_ignore_full_case false

black box

undrivensignals

multiply drivennets

RTL nameinterpretation

guide_enviroment

-Sequential optimizations

clock gating

compile_ultr -gate_clock

set verification_clock_gate_hold_mode any(synopsys_auto_setup)

set verification_clock_gate_edge_analysis true(new)

registermerging

guide_reg_merging

verify r:/xxx1 r:/xxx2 (single pointverify)

set_constraint coupled $ref/a1_reg $ref/a2_reg(emergency work-around)

registerreplication

set compile_register_replication true (DCG,default false)

setcompile_register_replication_across_hierarchy true (DCG, defaultfalse)

guide_reg_duplication

set_user_match $ref/a1_reg$ref/a2_reg

verify i:/xxx1 i:/xxx2

set_register_replication -num_copies 2A_reg

register_replication_naming_style (default%s_rep%d)

phaseinversion

guide_inv_push

verify -invertedr:/xxx i:/xxx

set_inv_push/set_user_match-inverted

adaptiveretiming

compile_ultra -retime

pipelineretiming

constant registerremoval

guide_reg_constant

verify r:/WORK/top/potentially_constant_reg-constant0

set_constant $ref/a_reg 0

unread registerremoval

Matched unread compare points are not verifiedby default

set verification_verify_unread_compare_pointstrue

verify

report_matched_points -status unread

report_unmatched_points -statusunread

-Structural Transforms

Datapath

Tree transforms

Share transforms

Sum of products

Ungrouping

guide_ungroup

Uniquification

DC performs different optimizations sincedifferent contexts

Boundaryoptimization

Others

-DesignWare

DC use built-in DW, butFormality use that HDL_DWROOTindicates

-Hierarchical Verification

write_hierarchical_verification_script

Isolation

set_cutpoint -type pin $ref/inst/P

set_cutpoint -type pin $impl/inst/P

probe points/cut-points

probe: don't have to go back tosetup

cut: canonly be applied during setup

-ECO Verification

fm_eco_to_svf (UNIXcommand)

analyze RTL files and produce supplementary SVFguidance

generate_eco_map_file(FM command)

guide_eco_map

Synopsys Formality Workshop 2013相关推荐

Synopsys Formality 2018操作流程
Synopsys Formality 2018操作流程王_嘻嘻 2020-09-16 15:20:18 1940 收藏 26 分类专栏: eda工具使用经验文章标签: verilog 版权声明:本 ...
Synopsys全系列工具简介
Synopsys的产品线覆盖了整个IC设计流程,使客户从设计规范到芯片生产都能用到完备的最高水平设计工具.公司主要开发和支持基于两个主要平台的产品, Galaxy设计平台和Discovery验证平台. ...
synopsys工具介绍
作为一个IC设计的工程师,不懂这些,就比较悲剧了.时常会说DC一下,PT一下.那么他们的含义是什么呢? 注:http://www.2ic.cn/html/89/t-423489.html http:/ ...
Cadence和Synopsys工具介绍
参考博文:https://blog.csdn.net/qq_28284627/article/details/52062031 和 https://blog.csdn.net/palaciopku/a ...
探讨 | 目前SLAM存在的问题
点击上方"小白学视觉",选择加"星标"或"置顶" 重磅干货,第一时间送达本文转自|计算机视觉联盟又到了每周组会的时间了,这周主要是收集了 ...
深度增强学习方向论文整理
from:https://zhuanlan.zhihu.com/p/23600620 作者:Alex-zhai 链接:https://zhuanlan.zhihu.com/p/23600620 来源: ...
推荐系统CTR预估学习路线：引入注意力机制
推荐系统CTR预估学习路线:从LR到FM/FFM探索二阶特征的高效实现推荐系统CTR预估学习路线:利用树模型自动化特征工程推荐系统CTR预估学习路线:深度模型推荐系统CTR预估学习路线:引入注意 ...
word2vec原理_word2vec论文阅读笔记
word2vec算是NLP中的经典算法,之前在课程中简单的学过,但面试时经不起深问.痛定思痛,参考Jack(@没搜出来)的总结,笔者重点阅读了Mikolov的原始论文[1]和Xin Rong的详细推导 ...
SPDA-CNN:Unifying Semantic Part Detection and Abstraction for Fine-grained Recognition
SPDA-CNN:联合语义检测和提取用以细粒度识别最近在做细粒度分类和研读CVPR2016结果,看到这篇文章.做个笔记,方便自己回顾和与大家讨论. 1.摘要及引言多数的卷积神经网络缺少能够mode ...

Synopsys Formality Workshop 2013

Synopsys Formality Workshop 2013相关推荐

最新文章

热门文章