基于GSTE中抽象问题的研究及其应用

摘要

随着社会的不断进步,集成电路在社会中的影响愈来愈大,占得比重愈来愈高。从个人日常所用的手机,平板电脑到支撑整个国家的卫星,航天飞机,集成电路已经和我们的生活息息相关。随着科技的日益发展,集成电路的复杂度也呈指数性增大。如何保证集成电路能够正确可靠的工作,便成为目前研究的重点。从传统的测试/模拟的方法,到最近兴起的形式化验证方法,所有的这些方法都是为了保证集成电路能够正确可靠的运行。在研究形式化方法中的推广化符号轨迹赋值方法的过程中,除了在降低集成电路的复杂度和提高计算效率方面有了大量的工作外,还发现集成电路布尔建模的过程同生物基因调控网络建模过程的相似之处,并将两者进行结合,创新的将形式化方法应用到生物基因调控网络的建模和计算过程中。　　本文主要工作成果与创新点如下:　　1.在降低集成电路复杂度和提高计算效率方面,创新的提出了推广化符号轨迹赋值中的抽象算法:最小化保留后续词的抽象函数算法,同时修正由于过度抽象而引发的伪错误现象,并提出优化后的最小化保留后续词的抽象函数算法,最后将提出的上述两种算法成功的应用到自主开发的验证工具:Whale验证平台。最终的实验结果表明上述算法的高效性和正确性。　　2.在推广化符号轨迹赋值方法的应用方面,创新的将算法应用到NAND Flash的软件仿真器模型的检验中,通过形式化方法的验证与具体的实验结果相结合的方式,保障NAND Flash的软件仿真器设计的正确性。　　3.在生物基因调控网络的模型建立方面,发现生物基因调控网络同布尔网络之间的关联,从而联想到集成电路中布尔建模过程同生物基因调控网络中的布尔建模过程有着诸多相似之处,并创新的将两者进行结合,成功的将集成电路中的一些建模方法应用到生物基因调控网络的模型建立过程中。　　4.在生物基因调控网络中同步吸引子的计算方面,创新的将同步吸引子分为三类,无分支吸引子,存在分支吸引子和全分支吸引子,并提出计算同步布尔网络中同步吸引子的算法,但是由于算法存在多余的重复计算,于是提出优化后计算同步布尔网络中同步吸引子的算法,并通过具体的实验案例比较优化前后计算同步布尔网络中同步吸引子的算法的差异。最后将上述两种算法与现有的计算同步布尔网络中同步吸引子的工具-BoolNet基于三组生物实验进行比较以辅证算法的高效性。　　5.在经过深入的研究之后,异步布尔网络会比同步布尔网络更贴合于实际生物基因调控网络中生物信号的传导。在生物基因调控网络中异步吸引子的计算方面,创新的将同步吸引子与异步吸引子合并,并分为四类,自循环吸引子,简单环吸引子,同步复杂环吸引子和异步复杂环吸引子,同时,根据同步吸引子和异步吸引子的内部特性,分析同步吸引子和异步吸引子之间的联系,并提出计算异步布尔网络中吸引子的算法,并对吸引子进行归类。在最后的实验部分,将上述算法实现为GeneFatt工具包,同现有的计算同步和异步布尔网络中吸引子的工具-GenYsis,在使用共同的测试用例的情况下进行实验测试。实验结果表明了GeneFatt工具包的优越性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪 论

1.1 引言

1.2验证方法与验证过程

1.3验证方法在基因调控网络中的应用

1.4 论文的研究重点、创新点以及章节安排

第二章 GSTE中基于断言图的抽象算法及其应用

2.1 STE/GSTE、断言图、二叉判定图

2.2 模型、断言图、满足性和抽象的定义

2.3 MPA和OMPA算法

2.4 实验结果与分析

2.5 GSTE在NAND Flash中的应用

2.6 本章小结

第三章 同步布尔网络中吸引子的计算

3.1基因调控网络和同步布尔网络

3.2 同步吸引子的定义和求解

3.3 三种类型的同步吸引子的定义和求解

3.4 实验结果与分析

3.5 本章小结

第四章 异步布尔网络中吸引子的计算

4.1异步布尔网络

4.2同步吸引子与异步吸引子的分类与关系

4.3 计算吸引子的相关算法

4.4 裂殖酵母分裂周期模型

4.5 经典生物基因调控网络实验分析

4.6本章小结

第五章 结论与展望

5.1 论文的主要工作和创新点

5.2进一步的研究工作和设想

致谢

参考文献

攻读博士学位期间取得的成果