面向特征的SystemC模型产品线的开发和形式化功能验证技术研究

发布时间：2020-05-30 08:04

【摘要】：随着芯片系统的功能日益复杂,上市时间却越来越短,越来越多的芯片系统希望实现为片上系统(SoC)。SoC是指集成有包括微处理器、存储器等各种硬件模块,以及运行于它们之上的嵌入式软件,以完成特定目标的系统。SoC的特点在于大量的系统功能以运行于硬件平台之上的嵌入式软件实现,因此开发更加灵活,周期更短。传统的芯片系统设计流程从描述系统的寄存器传输级(RTL)模型开始,难以适应嵌入式软件早期开发的要求,因此不适合SoC开发。新提出的开发流程从描述系统的事务级模型(TLM)开始。事务级比RTL抽象层次高,因此TLM开发更加容易,仿真速度也更快,可作为嵌入式软件早期开发的平台,适合SoC开发。SystemC是目前事务级建模的标准语言,因此针对SystemC模型开发和验证技术的研究具有重要意义。本文首先提出将针对同一SoC项目开发的一组SystemC模型视为一种特殊的软件产品线(SPL),称为SystemC模型产品线(SCPL),然后研究了SCPL的开发方法、组合安全性和形式化功能验证问题。SPL指针对同一领域开发的一组软件的集合。由于针对同一领域,这组软件间存在很多公共特征,SPL相关研究旨在利用这些公共特征提高软件的开发和验证效率。SCPL是针对同一SoC项目开发的一组SystemC模型,模型间同样存在很多公共特征,如何利用它们提高SystemC模型的开发和验证效率,是本文的研究目标。考虑到SystemC模型本质是C++程序,因此SCPL研究可借鉴SPL研究成果。考虑到SystemC模型旨在模拟硬件的并发行为,而软件是顺序执行的,因此SCPL研究与SPL研究存在差异。SPL研究主要包括四项内容,即开发方法、语法正确性、组合安全性和行为正确性。本文针对SCPL在以上四项内容开展了相应研究,取得了如下研究成果: (1)论证了以TLM为入口的芯片设计新流程下,SoC设计过程往往伴随着一组SystemC模型的开发,首次提出将这组SystemC模型视为一种特殊的SPL,并称之为SystemC模型产品线(SCPL)。指出了SCPL与普通SPL的异同。 (2)指出了以传统的面向对象方法开发SCPL存在的问题,提出以面向特征的方法开发SCPL。指出现有的面向特征方法在开发SCPL时存在的问题,提出了解决方案,并提出一套相应的面向特征的SCPL开发方法。案例研究表明,与面向对象开发方法相比,面向特征的SCPL开发方法可有效减少重复代码,提高开发效率。同时,与基于条件编译的SCPL开发方法相比,面向特征的SCPL开发方法可有效减少处于条件编译指令包围中的代码。由于条件编译指令的大量使用是造成代码难以开发、理解和维护的关键,因此本文提出的面向特征的SCPL开发方法可以提高SCPL开发效率,增强代码的可理解性和可维护性。 (3)提出了一套简化的SystemC语言SC~S及其面向特征的扩展FSC~S,讨论了以FSC~S开发的SCPL的组合安全性问题,给出了一套可靠且完全的形式化判定方法。要判定SCPL的组合安全性,传统方法只能逐个编译SCPL中所有的SystemC模型,与这种方法相比,本文的判定方法可以显著缩短判定时间,提高判定效率。 (4)基于属性保持的概念提出一种SCPL形式化功能验证方法,案例研究表明,与枚举SCPL中所有SystemC模型并逐个验证的方法相比,该方法能有效减少待验证SystemC模型的数目,从而有效改善SCPL形式化功能验证所需的时间和空间消耗。 (5)提出了属性推断的概念,并基于此概念提出一种SCPL形式化功能验证方法。与属性保持相比,属性推断的要求更加宽松,因此相应的SCPL形式化功能验证方法适用范围更广。案例研究表明,与枚举SCPL中所有SystemC模型并逐个验证的方法相比,基于属性推断的方法能显著减少待验证SystemC程序的数目,从而显著改善验证所需的时间和空间消耗。本文以面向特征的SCPL开发方法完成了OpenRisc 1000项目和MJPEG解码芯片项目的开发。并针对前一项目使用本文提出的方法进行了组合安全性判定和形式化功能验证。前一项目的开发与OpenCores组织提供的开源实现相比,处于条件编译指令包围中的代码量显著减少,从而改善了代码的可理解性和可维护性。后一项目的实现与面向对象的SCPL实现相比,代码总量大幅减少,从而提高了开发效率。针对OpenRisc 1000项目的组合安全性判定结果显示,本文提出的方法比基于枚举的判定方法验证效率大幅提高。针对OpenRisc 1000项目的形式化功能验证结果表明,与基于枚举的判定方法相比,本文提出的基于属性保持的方法能够有效减少判定所需的时间和空间消耗,本文提出的基于属性推断的方法能显著减少判定所需的时间和空间消耗。
【学位授予单位】：国防科学技术大学
【学位级别】：博士
【学位授予年份】：2011
【分类号】：TP368.1;TN47

【引证文献】