這篇不是書評，這本書亦不是一般自學程式設計的電腦書，是一本涉及非常專門的知識，只有設計晶片才會用得上的技術課本。非行內人完全看不明白，這篇只是我學習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「心法」：
- cover和assert是同一塊鏡子的兩面。同一個property，cover就是not左個property的assert的counter example。assert就係not左個cover既unreachable proof
- Formal engine係一個breath-first咁去行所有的state space。assume同assert就係cut細個state space，cut走左illegal state，如果行到去specification果個state，咪就proof度囉。
- 一開波不要立即寫full proof，先由cover開始玩。唔用assume，剩係寫你想睇乜output，睇下formal engine可不可以back trace你想要的input，然後再慢慢fine-tune那些assume
- 用cover整好晒assume，就可以上去bug hunting，專心搵assert的counter example，最後才整full proof。用之前兩個steps的assume
- 唔好load太多code，太多assert同cover，要divide and conquer。有些tricks可以用，如cutpoint，abstraction，free variable等等