Archives

Formal Verification – Erik Seligman, Tom Schubert

這篇不是書評,這本書亦不是一般自學程式設計的電腦書,是一本涉及非常專門的知識,只有設計晶片才會用得上的技術課本。非行內人完全看不明白,這篇只是我學習formal verification(形式化驗證)的心得和筆記,所以我亦不期望有什麼讀者。

什麼是Formal Verification?首先要講什麼是dynamic verification,設計晶片不同寫程式,寫程式有bug很簡單,除錯出patch沒有什麼大不了。晶片有bug就很大件事,因為要更正問題,就要重新tape-out多一次,去做一個全新的mask。可以想像製造晶片好印黑膠碟,先要整有一張母碟,然後才可以覆印,mask就是silicon的母碟。傳統上測式晶片設件主力用simulation(即dynamic verification),要花很多人力物力寫個testbench出來,然後模疑晶片所有的input同output。這是一個非常嚴格的工序,因為一個bug也不可以走漏。晶片出了街之後,fix一個bug的成本是幾百萬美元。寫testbench同寫普通software沒有太大分別,只不過測試硬件比測試軟件嚴格很多。Formal Verification則是用另一個方法去測試硬件,不用寫code,寫formal specification,再用數學邏輯理論,去證明硬件的設件必定等於那個specification。完全不同的思考方法,完全不同的用途。Formal Verification可以測試出simulation找不出來的bug,始終simulation並不是exhaustive,不過formal有很多限制,設計不能太大不能太深,始終formal proof係一個NP-complete problem。

多年來formal一直只是學術研究,真正的商業應用,大約五六年前才開始。早期的formal tool非常難用,常常被戲說要博士才懂用,很多designer聽見便敬而遠之。直至JasperGold的推出,formal才開始普及化,這些年來JasperGold手執牛耳,一枝獨秀差不多等同於formal的代名詞。早兩年我也嘗試過學formal,不過當年JasperGold的license太貴,我們細公司買不起,只好用了一個很差很難用的IFV,結果學師未成不了了之。去年我公司被一個大公司收購了,economy of scale讓我們有多好多tools用,今個project終於有機會用到JasperGold,同IFV相比簡直是天堂和地獄,「工欲善其善,必先利其器」,其實formal一點也不難,我花了兩星期便滿師,可以學懂簡單的formal specify,去proof我個design不會有dead lock。如果要用simulation作同樣測試,因為太多corner cases,是一件非常痛苦的差事。現在用formal去做,幾行code寫完,是一件很好玩的玩意。

我一直都有follow開formal的paper和tutorial,雖然沒有實戰經驗但formal理論大至明白,用新tool不過是學syntax,很快上手。我公司的formal expert介紹我看這本《Formal Verification》課本,這本書是三位Intel工程師編寫的,由淺入深講解很有系統地如何應用formal verification,真正的hard-core技術含量不多(技術東西可以自已看document),反而更像是過來人分享心得和經驗。這本書九成是老生常談,平時睇tutorial睇paper都學過聽過,不過餘下的一成非常有用,讓我茅塞頓開,很多看已paper不明白人家為什麼一定要這樣做的地方,經他一解釋完全明白,一理通,百理明。這本書可以說是我formal的啟蒙老師,任何一個初學formal者必定要看。市面上formal的textbook一隻手數得完,因為formal是太專門的技術,譎想想學就要交很貴學費請consultant去教,不過我認為這本書比consultant教得更好,因為作者有真正的實戰經歷,不似consultant般大多紙上談兵。

以下是我認為書中有用的formal「心法」:

  1. cover和assert是同一塊鏡子的兩面。同一個property,cover就是not左個property的assert的counter example。assert就係not左個cover既unreachable proof
  2. Formal engine係一個breath-first咁去行所有的state space。assume同assert就係cut細個state space,cut走左illegal state,如果行到去specification果個state,咪就proof度囉。
  3. 一開波不要立即寫full proof,先由cover開始玩。唔用assume,剩係寫你想睇乜output,睇下formal engine可不可以back trace你想要的input,然後再慢慢fine-tune那些assume
  4. 用cover整好晒assume,就可以上去bug hunting,專心搵assert的counter example,最後才整full proof。用之前兩個steps的assume
  5. 唔好load太多code,太多assert同cover,要divide and conquer。有些tricks可以用,如cutpoint,abstraction,free variable等等

Leave a Reply