時(shí)序電路的等價(jià)驗(yàn)證方法及其在FPGA中的應(yīng)用.pdf

1、隨著集成電路設(shè)計(jì)水平的進(jìn)步，電路規(guī)模日益增大，電路設(shè)計(jì)的時(shí)間越米越多的耗費(fèi)在電路的驗(yàn)證問(wèn)題上。傳統(tǒng)的基于模擬的驗(yàn)證逐漸不能滿足驗(yàn)證的需要，形式驗(yàn)證方法作為傳統(tǒng)模擬驗(yàn)證方法的補(bǔ)充成為研究的熱點(diǎn)。等價(jià)驗(yàn)證可以分為組合電路的等價(jià)驗(yàn)證和時(shí)序電路的等價(jià)驗(yàn)證。組合電路的等價(jià)驗(yàn)證算法目前發(fā)展比較成熟，成為很多時(shí)序電路驗(yàn)證算法的基礎(chǔ)。本文的研究工作主要集中在時(shí)序電路的等價(jià)驗(yàn)證部分，由兩部分組成： 第一部分是時(shí)序電路等價(jià)驗(yàn)證的研究。時(shí)序電路的等價(jià)

2、驗(yàn)證通常使用的方法都是對(duì)有限狀態(tài)機(jī)進(jìn)行遍歷，利用電路中的組合部分，或是展開成時(shí)間幀的形式加以驗(yàn)證，或是利用結(jié)構(gòu)中的相似性用固定點(diǎn)迭代的方式進(jìn)行驗(yàn)證，或是化作布爾表達(dá)式用可滿足性問(wèn)題的算法進(jìn)行驗(yàn)證。本文的算法將時(shí)序電路的時(shí)序行為用狀態(tài)轉(zhuǎn)換圖的形式來(lái)表示，對(duì)待驗(yàn)證電路的狀態(tài)轉(zhuǎn)化圖進(jìn)行同構(gòu)驗(yàn)證，從而驗(yàn)證兩電路是否等價(jià)。主要的創(chuàng)新處在于：1.不依賴于電路結(jié)構(gòu)的相似性，可以驗(yàn)證結(jié)構(gòu)不同，寄存器數(shù)目不同的電路；2.采用圖的方式表示時(shí)序電路的行為，而

3、不依賴于狀態(tài)編碼或者是布爾表達(dá)式：3.速度優(yōu)于傳統(tǒng)的基于BDD的狀態(tài)遍歷法以及結(jié)構(gòu)不動(dòng)點(diǎn)法。 第二部分是FPGA中電路等價(jià)驗(yàn)證的研究。針對(duì)FPGA流程的工藝映射流程、和裝箱流程展開驗(yàn)證。對(duì)于經(jīng)過(guò)工藝映射的由LUT(look up table)組成的電路和原始的gate_level的電路進(jìn)行等價(jià)驗(yàn)證，以及對(duì)于經(jīng)過(guò)裝箱的由cluster組成的電路和LUT組成的電路進(jìn)行等價(jià)驗(yàn)證。采用寄存器匹配的方法將時(shí)序電路轉(zhuǎn)化為組合電路后，用C-S