论文部分内容阅读
随着芯片系统设计复杂性的日益增加,上市时间的不断缩短,业界和学术界通过采用高层设计抽象,以及高效、无缝的设计重用,来解决工业界所面临的问题。当前,模型驱动的SoC设计方法已经引入到SoC的设计流程之中。新的设计方法带来了新的验证挑战,现有的SoC功能验证方法和技术(形式化验证方法和模拟验证方法)已经难以适应模型驱动的SoC设计方法提出的新的验证要求,急需从理论和方法上进行突破和创新,提出新的SoC验证方法和技术。模型驱动的验证方法综合了形式化验证方法和模拟验证方法的优点,以统一的描述模型为基础,以功能覆盖率为测度,通过应用基于模型的抽象技术、基于模型的测试程序自动生成技术、形式化验证等技术,实现对SoC不同抽象层次的功能验证,特别是对SoC行为级、事务级和RTL级设计的功能验证。因此,该方法一经提出就得到了广泛应用。本文针对模型驱动的SoC功能验证存在的不足和主要问题,重点研究模型驱动的SoC系统功能验证中的关键技术。由于形式化方法存在状态爆炸问题,对于集成IP核之后的SoC全系统功能验证的处理能力有限,本文从模拟验证方法入手展开研究。由于SoC的全系统验证需要考察环境因素,现有的功能规约方法对于环境因素考虑不足。因此,本文首先研究基于模型的SoC功能规约方法和系统级行为提取方法,并对影响系统功能正确性的关键行为和IP核进行风险评估,为系统级功能验证策略制定提供量化依据。模拟方法涉及两个关键问题:如何生成测试程序以及如何执行测试调度。本文研究基于模型的测试程序生成方法和相关的调度技术。在功能规约和测试生成的基础上,研究如何利用模拟方法加速和改进SoC系统形式验证方法,特别是模型级和事务级行为的一致性验证方法。最后,本文研究如何在SoC规约模型的基础上创建可执行模型,在可执行模型的基础上进行模拟验证,使得能够在SoC的设计初期进行和加速功能验证。本文在模型驱动的SoC验证方法框架中,对上述关键技术开展了研究,取得以下研究成果:(1)鉴于当前的SoC统一描述模型难以精确描述设计的约束信息,扩充了现有SoC的规约模型,将对象约束语言及其实时扩展形式集成到SoC统一描述模型之中,支持对SoC设计的约束建模,提高了利用统一描述模型创建SoC设计规约的精确性,为后续功能验证奠定了规约基础。(2)提出了一种环境驱动的、基于模型的SoC系统级行为抽取与设计风险评估方法。制定有效的SoC系统级功能验证策略需要对SoC设计进行行为抽取、设计度量和风险评估,抽取并标识潜在高风险的系统级行为和IP构件,对可能导致设计缺陷的IP构件和行为实施优先验证,是加速验证的关键。本文提出的行为抽取与风险评估方法,以环境呈现的功能为导向,对SoC设计对环境角色呈现功能的用例模型、场景模型引入约束机制和概率标记信息,创建SoC系统级行为场景。对行为场景涉及到的构件和通道执行轨迹分析,提取与场景相关的构件集和通道集,对其进行风险评估,获取场景的风险因子,并对整个SoC设计执行风险评估。该方法不但可以提取SoC的系统级行为,标识关键行为场景和构件,同时还能够有效评估特定构件在SoC系统级行为中所处于的地位,为验证系统级行为的策略制定提供重要的量化依据。(3)提出了一种环境驱动的、基于模型的SoC事务测试程序生成方法。该方法以SoC同环境的交互为驱动,对场景中环境对SoC的输入构造定向事务测试程序。所生成的事务测试程序能够高效应用于SoC的系统级行为验证,很大程度上减少了系统级行为验证所需输入激励的数量,节省了模拟资源。在SoC基于事务的验证方法中,事务调度技术对于SoC设计验证起着加速作用。本文基于Petri网的良好调度能力,提出了基于扩展Petri网模型的SoC事务调度方法和TAM资源约束下的事务调度方法,支持SoC的测试程序生成。该方法可以预先评估调度行为,支持多种调度模式,重用生成的事务,为SoC复杂行为的模拟验证提供输入激励。(4)提出了基于层次接口自动机和基于程序切片与面向方面代码注入的行为一致性验证方法。在模型驱动的SoC设计方法学中,不同抽象层次上行为一致性验证,是确保底层设计满足上层设计约束的关键。在基于层次接口自动机的方法中,通过定义层次接口自动机的操作语义,将SoC设计描述为一个层次接口自动机网。然后,通过构造和搜索状态空间,验证行为的一致性问题;在基于程序切片和面向方面代码注入的方法中,首先利用静态程序切片技术对SoC事务级设计进行设计化简。然后,在化简后的SoC设计上通过采用面向方面的代码注入,通过输入激励,执行模拟,捕获事件轨迹,实现对行为的一致性验证。(5)改进了基于扩展Petri网模型模拟验证SoC设计的方法。SoC功能的早期验证,在设计初期确保功能的正确性,对于SoC后续设计起着非常重要的影响。本文鉴于Petri网良好的形式化和模拟验证能力,扩展了Petri网模型,支持创建SoC高层可执行模型,为利用Petri网执行SoC早期设计验证提供支撑。本文设计实现了一个构件式SoC功能验证原型工具SoC-CBVE。该工具集成了本文所提出的基于模型的事务测试生成方法、事务调度方法、模型级与事务级行为场景的一致性验证方法。同时,本文基于所提出的利用Petri网创建SoC高层可执行模型的方法,设计实现了基于扩展Petri网模型的建模与模拟原型工具PTSE。利用上述原型工具对实际SoC设计进行了验证,发现了设计中的错误。