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)