在芯片的设计流程中,一般采用多种验证手段来确保芯片的正确性,包括功能验证,时序验证,测试验证等.其中最耗时的当推是功能验证,它主要是芯片流片之前,通过对芯片的软件模型进行验证,从而确保设计的芯片在逻辑功能上与功能规范做到一致.目前功能验证技术主要包括基于模拟的方法和形式化方法两类. 基于模拟的验证在当前业界最为常用,它将待验证的设计置于一个虚拟的软件测试平台中,对输入施加激励,然后把待验证设计的输出同参考输出进行比较,验证的力度是通过各种覆盖准则来度量.很显然它不是一种完全的方法.形式化的验证则不同,它不需要施加任何激励,直接使用严格的数学推理来证明设计满足规范的部分或全部属性,因此是一种完全的方法,它大体有等价性检验,模型检验,定理证明等几种.但这些方法在使用时会有状态空间的爆炸问题或者时间上的爆炸问题,所以目前只能应用于中小规模的设计. 在无界模型检验中,前像计算是算法中的一个重要操作.但是以ATPG或SAT引擎进行无界模型检验的前像计算时容易产生大量不必要的前像解,致使后面的不动点的迭代过程不易进行.本文的主要工作包括:1.系统的介绍了当前功能验证技术在工业界与学术界的发展现状.包括模拟验证,模型检验技术等内容.2.提出了一种结合ATPG与SAT引擎的无界模型检验前像计算方法,减少前像解的总个数,加快不动点的迭代过程.并通过实验证明了方法的有效性.3.将当前工业主流验证方法成功应用在一款低功耗处理器的功能验证上.包括基于约束的激励产生技术、断言检查技术、自动化响应比较技术、覆盖率评估技术等.