一直以來(lái)對(duì)MTK北京團(tuán)隊(duì)做的關(guān)于Cache一致性驗(yàn)證的方案有深刻印象，2019年當(dāng)時(shí)的一篇論文“An Enhanced Stimulus and Checking Mechanism on Cache Verification”（接下來(lái)該論文簡(jiǎn)稱PP-MESH）采用的是MESH預(yù)測(cè)的方法，對(duì)cache的數(shù)據(jù)做好準(zhǔn)確預(yù)測(cè)和檢查。

2022年的時(shí)候我們V3課程中的聯(lián)發(fā)科學(xué)員，還跟著我們一同回顧了這篇論文中涉及到的一些技術(shù)，給當(dāng)時(shí)正在做cache一致性驗(yàn)證的其他同學(xué)提供了思路。我們以往做的各個(gè)方向的技術(shù)分享和論文回顧，都有保存在V3課程視頻中。

這次我們要談的論文DVCon 2022 “CAMEL: A Flexible Cache Model for Cache Verification”（接下來(lái)該論文簡(jiǎn)稱PP-CAMEL），其背景正是基于PP-MESH做的更新，我們也可以借此以了解對(duì)于一個(gè)復(fù)雜設(shè)計(jì)而言，如何考慮規(guī)劃其參考模型，在實(shí)際項(xiàng)目中有哪些需要權(quán)衡的地方。

總體而言，在驗(yàn)證L1 cache system （L1SYS）的過(guò)程中，L1SYS的機(jī)構(gòu)被拆分為多個(gè)模塊，包括shadow command buffer, store buffer, sram, line filling buffer, evinctionbuffer, prefetch buffer，而根據(jù)不同thread訪問(wèn)數(shù)據(jù)時(shí)的cache hit/miss的情況和數(shù)據(jù)經(jīng)過(guò)L1SYS各個(gè)模塊的流向，又將L1SYS的不同數(shù)據(jù)讀寫行為定義為了各種情況（例如in-order, out-of-order, with-losses, any-in-order, either-in-order, MISO, with-redundancy等）。這種數(shù)據(jù)從點(diǎn)到點(diǎn)的流向，就構(gòu)成了DVCon 2019的這篇論文中數(shù)據(jù)檢查思想的框架，即根據(jù)每一個(gè)data stream的不同特征，分別對(duì)input stream, output stream做數(shù)據(jù)流向的標(biāo)注。



由于這種精細(xì)規(guī)劃和預(yù)測(cè)的方式，MESH檢查可以做到周期級(jí)的準(zhǔn)確（cycle-accurate），從下面這個(gè)圖也可以看到，L1SYS模型中的每一部分（STB/EB/LFB/PB/SRAM等）都需要監(jiān)測(cè)L1SYS設(shè)計(jì)外部和內(nèi)部數(shù)據(jù)，從PP-CAMEL的回顧來(lái)看，MESH方案需要連接5個(gè)VIP monitor，而且從VIP monitor監(jiān)測(cè)到的數(shù)據(jù)需要根據(jù)需要組合為stream，再按照MESH表格對(duì)這些stream進(jìn)行獨(dú)立的處理和檢查。

PP-CAMEL對(duì)以前的這部分工作評(píng)價(jià)是，盡管可以做到cycle-accurate的細(xì)致檢查，但帶來(lái)的一個(gè)煩惱是由于MESH方案需要與設(shè)計(jì)行為深度耦合，而且對(duì)驗(yàn)證人員提出較高的維護(hù)要求，如果設(shè)計(jì)發(fā)生變化，那么MESH方案作為一個(gè)整體都將需要花費(fèi)較大人力去更新MESH驗(yàn)證環(huán)境。



上面來(lái)自PP-CAMEL的評(píng)價(jià)便于理解，這就像如果我們把設(shè)計(jì)的模型做成一個(gè)big synthesized model，那么設(shè)計(jì)的每一處更新都會(huì)使得讓我們?nèi)ゾS護(hù)這個(gè)大模型，而大模型越來(lái)越大、復(fù)雜、乃至趨于臃腫的情況下，設(shè)計(jì)可能打補(bǔ)丁式的修改，也可能會(huì)讓參考模型去做類似的補(bǔ)丁式修改。

理想情況下，如果維護(hù)這個(gè)模型的人是同一個(gè)人（大公司里這種情況較多）那么還好一些，但是如果一旦人員發(fā)生變動(dòng)，模型當(dāng)時(shí)設(shè)定的好壞、代碼結(jié)構(gòu)是否合理、模型是否方便維護(hù)這些問(wèn)題就隨之而來(lái)了。 從PP-CAMEL最后的代碼對(duì)比來(lái)看，也能證實(shí)這個(gè)問(wèn)題，CAMEL模型的代碼量大概只有MESH模型的1/3。

但這并不是簡(jiǎn)單說(shuō)明，CAMEL既輕量化，又能完成MESH模型可以做的cycle-accurate的細(xì)致檢查。熊掌與魚難以兼得，CAMEL模型是在將功能檢查做了分層、分類以后，才將MESH模型原來(lái)可以一股腦完成的事情解耦合成CAMEL模型和其它模型，并且CAMEL模型能做的事情，也是分為了多種任務(wù)的。

一句話，那就是CAMEL模型做了檢查任務(wù)的規(guī)劃，沒(méi)有一來(lái)就試圖去構(gòu)建一個(gè)大而全的模型，而是一開始就打算將驗(yàn)證分成了多個(gè)步驟，逐一將從基礎(chǔ)功能到高級(jí)功能再到邊界情況的檢查分為了多個(gè)任務(wù)去實(shí)現(xiàn)的。



那么，PP-CAMEL為什么不采用PP-MESH中的大模型呢？難道是不需要做準(zhǔn)確預(yù)測(cè)了嗎？其實(shí)從論文一開始的背景闡述來(lái)看，即他們開始在做多核多線程的架構(gòu)（RISC-V）。這意味他們盡管可以參考原來(lái)PP-MESH中的L1SYS設(shè)計(jì)，但同時(shí)要適配多核ACE協(xié)議和snoop memory 請(qǐng)求（對(duì)于L1SYS而言屬于新的外部請(qǐng)求/響應(yīng)）。

我能猜想到的是，當(dāng)時(shí)也應(yīng)該是考慮過(guò)MESH方案復(fù)用的，但這意味著需要理解原有的方案，而且要修改MESH中的代碼。如果是同一位工程師修改維護(hù)他原來(lái)的方案，那么思路大概還能跟得上拍子，但如果是不同的工程師打算要做這件事情，那么他還會(huì)考慮另外一種可能，就是在原有MESH思路的基礎(chǔ)上，做一些檢查的優(yōu)化。

值得注意的是，PP-CAMEL論文中提到了PP-MESH原本在數(shù)據(jù)激勵(lì)方面的layer層次規(guī)劃清晰、各個(gè)方法接口也很豐富，這些有關(guān)激勵(lì)部分思想和接口仍然可以復(fù)用下來(lái)。



所以可能更符合當(dāng)時(shí)實(shí)際情況的是，已經(jīng)經(jīng)歷過(guò)PP-MESH“高精度”模型帶來(lái)驗(yàn)證環(huán)境與設(shè)計(jì)高度綁定以后的晃動(dòng)帶來(lái)的痛苦之后，PP-CAMEL決定采取一個(gè)“循序漸進(jìn)”的方案，即它的初衷是構(gòu)建一個(gè)更為快速能夠?qū)π碌腖1SYS設(shè)計(jì)進(jìn)行檢查的驗(yàn)證環(huán)境（如果能夠復(fù)用以前的一些激勵(lì)、測(cè)試序列那就更好）。

所以它一開始并沒(méi)有求全，而是把檢查的重心放在數(shù)據(jù)完整性上面，即data correctness check。這一點(diǎn)跟我們常規(guī)的數(shù)據(jù)流檢查類似，比如DMA數(shù)據(jù)搬遷或者數(shù)據(jù)打包解包操作等功能檢查，都是先完成數(shù)據(jù)完整性檢查，再去就設(shè)計(jì)的行為、時(shí)序做更為細(xì)致的檢查。



它的模型中的數(shù)據(jù)存放是較為模糊的，因?yàn)樗粫?huì)準(zhǔn)確預(yù)測(cè)數(shù)據(jù)，而是會(huì)存放所有可能從目標(biāo)地址讀出去的數(shù)據(jù)（stores all possible values of the same address），這種方式仍然可以在設(shè)計(jì)早期階段幫助驗(yàn)證做數(shù)據(jù)（模糊）檢查。它的優(yōu)點(diǎn)在于更快部署、不依賴于具體的設(shè)計(jì)、時(shí)序，與設(shè)計(jì)可以解耦。

如果檢查方案里有配置按鈕（configuration knob），那么這種檢查方式可以給起個(gè)名字（rough level check）。 接下來(lái)PP-CAMEL也提到了，如果要進(jìn)一步做到準(zhǔn)確的數(shù)據(jù)預(yù)測(cè)檢查，那么就需要獲得額外的信息，比如對(duì)cache hit/miss check和rationality read/write command to external memory（對(duì)外部存儲(chǔ)讀寫請(qǐng)求的合理性檢查，關(guān)系到cache hit/miss的預(yù)測(cè)和模型準(zhǔn)確度）。

那么就需要添加諸如location/SCB data/SRAM data這樣的屬性。而這些屬性又當(dāng)來(lái)自于各個(gè)VIP monitor。當(dāng)從monitor獲得的信息越多，那么CAMEL模型也將越復(fù)雜，而用于做data correctness check, hit/miss check, rationality check of request to external memory等也將越準(zhǔn)確。



這個(gè)道理我們似乎都懂，但是PP-CAMEL恰恰給出了與原有PP-MESH不同的驗(yàn)證環(huán)境實(shí)現(xiàn)步驟，下面這段話我認(rèn)為是整篇論文中要著重表達(dá)的驗(yàn)證工程思想。我們能夠理解，一個(gè)simple testbench不可能做到precise check，但我們能不能理解如果要設(shè)計(jì)一個(gè)complex testbench，是否有能力讓它做到simple check，或者做到different precision of check？對(duì)于MESH模型，PP-CAMEL給出的回顧似乎在說(shuō)維護(hù)這樣一個(gè)大模型很耗神，尤其在PP-CAMEL背景中遇到一個(gè)新的L1SYS設(shè)計(jì)的時(shí)候，需要修改的內(nèi)容恐怕很多，尤其是面對(duì)8000+行的MESH模型。



將模型先從簡(jiǎn)單做起，有的時(shí)候也是一種妥協(xié)。這種妥協(xié)可能是來(lái)自于項(xiàng)目的壓力，可能是來(lái)自于對(duì)復(fù)雜設(shè)計(jì)邏輯和時(shí)序，也可能是為了將來(lái)以后便于維護(hù)。PP-CAMEL的模型核心是圍繞著地址和數(shù)據(jù)的，它本身不復(fù)雜，而在此基礎(chǔ)之上添加了一些必要的屬性，即能夠創(chuàng)造出條件做不同精確度的檢查。最終，檢查精度還會(huì)落回到模型復(fù)雜性上。

只不過(guò)，從trade-off來(lái)看，PP-CAMEL提出的思路，使得在驗(yàn)證L1SYS過(guò)程中，得以找到一條從簡(jiǎn)單到復(fù)雜的路，使得可以對(duì)L1SYS的各個(gè)功能逐一做從基礎(chǔ)到復(fù)雜的檢查。另外，在PP-CAMEL中可以看到，與PP-MESH的驗(yàn)證思路聯(lián)系緊密，盡管模型的實(shí)現(xiàn)方式發(fā)生了較大變化，但激勵(lì)層次的組織和復(fù)用、以及原有的各個(gè)API的復(fù)用仍然帶來(lái)了幫助。

這種有歷史銜接的論文前后研究起來(lái)也很有收獲，而這兩篇論文也可以啟發(fā)我們?cè)趯?shí)現(xiàn)參考模型時(shí)，究竟是按照大模型來(lái)實(shí)現(xiàn)，還是按照分層（由易到難）模型來(lái)實(shí)現(xiàn)，需要考慮諸多工程因素。






審核編輯：劉清