基于线性规划的RTL性质验证研究

基于线性规划的RTL性质验证研究

论文摘要

集成电路的验证,已经成为其研发的最大障碍。传统的模拟验证技术无法满足当前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时间上。

论文目录

  • 摘要
  • Abstract
  • 第1章 引言
  • 1.1 集成电路验证概述
  • 1.2 模拟验证
  • 1.3 形式验证
  • 1.3.1 等价性验证
  • 1.3.2 性质验证
  • 1.4 本文的主要贡献
  • 1.5 论文组织
  • 第2章 理论基础
  • 2.1 模型判别
  • 2.2 时态逻辑
  • 2.3 模型判别基本算法
  • 2.4 可满足性问题
  • 2.5 基于 SAT 的有限模型判别
  • 2.5.1 电路展开
  • 2.5.2 CNF 范式生成
  • 2.6 本章小结
  • 第3章 基于线性规划的RTL 性质验证
  • 3.1 RTL 电路对验证工作带来的挑战
  • 3.2 RTL 可满足问题定义
  • 3.2.1 RTL 电路模型
  • 3.2.2 RTL 可满足性问题
  • 3.3 基于 LP 的RTL 可满足问题求解与性质验证
  • 3.3.1 RTL 性质验证算法框架
  • 3.3.2 基于 LP 的电路建模
  • 3.3.3 电路展开
  • 3.3.4 性质描述
  • 3.3.5 性质验证
  • 3.4 实验与分析
  • 3.5 本章小结
  • 第4章 层次式 RTL 性质验证
  • 4.1 层次式验证带来的优势
  • 4.2 层次式电路模型
  • 4.3 层次式RTL 性质验证
  • 4.4 实验结果及分析
  • 4.5 本章小结
  • 第5章 结论
  • 5.1 研究总结
  • 5.2 需要进一步开展的工作
  • 参考文献
  • 致谢
  • 声明
  • 个人简历、在学期间发表的学术论文与研究成果
  • 相关论文文献

    • [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)

    标签:;  ;  ;  ;  ;  

    基于线性规划的RTL性质验证研究
    下载Doc文档

    猜你喜欢