九零年代初，工程师已越过1,000 Gates的设计，正朝着100,000 Gates次微米设计突破，此时EDA业界正迈入二十周年。客户开始要求更低的价格换到更高的容量，英特尔的创办人高登．莫尔由观察到现象所发表的工业界定律，已进入了第二十七个年头，对于更高容量的需求一样无法满足，但是能够促使这现象发生的工具却开始遇到瓶颈。

当逻辑验证(Logic Verification)占据其50％的工程时间，随着Gates数目增加，这比重还会持续上升，Simulation此时变成了Logic Verification上的速度障碍。在Gate-level过长的Run Times和设计规模的限制，严重影响整个时程，这些都是费用和困扰。在一个以指数成长的市场，这些损失的时间，最后都可以看成是错失机会的成本。

Formal Verification带来重大突破

在这同时，一群在麻州Chrysalis Symbolic Design的工程师开始思考，如何解决在次微米制成中百万Gate-count以上的设计中Logic Verification的挑战。 Regression simulation需要许多向量Vector，而Gate-level的Full-vector的Simulation变成耗时耗钱，这些工程师寻找新的方法和工具来加速设计过程，Formal Verification提供了一个可能的解决途径，但是工具尚待开发，且只有少数的先驱在这方面努力，希望把这样的观念由学术界带到市场上。

这些Chrysalis工程师的研究产生了一种新科技，这新科技叫做「Symbolic Logic」。 ，这群人在1993年推出最初的Equivalency Checking工具。 HP购买了第一套的Design VERIFYer，前达科技(Avant!)Formal Verification部门的行销经理Dave Guinther回忆：「在开拓Formal Verification市场之初，我们拥有可以解决客户痛苦的科技，但是人们不了解什么是Equivalence Checking、为什么需要Equivalence Checking，我们要教育使用者，让人们知道这是条未来必经的路。」

不过那一段时间并不长，在Design VERIFYer进入市场两年后，采用的客户开始迅速快速成长。 Guinther说：「我们找到了技术和技术支援的配合比例。Design VERIFYer让使用者每天都安稳的睡觉。」其他率先采用的公司包括了IBM、LSI Logic，和Sun Microsystem。

什么是Formal Verification

就像是EDA工具一样，Formal Verification加速了数位IC的设计和验证过程，Equivalence Checking工具提供了完整、独立的逻辑设计的验证，增加工程师的生产力，缩短了产品上市的时间。

Formal Method是深次微米ASIC和IC设计决策中影响最大的一环。身为Formal Verification工具，Equivalence Checking将参考设计和另一修改过的设计案例作数学运算，比较两者之间逻辑上是否相等，经过这样的过程，结果不证自明，因为整个设计已经在所有的逻辑条件下通过了验证。

受到排程参数限制(Schedule Constraints)的影响，在每一个Gate-level的版本上跑完所有的回归向量(Regression Vector)是不可能做到的。但是若只选择一个向量的子集合来做模拟，就牺牲了涵盖面，也提高漏抓程式错误的机会。若等到最后的Netlist来做验证，结果是问题必须到最后阶段才能发现，这有可能延迟Tape-out的时间。就是因为Equivalence Checking不需要用到向量，所以它比模拟的方式快上数千倍。

设计者发现，使用Formal Verification来代替回归方式模拟，可以将整个逻辑验证的时间从几个月、几周缩短到几小时。更强的是Design VERIFYer Equivalence Checking提供连续多种验证方式：RTL和RTL、RTL和Gate、Gate和Gate、Gate和RTL。工程管理者可以在很短的期限内，看到投资的报酬─更短的上市时间、减少验证的时间、在Tape-out之前找到问题、对设计的结果有信心。

现有和未来的科技

1999年，前达科技合并了Chrysalis Symbolic Design，这样的结果使得可以投入Formal Verification研发上的资源大为增加。前达的商业模式通常强调使用密集的研发人力，这正可以使Formal Verification部门的资源更充裕，有能力同时在现有和未来的产品做同步的研发。 Noel Strader博士，Avant!逻辑产品部门的商业策略负责人提到，「当这行业其他公司通常只靠一项产品生存，其后随着产品世代的交替，公司也慢慢老去。但是，我们有足够的财力让旧世代的产品自行淘汰，并用余力去研究新世代的科技，以满足客户对性能上不断成长的需求。 」

最新版本的Formal Equivalence Checking工具就是Design VERIFYer 3.0。其中含有OAS(Optimized Algorithm Selection)科技，这技术使Design VERIFYer扩大全晶片设计范围。 3.0版本中，使用者可以在整个设计流程的每一个步骤中做验证，它支援RTL，Gate，Switch和SPICE的表现方式。

CV功能选项可以做到SPICE模式和修订过的SPICE模式、Verilog或是VHDL之间的比较，他将电晶体模式(Transistor Model)和模拟模式(Simulation Model)间做比较，来保证出来的结果是彼此一致的。他可以轻易的比较修改过后的library cell，编译和验证的时间只要用到几秒，从此那种需要用到数周的测试环境和模拟向量的设定过程就可以省了。

Design VERIFYer 3.0使用和合成(Synthesis)工具完全不相同的方式来编译，因此绝不可能会漏掉与合成工具相同的错误。可以读取的格式包括Verilog,VHDL可合成模式，Verilog、VHDL、EDIF和NDL的Netlist。错误的来源也可以透过一种独特又强力除错环境轻易的找出来。

Design VERIFYer 3.0中OAS的技术将计算法则最佳化，以求得最好的执行效率，最低设备要求，使得工具可以轻易的处理复杂如SoC的设计。举例而言，一个三百万Gates的设计需要约十五小时的RTL的比较时间，现在透过OAS的技术可缩小到四十分钟。而且，计算法则是自动选取的，完全不需要使用者再花时间研究。 Design VERIFYer可以独自使用，不需要太多额外的设定。如果有逻辑错误发生，Design VERIFYer也会产生一个操作简易但是内容丰富的除错环境，透过这环境能很快指出错误逻辑的所在之处。

更且Design VERIFYer 3.0在Equivalence Checking之上又加了模式检查的能力，模式检查可以有效的完成模拟工作，又顾及各种设计细节上的小变化。模式检查可以在组成全晶片模型之前的Block Level帮助设计者除错去RTL程式上的错误。这样就可以在设计阶段发现功能上的错误，节省修复的成本。

如何才是完整Formal Technology厂商

模式检查还有第二项用途，透过简单的设定，来自动验证设计中重复出现的部分。模式验证可帮助找出模拟时的错误，也可以​​协助找出很难找的制造后期错误，诀窍在于独立各项造成失序的事件，这样的工作用模拟器或是逻辑分析工具很花时间，而模式检查可以利用使用者已知正确的条件，来找出一串可能造成错误的连续事件。

Lee LaFrance，前达Formal Verification的负责人，解释这样发展的方向：「一个提供Formal Technology的厂商必须要能同时提供Equivalence Checking和模式检查的功能，才算是一个完整Formal Technology厂商。」Formal Verification部门希望他们的产品超越单点工具的局限性，而能以整体性做考量，和Avant!的SinglePass设计流程从RTL到Silicon一气呵成。

藉由共享Milky Database的单一介面，Avant!创造了一项EDA业界的典范─SinglePass设计流程。这项设计的目的是减少因为逻辑设计和矽晶圆制造上的断层，而产生不断重复的流程。现在深次微米的时代中，超过20％的讯号延迟是由于线路相交所造成的，只有约20％的是闸的延迟，如果设计不能够考虑这样的现实，那么设计后在那种速度下能够工作的机会几乎是零。

设计团队现在所需要的方法，必须要能够在流程及早将实体效应考虑进来。只有消除那好似永无终止的逻辑设计回路，来检查实体的应用面，才能够达到对时序收敛的要求。

未来三年市场将成长一倍

由于Formal Verification科技和Design VERIFYer上市七年来的快速成长，整个市场已经达到了每年四千四百万美金的规模。更者，预料未来三来市场还有机会成长一倍，很明显的，设计者们已经开始看出这些工具背后所隐藏的更高价值。多年以来，Design VERIFYer已成功的打入了270个客户，许多公司将Equivalence Checking加入了他们的设计流程，和这些公司合作的结果，使Avant!有机会在彼此合作的21,000的案子中，完整的测试了工具的各种性能，在各种不同的设计流程中完成了上千个Tape-out，包括了ASIC，COT和微处理器。

「当我们说我们的工具是通过了生产的证明时，我们的的确接受了完整的考验。」LeFrance说，「只有一年的时间是不可能有像这样的大的案量来完成所有的验证。」许多客户会选择Design VERIFYer也是基于Design VERIFYer团队有这么丰富的经验。 「对于晶片上大部分的地方，含Cell Libraries在内，我们都有好多个Verilog模式，我们使用Design VERIFYer来证明所有的Library Models是相等的，不论是在行为层、结构层或是基于原始提案和UDP。在Layout的过程中，我们也开始在每一次Netists的改变后，针对Rebufferings、Clock Tree和Insertion做验证。这让我们能够以最快的速度找到以往发现不到的错误。 」Vitesse Semiconductor公司技术副总裁Steve Sheafor说。

就在Billerica，这个团队正准备开发下一代的Formal Verification工具，和过去一样，他们对于未来充满了期待。 「没有人知道下一个新方式之后，我们会到哪里，但是一定会很刺激。」Memmi说。

(作者任职Avant!逻辑产品部门行销经理)