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