根據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]來說吧！依據Moore定理，每十八個月硬體的複雜度可以增加一倍，但工程師的產品設計能量卻達不到這個增加的速率。而在單晶片系統中所涵載的大量記憶體，雖然可以支援智慧型（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，如德州大學的NqThm[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撰寫依據。

反例的分析（counter-example 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.〉