基于GSTE中抽象問題的研究及其應(yīng)用.pdf

1、隨著社會的不斷進(jìn)步,集成電路在社會中的影響愈來愈大,占得比重愈來愈高。從個(gè)人日常所用的手機(jī),平板電腦到支撐整個(gè)國家的衛(wèi)星,航天飛機(jī),集成電路已經(jīng)和我們的生活息息相關(guān)。隨著科技的日益發(fā)展,集成電路的復(fù)雜度也呈指數(shù)性增大。如何保證集成電路能夠正確可靠的工作,便成為目前研究的重點(diǎn)。從傳統(tǒng)的測試/模擬的方法,到最近興起的形式化驗(yàn)證方法,所有的這些方法都是為了保證集成電路能夠正確可靠的運(yùn)行。在研究形式化方法中的推廣化符號軌跡賦值方法的過程中,除了

2、在降低集成電路的復(fù)雜度和提高計(jì)算效率方面有了大量的工作外,還發(fā)現(xiàn)集成電路布爾建模的過程同生物基因調(diào)控網(wǎng)絡(luò)建模過程的相似之處,并將兩者進(jìn)行結(jié)合,創(chuàng)新的將形式化方法應(yīng)用到生物基因調(diào)控網(wǎng)絡(luò)的建模和計(jì)算過程中。
　　本文主要工作成果與創(chuàng)新點(diǎn)如下:
　　1.在降低集成電路復(fù)雜度和提高計(jì)算效率方面,創(chuàng)新的提出了推廣化符號軌跡賦值中的抽象算法:最小化保留后續(xù)詞的抽象函數(shù)算法,同時(shí)修正由于過度抽象而引發(fā)的偽錯誤現(xiàn)象,并提出優(yōu)化后的最小化保留

3、后續(xù)詞的抽象函數(shù)算法,最后將提出的上述兩種算法成功的應(yīng)用到自主開發(fā)的驗(yàn)證工具:Whale驗(yàn)證平臺。最終的實(shí)驗(yàn)結(jié)果表明上述算法的高效性和正確性。
　　2.在推廣化符號軌跡賦值方法的應(yīng)用方面,創(chuàng)新的將算法應(yīng)用到NAND Flash的軟件仿真器模型的檢驗(yàn)中,通過形式化方法的驗(yàn)證與具體的實(shí)驗(yàn)結(jié)果相結(jié)合的方式,保障NAND Flash的軟件仿真器設(shè)計(jì)的正確性。
　　3.在生物基因調(diào)控網(wǎng)絡(luò)的模型建立方面,發(fā)現(xiàn)生物基因調(diào)控網(wǎng)絡(luò)同布爾網(wǎng)絡(luò)之

4、間的關(guān)聯(lián),從而聯(lián)想到集成電路中布爾建模過程同生物基因調(diào)控網(wǎng)絡(luò)中的布爾建模過程有著諸多相似之處,并創(chuàng)新的將兩者進(jìn)行結(jié)合,成功的將集成電路中的一些建模方法應(yīng)用到生物基因調(diào)控網(wǎng)絡(luò)的模型建立過程中。
　　4.在生物基因調(diào)控網(wǎng)絡(luò)中同步吸引子的計(jì)算方面,創(chuàng)新的將同步吸引子分為三類,無分支吸引子,存在分支吸引子和全分支吸引子,并提出計(jì)算同步布爾網(wǎng)絡(luò)中同步吸引子的算法,但是由于算法存在多余的重復(fù)計(jì)算,于是提出優(yōu)化后計(jì)算同步布爾網(wǎng)絡(luò)中同步吸引子的算

5、法,并通過具體的實(shí)驗(yàn)案例比較優(yōu)化前后計(jì)算同步布爾網(wǎng)絡(luò)中同步吸引子的算法的差異。最后將上述兩種算法與現(xiàn)有的計(jì)算同步布爾網(wǎng)絡(luò)中同步吸引子的工具-BoolNet基于三組生物實(shí)驗(yàn)進(jìn)行比較以輔證算法的高效性。
　　5.在經(jīng)過深入的研究之后,異步布爾網(wǎng)絡(luò)會比同步布爾網(wǎng)絡(luò)更貼合于實(shí)際生物基因調(diào)控網(wǎng)絡(luò)中生物信號的傳導(dǎo)。在生物基因調(diào)控網(wǎng)絡(luò)中異步吸引子的計(jì)算方面,創(chuàng)新的將同步吸引子與異步吸引子合并,并分為四類,自循環(huán)吸引子,簡單環(huán)吸引子,同步復(fù)雜環(huán)吸