基于SOC异步FIFO的设计与形式验证

发布时间：2017-11-12 17:34

  本文关键词：基于SOC异步FIFO的设计与形式验证

  更多相关文章： SOC 异步FIFO 形式验证 JASPER

【摘要】：近年,随着集成电路产业的快速发展,半导体工艺水平已经达到亚微米水平,随之而来的现状就是芯片集成规模越来越复杂。纵观整个芯片设计流程,从行为级HDL一直到芯片最后的投片,最复杂、最重要的环节就是验证。在面对更大的验证压力时,传统的模拟仿真验证已经渐渐暴露出其局限性。形式验证方法作为传统验证方法的补充,日益引起人们的关注。形式验证方法以不同的验证逻辑实现验证目标,能够克服传统验证方法的不足,所以本文的研究重心为形式验证,并结合JASPER平台提出了适用性更广的形式验证方法。首先,本文选取SOC中常用模块异步FIFO为验证对象,基于传统异步FIFO设计结构和功能实现逻辑,本文提出了改进后的异步FIFO设计,与传统设计相比,改进后的设计优势在于运用了新的空满标志位判断逻辑,克服了传统设计中存储器深度的局限性;然后,本文分析了形式验证当前的应用局限性,研究了基于Jasper平台形式验证方法的逻辑原理以及形式验证状态空间的意义,并对Jasper平台特征验证流程进行了详细的说明,同时,引入了Jasper的特征验证语言SVA,通过举例分析研究了SVA语言关于设计特性的描述细则;最后,以本文中改进后的异步FIFO为验证对象,制定出特定的Jasper验证方案,并基于异步FIFO设计的功能划分进行断言语句的编写,在验证结果分析中,通过特征语句编写错误为例详细讨论了如何使用Jasper图形界面进行验证分析纠错。本文形式验证方法的研究结果表明,基于JASPER平台的形式验证方法较传统模拟仿真方法,具有无需编写Testbench与Testcase、验证周期短、验证覆盖率高等特点。目前,本文所研究的形式验特征验证方法已经广泛用于INTEL SOC验证项目中,多为与模拟仿真方法相结合,大大提高了原始单一方法验证的效率。形式验证方法的研究对未来数字IC验证的发展具有极其深远的实际意义,同时,对日益复杂的数字IC设计也提供了充分的验证保障。
【学位授予单位】：西安电子科技大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP333

【共引文献】

中国期刊全文数据库 前10条

1 郑庆伟;周武;余跃;;航天IP核的自主设计、评测关键技术研究[J];航天标准化;2012年02期

2 杨军;葛海通;郑飞君;严晓浪;;一种形式化验证方法:模型检验[J];浙江大学学报(理学版);2006年04期

3 王海峰,吕永波,张仲义;一种系统安全性的形式化验证方法[J];计算机工程与应用;2003年04期

4 李光辉,邵明,李晓维;通用CPU设计验证中的等价性检验方法[J];计算机辅助设计与图形学学报;2005年02期

5 鲁巍;吕涛;杨修涛;李晓维;;RTL可观测性语句覆盖评估方法[J];计算机辅助设计与图形学学报;2006年01期

6 李光辉,邵明,李晓维;验证包含黑盒的电路设计的有效方法[J];计算机学报;2004年06期

7 张仲义,王海峰;智能交通安全控制系统的模型验证[J];交通运输工程与信息学报;2003年01期

8 胡东华;张旭;;模拟退火算法在BDD变量最优排序中的应用[J];科技信息(科学教研);2007年34期

9 岳园;何安平;;使用逻辑锥分割的组合电路等价性验证[J];计算机工程与应用;2013年02期

10 谷伟卿;施智平;关永;张杰;赵春娜;叶世伟;;Gauge积分在HOL4中的形式化[J];计算机科学;2013年02期

中国硕士学位论文全文数据库 前10条

1 李鸿翔;基于VMM的硬件验证技术研究及应用[D];哈尔滨工程大学;2010年

2 闫硕;基于多项式符号代数的电路形式验证[D];北京交通大学;2011年

3 刘林;数字集成电路功能验证中的变异测试方法研究[D];山东大学;2011年

4 马丽丽;基于静态分析的RTL设计错误检测方法研究[D];湘潭大学;2011年

5 王瑞蛟;安全SoC体系结构的设计与实现研究[D];解放军信息工程大学;2011年

6 吴俊华;组合电路的形式验证方法研究[D];哈尔滨工程大学;2004年

7 李树杰;中科SoC通用验证平台及验证方法学研究[D];山东科技大学;2005年

8 胡靖;可再配置结构中针对IP重用技术的综合方法研究[D];哈尔滨工程大学;2005年

9 郑伟伟;基于线性规划的RTL性质验证研究[D];清华大学;2005年

10 王迪;微处理器的分级模型检验验证研究[D];清华大学;2005年

，

本文编号：1176944