芯片驗(yàn)證的挑戰(zhàn)之一：理論上無(wú)限的驗(yàn)證空間
時(shí)間：2021-11-05 13:46:14
手機(jī)看文章
掃描二維碼
隨時(shí)隨地手機(jī)看文章
[導(dǎo)讀]如今，消費(fèi)者對(duì)芯片的特性要求以及驗(yàn)證的復(fù)雜度呈同樣的指數(shù)級(jí)增長(zhǎng)。例如，消費(fèi)者自然而然地會(huì)希望汽車(chē)芯片在汽車(chē)整個(gè)行駛過(guò)程中都是正常的，也并不期望因?yàn)樾酒瑔?wèn)題導(dǎo)致服務(wù)器宕機(jī)而無(wú)法訪問(wèn)到想要的數(shù)據(jù)。這些業(yè)務(wù)上的需求，正是驗(yàn)證最本質(zhì)上的驅(qū)動(dòng)。?以一個(gè)簡(jiǎn)單的交通燈控制器為例。在經(jīng)過(guò)一些市場(chǎng)...
如今，消費(fèi)者對(duì)芯片的特性要求以及驗(yàn)證的復(fù)雜度呈同樣的指數(shù)級(jí)增長(zhǎng)。例如，消費(fèi)者自然而然地會(huì)希望汽車(chē)芯片在汽車(chē)整個(gè)行駛過(guò)程中都是正常的，也并不期望因?yàn)樾酒瑔?wèn)題導(dǎo)致服務(wù)器宕機(jī)而無(wú)法訪問(wèn)到想要的數(shù)據(jù)。
這些業(yè)務(wù)上的需求，正是驗(yàn)證最本質(zhì)上的驅(qū)動(dòng)。?以一個(gè)簡(jiǎn)單的交通燈控制器為例。在經(jīng)過(guò)一些市場(chǎng)調(diào)研之后，我們明確了交通燈控制器的原始需求：
1、當(dāng)十字路口繁忙時(shí)，傳感器要檢測(cè)到這兩條街上的交通狀況。特定的時(shí)間內(nèi)，兩條公路上的交通燈應(yīng)該是公平的。2、每個(gè)方向燈應(yīng)保持綠色1分鐘。
在下圖這個(gè)有缺陷的設(shè)計(jì)中，Main street上如果一直都有車(chē)輛在行駛，那么會(huì)無(wú)限鎖死Elm street的交通。（這種問(wèn)題在總線設(shè)計(jì)中可能很容易發(fā)生）。當(dāng)然，這導(dǎo)致了Elm street的一場(chǎng)噩夢(mèng)。驗(yàn)證工程師的工作是發(fā)現(xiàn)這些設(shè)計(jì)缺陷，確保最終產(chǎn)品符合預(yù)期。如果不經(jīng)過(guò)完備的驗(yàn)證，這種帶有缺陷的設(shè)計(jì)會(huì)被翻譯成HDL，進(jìn)而翻譯成門(mén)級(jí)網(wǎng)表，直到安裝到十字路口，造成交通癱瘓。
數(shù)字芯片由很多上述這樣的邏輯門(mén)組成，驗(yàn)證工程師的工作就是通過(guò)復(fù)雜的仿真檢測(cè)出RTL實(shí)現(xiàn)和規(guī)格不一致的地方。
驗(yàn)證工程師面臨的第一大挑戰(zhàn)就是：RTL設(shè)計(jì)巨大的狀態(tài)空間。?芯片中存儲(chǔ)的內(nèi)容（例如register和memory）稱(chēng)為芯片當(dāng)前的狀態(tài)，其和芯片當(dāng)前的輸入組合成巨大的驗(yàn)證空間。芯片中的下一狀態(tài)由當(dāng)前狀態(tài)和設(shè)計(jì)輸入決定。為了徹底驗(yàn)證芯片的功能，我們需要覆蓋到芯片當(dāng)前狀態(tài)和設(shè)計(jì)輸入的組合。?同樣以上面提到的交通燈為例，只有2bit的內(nèi)部狀態(tài)，以及5個(gè)輸入端口，所以總的驗(yàn)證空間為4*32個(gè)。
為了解決驗(yàn)證空間隨著設(shè)計(jì)規(guī)模爆炸的問(wèn)題，和其它解決復(fù)雜問(wèn)題一樣驗(yàn)證工程師采用各個(gè)擊破的策略。一個(gè)典型的數(shù)字芯片可能有幾十萬(wàn)個(gè)當(dāng)前狀態(tài)和輸入信號(hào)。驗(yàn)證時(shí)沒(méi)有必要只以整個(gè)芯片為研究對(duì)象，而是對(duì)設(shè)計(jì)進(jìn)行劃分，然后在設(shè)計(jì)、驗(yàn)證、物理實(shí)現(xiàn)各個(gè)方面分別處理，最后進(jìn)行集成，方便管理，同時(shí)不管是在設(shè)計(jì)、驗(yàn)證還是物理實(shí)現(xiàn)上都處理地更加周全。
此外，芯片中可能還有許多狀態(tài)是非法場(chǎng)景，即理論上或者業(yè)務(wù)上設(shè)計(jì)不可能進(jìn)入的設(shè)計(jì)狀態(tài)。例如上面的交通燈控制器的輸出只可能是2’b01或者2’b10，即總的4*32個(gè)驗(yàn)證空間只有一半是合法的。
通過(guò)分析非法空間能夠減少驗(yàn)證的工作量，同時(shí)定義illegal場(chǎng)景有時(shí)也能夠斷言出設(shè)計(jì)的故障。
這些業(yè)務(wù)上的需求，正是驗(yàn)證最本質(zhì)上的驅(qū)動(dòng)。?以一個(gè)簡(jiǎn)單的交通燈控制器為例。在經(jīng)過(guò)一些市場(chǎng)調(diào)研之后，我們明確了交通燈控制器的原始需求：
1、當(dāng)十字路口繁忙時(shí)，傳感器要檢測(cè)到這兩條街上的交通狀況。特定的時(shí)間內(nèi)，兩條公路上的交通燈應(yīng)該是公平的。2、每個(gè)方向燈應(yīng)保持綠色1分鐘。
在下圖這個(gè)有缺陷的設(shè)計(jì)中，Main street上如果一直都有車(chē)輛在行駛，那么會(huì)無(wú)限鎖死Elm street的交通。（這種問(wèn)題在總線設(shè)計(jì)中可能很容易發(fā)生）。當(dāng)然，這導(dǎo)致了Elm street的一場(chǎng)噩夢(mèng)。驗(yàn)證工程師的工作是發(fā)現(xiàn)這些設(shè)計(jì)缺陷，確保最終產(chǎn)品符合預(yù)期。如果不經(jīng)過(guò)完備的驗(yàn)證，這種帶有缺陷的設(shè)計(jì)會(huì)被翻譯成HDL，進(jìn)而翻譯成門(mén)級(jí)網(wǎng)表，直到安裝到十字路口，造成交通癱瘓。
數(shù)字芯片由很多上述這樣的邏輯門(mén)組成，驗(yàn)證工程師的工作就是通過(guò)復(fù)雜的仿真檢測(cè)出RTL實(shí)現(xiàn)和規(guī)格不一致的地方。
驗(yàn)證工程師面臨的第一大挑戰(zhàn)就是：RTL設(shè)計(jì)巨大的狀態(tài)空間。?芯片中存儲(chǔ)的內(nèi)容（例如register和memory）稱(chēng)為芯片當(dāng)前的狀態(tài)，其和芯片當(dāng)前的輸入組合成巨大的驗(yàn)證空間。芯片中的下一狀態(tài)由當(dāng)前狀態(tài)和設(shè)計(jì)輸入決定。為了徹底驗(yàn)證芯片的功能，我們需要覆蓋到芯片當(dāng)前狀態(tài)和設(shè)計(jì)輸入的組合。?同樣以上面提到的交通燈為例，只有2bit的內(nèi)部狀態(tài)，以及5個(gè)輸入端口，所以總的驗(yàn)證空間為4*32個(gè)。
為了解決驗(yàn)證空間隨著設(shè)計(jì)規(guī)模爆炸的問(wèn)題，和其它解決復(fù)雜問(wèn)題一樣驗(yàn)證工程師采用各個(gè)擊破的策略。一個(gè)典型的數(shù)字芯片可能有幾十萬(wàn)個(gè)當(dāng)前狀態(tài)和輸入信號(hào)。驗(yàn)證時(shí)沒(méi)有必要只以整個(gè)芯片為研究對(duì)象，而是對(duì)設(shè)計(jì)進(jìn)行劃分，然后在設(shè)計(jì)、驗(yàn)證、物理實(shí)現(xiàn)各個(gè)方面分別處理，最后進(jìn)行集成，方便管理，同時(shí)不管是在設(shè)計(jì)、驗(yàn)證還是物理實(shí)現(xiàn)上都處理地更加周全。
此外，芯片中可能還有許多狀態(tài)是非法場(chǎng)景，即理論上或者業(yè)務(wù)上設(shè)計(jì)不可能進(jìn)入的設(shè)計(jì)狀態(tài)。例如上面的交通燈控制器的輸出只可能是2’b01或者2’b10，即總的4*32個(gè)驗(yàn)證空間只有一半是合法的。
通過(guò)分析非法空間能夠減少驗(yàn)證的工作量，同時(shí)定義illegal場(chǎng)景有時(shí)也能夠斷言出設(shè)計(jì)的故障。
下載文檔
