基于PSA的集成电路形式验证方法研究.docx

基于PSA的集成电路形式验证方法研究
摘要
现代集成电路中，PSA（PropertySpecificationLanguageandAutomatedverificationtools）成为验证器件性能与正确性的重要手段之一。本文针对PSA的验证方法进行深入分析和研究，并提出一种基于PSA的集成电路形式验证方法。该方法能够通过建立一定的规范模型来实现集成电路的正确性验证，并可以更好地提高验证效果和准确性。通过分析实验结果，验证方法的准确率和效率达到了很好的水平，为实现自动化验证提供了重要参考。
关键词：PSA、集成电路、形式验证、规范模型、自动化验证
正文
1.引言
随着集成电路在各个领域的广泛应用，其性能和正确性的验证已经成为工业化生产中一项重要的工作。传统的验证方法通常使用人工进行，这样长期以来，不仅耗时耗力，而且效率不高。随着信息技术的飞速发展，像PSA（PropertySpecificationLanguageandAutomatedverificationtools）这样的自动化验证工具已经引起了业界的广泛关注。
PSA是一种基于规范模型的验证工具，它可以直接利用设计文档中的规范来验证器件性能和正确性。因为它的直观性和易用性，PSA得到了许多业界从业人员的认可和推荐。本文通过对PSA工具的分析和验证方法的研究，提出了一种基于PSA的集成电路形式验证方法来实现集成电路的正确性验证。
2.PSA工具分析
PSA作为一种自动化验证工具，主要通过建立规范模型来验证机器或程序的正确性。PSA工具包括两部分：PSL（PropertySpecificationLanguage）和PV（PropertyVerification）。其中，PSL是一种用于描述规范的语言，由PSA开发库中的文件格式、语法和标准函数组成。PV实际上是PSA的核心，它是一个用于执行形式化验证的命令行工具。
当然，不同的设计文档和实现细节可能需要不同的规范模型来验证，因此PSA也支持多种模型和直接调用Vera、SystemC、OCP/IP等常用验证工具来编写模型。对于复杂的规范模型，PSA还提供了高层次的分层验证方法，不仅提高验证速度，而且还有利于发现系统中的异常行为。
3.规范模型的建立
建立规范模型是进行PSA验证的关键步骤。在规范模型中，各类规范都被文本化描述，并映射到具体的模型元素。这些模型元素可以是硬件组成单元，或者是生产程序的基本单元。细致的模型设计能够充分尽可能地描述这些基本单元的运作和相互作用，并保证最终的验证结果能够符合要求。
总体上，建立规范模型需要以下步骤：
①定义规范
设计文档中的规范可以通过语句描述出来，而这些语句中应该恰如其分地体现出规范的实质。比如，一个简单的规范“空闲时按照优先级排队，不论是否是新进程”可以转化为如下的语句：
Priority>Preemption
此时，规范已经被形式化地描述出来。
②建立模型
基于规范，可以开始建立模型。PSA支持多种建模方式，包括有限状态机、层次状态机、Petri网等。选择合适的建模方式可以保证建立出的模型不仅能鲁棒性更好，而且更不易出错。
③验证规范
模型建立完成后，就可以使用PSA的验证工具来验证规范是否符合要求。验证过程中，需要确认模型的功能覆盖率、灵敏度和具体描述能力等，在满足这些需求的前提下才能达到最终的验证效果。
4.基于PSA的集成电路形式验证方法
基于PSA的集成电路形式验证方法是一种自动化验证方案，它可以通过对规范的编写，以及对模型和验证结果的分析，更好地判断集成电路的正确性和稳定性。基本流程如下：
①定义规范
制定验证标准是验证正确性的前提。比如，对于电路功能板块，可以制定以下的验证标准：
--如果输入信号为0，则输出信号保持为0；
--如果输入信号为1，则输出信号必须为1。
②建立模型
为了验证集成电路器件的正确性，需要建立规范模型。PSA工具支持多种模型建立方式。例如，使用有限状态自动机（FSM）描述集成电路状态变化；或者使用层次状态机（HSM）等。建立模型后，可以对模型进行仿真验证。
③执行验证
基于定义的规范和建立的模型，进行相关的自动化验证。验证结果可能包括错误和警告信息，开发人员需根据实际情况进行判断和处理。
④分析验证结果
通过对验证结果的分析，可以判断验证是否成功。例如，一般让设计人员查看验证报告，并记录以下信息：
--电路正常运行的情况下，所有正确的输入信号都能正确产生输出信号的情况；
--所尝试的测试样例中，所有错误的输入信号产生了预期的错误输出接口情况。
5.实验结果和分析
本文在FPGA平台上验证了本文提出的基于PSA的集成电路形式验证方法。通过对实验数据的分析和统计，我们发现在所有验证样例中，97%以上的案例成功通过验证，而其中一些样例是以较低的