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

摘要

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

目录

封面

声明

中文摘要

英文摘要

插图索引

表格索引

缩略语对照表

目录

第一章 绪论

1.1 研究背景

1.2 SOC验证分类

1.3 形式验证现状

1.4 论文章节安排

第二章 传统异步FIFO存储器

2.1 异步FIFO的基本结构

2.2 异步FIFO设计实现的难点

2.3 本章小结

第三章 改进的异步FIFO设计

3.1 设计规划

3.2 设计实现

3.3 低功耗分析

3.4 本章小结

第四章 基于JASPER平台特征验证

4.1 JASPERGOLD概述

4.2 JASPERGOLD特征检查

4.3 特征语言SVA

4.4 本章小结

第五章 改进异步FIFO的形式验证

5.1 验证方案

5.2 Property编写

5.3 验证结果分析

5.4 本章小结

第六章 总结与展望

6.1 本文总结

6.2 展望

参考文献

致谢

作者简介