九零年代初，工程師已越過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!邏輯產品部們行銷經理)