论文摘要
集成电路的验证,已经成为其研发的最大障碍。传统的模拟验证技术无法满足当前SOC(System-On-Chip)设计带来的空前巨大的验证需求。基于此,形式化的验证方法作为模拟方法的一种重要补充,越来越得到人们的关注。模型判别技术(Model Checking)是形式验证技术的一种,用户参与少、自动化程度高,可以应用于电路设计的不同层次的优点使其成为该领域的研究热点。但是电路规模的增大,有限自动机的状态数以指数的形式增加,在实际中受到了有限内存的约束,这个问题就是模型判别中的瓶颈问题——状态空间爆炸。有限模型判别技术(BoundModel Checking,BMC)应运而生。传统的BMC技术基于BDD或SAT,而当前的设计主流是寄存器传输级(Register Transfer Level,RTL),其字位混合的约束使得传统的BMC技术极其低效。本文提出一种新颖的方法解决这个问题。首先将电路按照时序展开;接着使用线性规划(Linear Programming,LP)约束对RTL电路进行约束建模,生成隐式自动机;并将待验证的性质进行线性化描述,生成线性规划约束;最后是用LP求解器,得出验证结果。实验表明这种方法,较传统的BMC技术,在CPU时间和内存消耗上具有较大的优势。在进行上述技术研究时,我们发现如果能够将RTL设计的模块化层次式结构信息引入到验证系统中来,将对验证过程起到较大的指导意义。我们进一步开发了H-LPSAT系统。它可以验证层次式的RTL设计。实验表明H-LPSAT系统的验证效率,较上述方法有了更进一步的提高,尤其在CPU时间上。
论文目录
相关论文文献
- [1].优先级资源共享在RTL综合中的实现[J]. 华南理工大学学报(自然科学版) 2013(06)
- [2].一种自动生成状态机RTL代码的方法[J]. 微电子学与计算机 2008(07)
- [3].采用二元CSP引擎求解RTL数据通路的可满足性[J]. 计算机辅助设计与图形学学报 2009(04)
- [4].扩展型资源共享方案在RTL综合中的实现[J]. 深圳大学学报(理工版) 2013(05)
- [5].功耗限制下RTL数据通路扫描测试调度方法[J]. 微计算机信息 2012(02)
- [6].基于FPGA的RTL级USB2.0协议层设计与实现[J]. 中国集成电路 2008(07)
- [7].阿克陶6.7级地震前RTL异常演化特征分析[J]. 国际地震动态 2017(08)
- [8].设计质量及其对设计收敛的影响[J]. 电子设计技术 2010(10)
- [9].基于Cycle True准则的算法仿真和RTL代码生成方法研究[J]. 科技视界 2012(06)
- [10].欧洲广播电视的媒介融合实践研究——以英国BBC和欧洲RTL为例[J]. 中国电视 2018(05)
- [11].芦山M_S 7.0地震前地震活动性分析及区域地震活动水平参数I_(RTL)的应用[J]. 地学前缘 2017(02)
- [12].面向RTL的VHDL语言模拟系统设计与实现[J]. 微电子学与计算机 2010(02)
- [13].RTL综合中FPGA片上RAM工艺映射[J]. 电子学报 2016(11)
- [14].基于RTL内部功能模块的测试向量产生方法[J]. 计算机工程 2011(03)
- [15].基于RTL的函数调用图生成工具CG-RTL[J]. 小型微型计算机系统 2014(03)
- [16].基于HP-GL/2及RTL的测井数据跨平台光栅打印技术的实现[J]. 石油工业计算机应用 2013(02)
- [17].门控时钟技术在RTL功耗优化上的应用[J]. 中国集成电路 2013(11)
- [18].基于加权数据通路的RTL级低功耗SoC设计[J]. 计算机科学 2011(02)
- [19].Synopsys推出用于早期RTL探测的DC Explorer[J]. 电子测量技术 2011(04)
- [20].完全的IC仿真需要一个完整的软硬件工具箱[J]. 电子设计技术 2011(06)
- [21].一种RTL级数据通路ODC低功耗优化算法[J]. 电子学报 2010(07)
- [22].RTL代码和R2G流程之间的内在联系[J]. 微处理机 2015(02)
- [23].RTL数字系统的形式化描述[J]. 安徽科技学院学报 2014(06)
- [24].应用RTL算法对岫岩M_s5.4地震的回顾性预测[J]. 东北地震研究 2008(01)
- [25].用于RTL设计验证的静态错误检测方法[J]. 计算机工程 2011(12)
- [26].一种基于FPGA的RTL级电路功耗评估方法[J]. 科学技术与工程 2009(08)
- [27].OPB总线仲裁器的RTL设计与FPGA实现[J]. 微计算机信息 2009(29)
- [28].利用SMT约束分解方法求解RTL可满足性问题[J]. 计算机辅助设计与图形学学报 2010(02)
- [29].SoC:IP是新的抽象[J]. 电子设计技术 2011(11)
- [30].一种基于混合SAT求解器的RTL验证方法[J]. 浙江大学学报(工学版) 2010(02)