根据Moore定律，硬体的复杂度是每十八个月增加一倍，而工程师的设计生产力却跟不上这个速率。徒然增加设计团队的人力，却不能在根本的生产力工具上改进，只会提高整合的困难。这由目前各大型计画，超过一半的预算是花在整合（integration）与验证（verification）上，可以得知[Silburt98]。

目前用以保证系统设计品质的方法大致可分三种：传统的测试（testing）[BA00,KFNFN99]、模拟（simulation）[LK00]、与新近的技术：正规（formal）验证（verification）[CE81, CES86, Pnueli77]。测试是指在软／硬体产品已经生产出来后，将选定的输入信号送入待测物件（Device under Testing；DUT），以检验产品设计的正确与否。模拟则不需要用到实际的待测物件，而用一个数学模型代替，观察此数学模型的行为，以推断产品设计的正确与否。而最近渐渐受到重视的formal验证技术，则是完全在数学模型的抽象层次，企图证明系统设计架构的正确性。

“Formal”一词，缘起于“formal methods”，最早期的代表是IBM的维也纳研究中心所开发出来的VDM （Vienna Development Methods）[Jones90]技术，也就是用数学的符号，表达出系统设计的规格，从而减少工程师间错误沟通的可能性，进而提升系统设计的品质。

在过去数十年间，工程师结合了传统的测试与模拟的技术，保障了种类繁多的产品品质。在结合了先进电脑科技之后，现在可以用电脑分析产生特定的测试pattern序列，以达成特殊错误模型下的错误涵盖率（fault coverage）[BA00,KFNFN99]。而在高速电脑运行下，结合有限元素（finite element）分析法[Jin02]，更可以让工程师在虚拟的环境中，窥探多度空间的物体互动反应栩栩如生的动画，将系统设计的品质管理推升到了空前的境界，进而鼓舞了无穷的人类创意。

但是新世纪的破晓余晖下，上一个世纪的惊人工业成就，却也对新世纪的工程师们摔下了严苛的战帖。就以热门的单晶片系统（System on Chip，SOC）[RPS01]来说吧！依据M​​oore定理，每十八个月硬体的复杂度可以增加一倍，但工程师的产品设计能量却达不到这个增加的速率。而在单晶片系统中所涵载的大量记忆体，虽然可以支援智慧型（intelligent）嵌入式软体（embedded software）的制作，开拓了大量低价的嵌入式系统应用的美丽新愿景，却也更加深了软硬体整合验证的困难。如果单纯只靠测试的技术来保障系统设计的品质，则工程品质的管理将被推迟到产品设计的后期阶段，延宕了修改早期设计错误的契机，并大幅浪费人力／物力成本于不良的产品设计架构上。

而模拟的技术虽然可以在系统设计的早期阶段，让我们窥见其数学模型的行为轨迹，但考量到系统每增加一个位元（bit）的容量，其复杂度就增加一倍，因此在Moore定律的假设下，系统设计的复杂度势必以超指数（super-exponential）的速率成长。而验证工程师的生产力，在于借助先进电脑模拟技术，单位时间内能够检查的模拟行为轨迹，也只能相对缓慢的增加，因此面对今日高复杂度、高智慧型的系统设计工作，要以少数几条行为轨迹来推断系统所有行为的正确／安全性，实在与古人以管窥天、以蠡测海一般，非常容易就错过了种种的设计上的缺失遗漏。

反观formal功能验证的新技术，是在数学的层次上，以严谨的模型架构推导／证明出系统设计的正确性，可以全面关照到系统设计的每一个幽暗死角，从而保障系统设计的安全性，因此渐渐成为新时代系统设计中重要的技术。但国内工程界对这项新科技却认知不深，采用的更少。而作者在过去十余年间，一直专注于嵌入式系统自动验证技术的理论研究与工具开发，因此不自知深浅，愿意在此介绍此一领域的历史发展、最新技术、与未来走向。若有国内先进、新秀看了本文，能够激发灵感，投入此一新科技领域的开拓研究，就是达成了本文的目的。

历史背景

Formal验证的研究，植根于深奥的计算理论。从二十世纪初开始，始有computability与decidability的观念的探讨（探讨有限记忆体计算机是否能够计算某些问题的答案）[HU79]。到了第二次大战后，数位电脑应用一日千里，各种verification问题复杂度结构浮现成形[HU79]。 1977年，Amir Pnueli提出了运用时态逻辑（temporal logics）来遂行数位系统验证的理论架构[Pnueli77]。1981年，Clarke与Emerson等人又提出了今日普遍被接受的模型检验（model-checking）的理论架构与演算法[CE81,CES86]。

但真正开启了Formal 验证工业应用之门的关键技术，则为以下两项：第一项是BDD（Binary-Decision Diagram；二元决定图）技术[Bryant86]；这项技术最早是在IBM研究中心中使用，但是为工业机密，IBM以外不得而知，而IBM内相关的技术人员对BDD的许多理论也未深究。运用BDD技术，我们可以对数位系统的combinational（不含记忆体的）线路进行精简的高效率处理。到了1986年，CMU（Carnegie-Mellon University）的Randal Bryant才独立研发出了BDD与相关的高效率演算法，更对BDD的复杂度进行探讨，揭开了近年对formal验证技术热潮的序幕[Bryant86 ]。第二项关键技术是1990年，McMillan等人首先提出了运用BDD对含有记忆体的数位系统的模型检验演算法，并成功的验证出一个Intel三十二位元的Pipeline ALU线路设计[BCMDH90] 。此一线路之状态空间含有超过1020个状态。自此电脑科学与工程界才意识到，在地平线的那一端，电脑辅助系统发展的潜力正逐渐被释放出来了。

1994年，平地一声雷响起，Intel的Pentium CPU竟然出现了严重设计瑕疵[Pratt95]，迫使Intel收回成品，造成严重损失。而CMU的团队也适时的证明他们的BDD技术有能力检测出该项设计瑕疵[Bryant96]。这著名的Pentium bug，不只让人们了解到了新一代数位系统设计的复杂度，已经渐渐凌驾了传统的测试与模拟技术的掌握，更让人们见识到formal验证技术的未来潜力。

Formal验证目前最常被使用来作为除错（debug）的辅助工具，由于formal验证的系统行为模型通常都在比较抽象的高层次上描述，因此往往会较不精准，容易产生false alarm（也就是在实际系统设计中，并不会发生的错误，但在抽象层次模型中却会发生）。与传统的测试与验证技术相较，Formal验证的困难在于复杂度太高与基础理论艰深、入门不易。目前一般的看法，是在可预见的未来，测试、模拟与formal验证必须携手合作，才有可能应付不断攀升的设计复杂度。

在美国矽谷，新的formal验证的公司也如雨后春笋，试图将各种艰深的formal技术包装成可以让工程师便利使用的工具软体。而大型的EDA公司，如Cadence与Synopsys也各自有formal验证技术的工具软体贩售，而Intel公司也以坚强的formal验证团队来保障他们产品的领先地位。

Formal验证的技术流派

以下介绍几种常见的自动化验证技术：

定理证明（Theorem-proving）

定理证明又称为定理检验（proof-checking）[CL73]，源自于AI（Artificial Intelligence）研究[BF82]的一个流派。其主要概念，是将系统的设计写成逻辑公理（axioms）与假设（assumption），将要验证的性质写成定理（theorem），然后依据逻辑理论、集合论、数论等架构，运用电脑程序，推导逻辑反证（refutation）定理，以证明系统设计的正确性。由于基础的理论架构（如一阶逻辑[first-order logics]、集合论、数论等）的定理推导，都是不具有演算法的undecidability问题，因此在定理证明的架构下，通常都是由验证工程师规划一系列的lemma，由这些lemma串连起来，以证明最终的目的定理（也就是目标验证性质）。然后在工程师的导引下，由theorem-prover来证明这一个个的lemma。目前著名的Theorem-prover,如德州大学的Nq Thm[BM79]、SRI(Stanford Research Institute)的PVS[ORRSS96]、还有高阶逻辑(Higher-order logics)的Isabella[NPW02]。

由于要能够妥善发挥theorem-prover的功效，必须对各种基础理论有着通透的了解，因此定理证明的验证工程人员是非常不容易训练的，通常至少要有博士学历与多年的工具使用经验。

模型检验

模型检验[CE81,CES86]是将系统行为表达成有限状态图（finite-state graph），再将要证明的性质表达成时态逻辑，然后运用以电脑程式写成的演算法，来自动计算性质的成立与否。这是全自动验证的理论架构，因此最适合普及于一般工程师使用。目前最知名的工具，有CMU（Carnegie-Mellon University）与Cadence发展的SMV系统[McMillan92]、University of Colorado发展的CUDD[CUDD01]、及Cadence发展的FormalCheck。比较老的系统，还有Bell Labs的SPIN[Holzmann97]。

即时系统与嵌入式系统的模型检验

传统的模型检验理论，只能检验事件的先后顺序，而不能检验事件之间时间长短的关系。这对于即时系统、或分散式系统多时钟系统的自动验证，就显得​​不足。在1990年，Alur、Courcoubetis、与Dill对具有多重稠密性（dense）读值时钟的真时系统，提出了第一套时态逻辑验证演算法[ACD90]。在接下来数年，理论界与工程界还持续在这新发现的兴奋状态中，并将这套架构扩充到含有多元稠密性变数（如时间、温度、高度、速度）的混合式系统（ybrid Systems）[ACHH93、ACHHHNOSS95]。目前这类工具的应用范围多数还是在低层（如physical layer、data-link layer）的通讯协定（communication protocol）的自动验证上。

目前对即时系统的模型检验，较知名的工具有Uppsala大学的UPPALL[PL00]、VERIMAG的Kronos[BDM98]、台湾大学的red[Wang03]、与中正大学的SGM[WH02]。混和式自动机的模型检验，知名的工具有Hytech[ACHH93]。

等价检验（Equivalence-checking）

等价检验[HC98]是最近这几年应用非常成功的formal验证技术。它可以帮助工程师检验RTL（register-transfer level）与gate level两层间的硬体结构描述是否一致。著名的软体，如Verplex公司的Conformal。

符号式模拟（symbolic simulation）

符号式模拟[SB95]又称为semiformal验证，是利用逻辑的公式来抽象表达一个行为轨迹的集合，而在模拟的过程中，同时操控这抽象集合的前进，并侦测集合中行为的安全性。至于在一个步骤中，要涵盖哪些行为轨迹，又要舍弃哪些行为轨迹，可以由使用者来决定，也可以由演算法来控制，达到验证资源运用的弹性。因为这项技术同时使用了formal验证的技术（如BDD等），又使用了模拟的概念，因此称为semiformal的验证。其优点在于结合了模拟技术的低复杂度，与formal验证的高层次抽象性。因此在模拟的过程中，可以同时监测许多行为轨迹的安全性，并有利于快速提高行为的涵盖率（coverage）。

SAT检验

SAT是satisfiability的缩写，代表一个逻辑公式是否有解，或是否等价于false。在过去数十年间，纯数学领域内与人工智慧领域内，都已经累积了许多逻辑公式种类（subclass）的SAT检验程序工具软体，如命题逻辑（propositional logics）、一阶逻辑（first-order logics ）、Presburger逻辑、Quantified命题逻辑。这些种类的逻辑公式的satisfiability问题，在理论上都承载着极高的复杂度，但在各种程式设计技巧下，对实际工程案例却往往表现出优异的效能。譬如对命题逻辑的satisfiability问题，目前最好的SAT检验工具往往可以处理数百、数千个变数的逻辑公式；反观BDD处理程序，却往往只能处理几百个变数的逻辑公式。 SAT检验技术可以视为对BDD技术的反动，在前几年对BDD处理程序的研究热潮过后，现在研究人员又回投到传统的SAT检验研究文献中去寻宝了。

有限模型检验（bounded model-checking）

此项技术与符号式模型检验非常类似，差别在于有限模型检验[BCCZ99]在每一个步骤都涵盖了所有的轨迹行为，从来都不舍弃任何行为轨迹。因此这项技术是全自动化的，全面性的侦错。一般来说，这项技术都是结合了SAT检验技术而不使用BDD技术，但目前并没有有效的方法可以决定需要执行多少步骤，才能检验出系统设计所有的可能错误。因此，这项技术目前适合用以侦测浅层的设计错误（在开机少数步骤后，就有可能发生的错误）。

组合式验证（compositional verification）

将一个复杂的问题，利用分进合击（divide-and-conquer）的策略，拆卸成简单的子问题逐一解决，然后再组合出整体的解决方案，原本是设计方法上的重要抽象化策略。譬如我们会将大型软体系统分工为不同的子系统，再分为不同的功能程序（procedure），然后借着程序元件的品质保证，来分层组合出整体系统的品质保证。此一策略在SoC硬体设计的IP元件分类上，也可以发现。同样的，我们对系统验证，也很自然地会依循组合式设计的策略，发展出组合式验证的策略。

这部分最早期的工作，有UNITY上的平行程式验证架构[CM88]、假设／保证（assume-guarantee）的验证架构、Reactive Module的理论[AAGHKMMMKW01,AH99]、还有UC-Berkeley的interface理论等等。一般来说，是希望在一个尽量宽松假设（assumption）条件架构下，去证明不同元件组合后的系统性质。

Assertion-based验证

Assertion是写在系统模型的档案中的条件限制，往往以注解（comment line）的形式出现。在执行验证任务时，要未经formal验证训练过的工程师写出必须验证的性质，或从自然语言写出的系统规格中抽取出要验证的性质，往往都是非常困难的。Assertion的机制，就是让工程师可以在设计系统时，依照assertion的语法，把他心中对环境的假设、对元件行为的要求，都即时地写录下来，成为系统设计的comment line，而与系统设计档案同时存在，这些assertion以后就可以成为simulation、或自动验证时重要的specification撰写依据。

反例的分析(counterexample analysis)

在计算formal验证的过程中，许多重要的模型行为轨迹资讯都累积在电脑记忆体中了。因此不论验证的结果是「是」（安全）还是「否」（不安全），这些累积的行为轨迹资讯都可以进一步协助我们改良系统的设计。反例分析[CGJLV00]就是当发现验证的结果是否定时，自动验证软体可以提供适当的建议资讯，或者让我们知道如何可以修改系统行为以满足规格的要求，或对系统提供更精确的数学模型以求得更精确的验证结果。

此外，这类分析也可以在加入成本、机率的概念后，进行危机成本分析，帮助我们评估不同修改方案的可行性[JM01]。

Formal验证的未来走向

虽然过去十余年间，formal验证的研究与应用都呈现了爆炸性的成长，但与传统的测试、模拟技术相比，目前formal验证还是无法承担系统验证的主要任务，许多系统设计公司，仍然倚赖测试、与模拟为主要的品质保证手段。未来我们预计，formal验证的许多技术会被自动化，并且被测试、模拟等技术所吸纳，而大幅提升测试与模拟的智慧功能。譬如，目前思源科技（Springsoft）与NOVAS公司所开发出来的Debussy系统，就结合了formal验证的技术，而对系统设计的debug功能提供了良好的智慧型附加价值。

但话又说回来了，formal验证技术起飞也只是最近十余年间的事。与传统的测试、模拟技术相比，formal验证还只是在幼年期而已。随着相关工具的自动化、商品化，以及各种formal验证的工业标准出现（如Accellera委员会所审定的新assertion语言标准，也就是IBM的Sugar[sugar02]），也将促进新formal验证工具效能的进一步提升，而与测试、模拟更成为缺一不可的三位一体品质管制方案。

要对抗不断攀升的巨大设计复杂度，Formal验证的趋势已是非常明显可见的，但对一个学术界的研究人员而言，其重要性与挑战性更是充满了不断的诱惑，就好比看了那巍峨的高山，就想像着攀越顶峰，呼吸着寂静爽洌的空气，在宇宙微妙玄通的真理与渺小的人间世，建立起不可思议、无可言喻的关连。

（作者为国立台湾大学电机工程学系副教授）

〈参考资料

[AAGHKMMMKW01] L.d. Alfaro, R. Alur, R. Grosu, T.A. Henzinger, M. Kang, R. Majumdar, F. Mang, C. Meyer-Kirsch, B.Y. Wang. Mocha: A Model-Checking Tool that Exploits Design Structure. ICSE'01.

[ACD90] R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems, IEEE LICS, 1990.

[ACHH93] R. Alur, C.Courcoubetis, T.A. Henzinger, P.-H. Ho. Hybrid Automata: an Algorithmic Approach to the Specification and Verification of Hybrid Systems. in Proceedings of Workshop on Theory of Hybrid Systems, LNCS 736, Springer-Verlag, 1993.

[ACHHHNOSS95] R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138(1995) 3-34, Elsevier Science B.V.

[AH99] R. Alur, T.A. Henzinger. Reactive Modules. Formal Methods in System Design 15:7-48, 1999. Also in the proceedings of the 11th IEEE LICS'1996, pp. 207-218.

[BA00] M.L.J. Bushnell, V.D. Agrawal. Essentials of Electronic Testing for Digital, Memory, and Mixed-Signal VLSI Circuits, Kluwer Academic Publishers, 2000.

[BCCZ99] A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. TACAS 1999, LNCS 1579, Springer-Verlag.

[BDM98] M. Bozga, C. Daws. O. Maler. Kronos: A model-checking tool for real-time systems. 10th CAV, June/July 1998, LNCS 1427, Springer-Verlag.

[BF82] A. Barr, E.A. Feigenbaum. The Handbook of Artificial Intelligence, Pitman, 1982.

[BM79] R.S. Boyer, J.S. Moore. A Computational Logic, Academic Press, 1979.

[Bryant86] R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., C-35(8), 1986.

[Bryant96] R.E. Bryant. Bit-level analysis of an SRT divider circuit. In Design Automation Conf., pages 661--665, 1996.

[CE81] E. Clarke and E.A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic, Proceedings of Workshop on Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.

[CES86] E. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal-Logic Specifications, ACM Trans. Programming, Languages, and Systems, 8, Nr. 2, pp.~244--263.

[CGJLV00] E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-guided abstraction refinement. In Computer-Aided Verication, LNCS 1855. Springer-Verlag, 2000.

[CL73] C.-L. Chang, R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving, Academic Press 1973.

[CM88] K.M. Chandy, J. Misra. Parallel Program Design. Addison-Wesley, 1988.

[CUDD01] http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html

[HC98] S.-Y. Huang, K.-T. Cheng. Formal Equivalence Checking and Design Debugging, Kluwer Academic Publishers, 1998.

[Holzmann97] G. Holzmann. The model checker SPIN, IEEE Transactions on Software Engineering, Vol. 23, pp. 279--295, 1997.

[KFNFN99] C. Kaner, J.L. Falk, H.Q. Nguyen, J.Falk, H.Q.Nguyen. Testing Computer Software, Wiley, John & Sons, 1999.

[Jin02] J. Jin. The Finite Element Method in Electromagnetics, John Wiley & Sons; 2nd Edition edition (June 2002).

[JM01] S. Jha, J. M. Wing. Survivability Analysis of Networked Systems, ICSE 2001. IEEE press.

[Jones90] C.B. Jones. Systematic Software Development using VDM, 2nd edition, Prentice Hall, 1990.

[LK00] A.M. Law, W.D. Kelton. Simulation Modeling and Analysis, 3rd edition, McGraw Hil, 2000l.

[McMillan92] K. L. McMillan. Symbolic model checking - an approach to the state explosion problem. PhD thesis, SCS, Carnegie Mellon University, 1992.

[NPW02] T. Nipkow, L.C. Paulson, M. Wenzel. The Tutorial on Isabelle/HOL, LNCS 2283, Springer-Verlag.

[ORRSS96] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, M.K. Srivas. PVS: Combining Specification, Proof Checking, and Model Checking, CAV '96, LNCS 1102, Springer-Verlag.

[PL00] P. Pettersson, K.G. Larsen. UPPAAL2k. Bulletin of the European Associatoin for Theoretical Computer Science, vol. 70, pp.40-44, 2000.

[Pnueli77] A. Pnueli, The Temporal Logic of Programs, 18th annual IEEE-CS Symp. on Foundations of Computer Science, pp. 45-57, 1977.

[Pratt95] V. Pratt. Anatomy of the Pentium Bug, TAPSOFT'95: Theory and Practice of Software Development, LNCS 915, Springer-Verlag.

[RPS01] P. Rashinkar, P. Paterson, L. Singh. System-on-a-chip Verificatoin, Methodology and Techniques, Kluwer Academic Publishers, 2001.

[SB95] C.-J.H. Seger, R.E. Bryant. Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods in System Designs, Vol. 6, No. 2, pp. 147-189, Mar. 1995.

[Silburt98] A. Silburt, Nortel, DesignCon98.

[sugar02] http://www.haifa.il.ibm.com/projects/verification/sugar/

[Wang03] F. Wang. Efficient Verification of Timed Automata with BDD-like Data-Structures, to appear in proceedings of the 4th VMCAI (Verification, Model-Checking, and Abstract-Interpretation), LNCS 2529, Jan. 2003.

[WH02] F. Wang, P.-A. Hsiung. Efficient and User-Friendly Verification. IEEE Transactions on Computers, Jan. 2002.〉