形式验证

摘要： 多周期路径是将复杂电路运算拆分在多个时钟周期完成,从而提高电路总体运行频率的一种方法;在设计和验证中,多周期路径约束错误会导致设计迭代反复和验证误报;文章对多周期路径的产生机理和设计验证中常见的问题进行分类分析,提出一种用静态时序分析和形式验证结合来查找设计中的多周期路径的方法,首先通过静态时序分析,查找出时序违例的路径,针对这些路径,插入设计的检测电路,检测电路主要通过检测目的触发器采样控制信号有效时间,来判断该路径是否为多周期路径;采用基于断言的形式验证,用自动化的手段检测多周期路径;实践结果表明,该方法针对两种时钟下的多周期路径,能够100%准确地检测出违例的多周期路径,避免多周期路径错误约束,省略人工分析和动态仿真确认多周期路径环节。

摘要： 随着科学技术及人们生活水平的不断提升,楼宇智能化综合安防监控系统得到了广泛的应用,但由于系统设计以及硬件设备等因素的影响下,系统的安全等级往往无法达到理想的要求。为了实现楼宇安全防护具有更加科学、合理的系统设计,本研究将基于物联网技术,对楼宇智能化综合安防监控系统的硬件、软件模块实施优化设计,并通过实验分析的形式验证本研究中所提出设计的安全防护效果。

摘要： 作为EDA工具的重要组成部分,逻辑功能更正技术的重要性不可忽视。本文介绍了逻辑功能更正技术在EDA工具中的地位和应用,简单介绍了逻辑功能更正技术的理论发展过程及其产品发展历程,最后展望了逻辑功能更正技术的未来发展趋势。

摘要： 数据的快速增长限制了传统存储技术存储和管理数据的能力,云存储系统应运而生.云存储系统最重要的特征是数据以块的形式存储,且每个块被视为一个独立的存储单元.因此,云存储系统通常包含两种存储单元:原始地址和块地址,这使得云存储系统与传统内存系统相比有着显著的不同.从而,如何保证云存储系统的可靠性成为了有待解决的难题.本文基于分离逻辑提出了一种系统方法来验证云存储系统管理程序的正确性.主要贡献包括:(1)提出了一种建模语言来描述云存储管理;(2)扩展了分离逻辑的断言语言来描述云存储系统中有关块的属性;(3)在上述两个语言的基础上,提出了一套霍尔型的规范规则对云存储系统进行推理.规范的前置和后置条件都以断言对的形式给出.运用这些方法,能够验证云存储管理程序的正确性.

摘要： 形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.

摘要： 形态变化和虚词运用,两者异曲同工,殊途同归.对汉语而言,虚词在运用的广度、深度、精度、频度方面是任何其他语言都无法比拟的,因此我们必须重新审视虚词在汉语中的定位和作用.在典型实词与典型虚词之间,存在着一个过渡地带,为此,我们提出"广义虚词"这一新的理念.汉语虚词研究将形成六个新趋势:(1)国际汉语教学的紧迫需求促使我们重新认识虚词在汉语语法体系中无可替代的主导地位;(2)虚词语法意义的确认,关键在于形式上的验证,要为每个虚词义项建立"定位框架";(3)虚词研究必须在一定的"语境"背景下才能有效地进行;(4)虚词研究的深化,必须在时间的纵轴和空间的横轴结合上下功夫;(5)重要虚词的个案深入研究和范畴虚词的比较研究将有机地结合起来;(6)虚词研究必须在研究方法和工具的现代化与网络化方面与时俱进.

摘要： 现如今的SoC中,几乎都包含PAD控制逻辑电路(Pad Control Logic,PCL),以此来实现PAD复用技术,从而满足芯片面积不断缩小但功能不断增加的需求.针对PCL极其繁琐复杂的控制逻辑与其在芯片中举足轻重的地位,本文介绍了一种基于Jasper验证平台,采用SVA断言(System Verilog Assertion)来进行属性检查(Property Check)的PCL形式验证(Formal Verification)方法.与传统动态仿真验证方法相比,该方法无需搭建Test Bench,无需编写Test case,具有验证覆盖范围广、验证速度快及验证方式简便等特点.通过已有实际项目的证实,该方法可有效提高PCL验证的覆盖程度,极大缩短验证周期,有效节省验证精力.

摘要： With complex multi-clock-domain functional blocks integrated into Soc, errors in cross domain crossing (CDC) signals path design can lead to metastability, glitches or other functional failures. The issues caused by metastability and traditional verification methods are introduced. Compared to the traditional dynamic simulation method, which is time consuming and non-exhaustive, static formal verification leverages the power of mathematical method and checks the design exhaustively. It helps to improve Qo R of verification, and is quick, highly efficient and exhaustive. Various CDC and reset errors found by static formal method are given as examples to illustrate the challenges in multi-clock-domain designs. Verification results from design blocks of different scale are compared and analyzed.%Soc芯片的各个复杂功能模块中通常包含多个时钟域和复位域, 跨时钟域信号路径设计的错误可能引起亚稳态问题进而导致设计故障.本文介绍了亚稳态的危害、以及传统的验证方法.相对于传统动态仿真方法耗时、容易遗漏的缺点, 静态形式验证利用数学方法进行穷举, 可以高效、快速、完备的检查可能出现的所有场景, 提高验证的质量和效率.本文通过实例, 利用静态形式验证技术对不同规模的设计中存在的跨时钟域和复位问题进行检视, 并对验证结果进行了对比和分析.

摘要： 为解决SoC(system on chip)设计中无法在RTL(register transfer level)阶段验证毛刺存在及其影响问题,提出一种使用形式验证技术在RTL级检测毛刺的方法,同时提出RTL级毛刺故障注入方法.通过检测逻辑门输入同时翻转的原理设计毛刺检测电路,使用形式验证中断言实现检测电路;基于毛刺检测电路和毛刺在时序逻辑的影响,设计其影响等价电路,实现RTL级毛刺故障注入.实验结果表明,该方法能够准确检测毛刺存在并通过毛刺注入分析,进一步发现毛刺对电路功能的影响,将对毛刺的检测和影响分析提前到RTL级,减少了因后期毛刺故障带来的设计迭代和周期成本.

摘要： 内存管理单元(Memory Management Unit,MMU)和缓存(Cache)在现代微处理器(CPU)设计中应用广泛,它们在提高CPU性能的同时,也增加了CPU设计验证的复杂度.本文提出了一个公理系统对带有MMU和Cache的CPU结构进行形式化描述,给出一种对带有MMU和Cache的指令通路进行形式验证的定理证明方法,实现了一个自动证明工具并使用该工具高效地完成了对MIPS指令集83条指令指令通路的形式验证.

摘要： 编译器是重要的系统开发工具,其安全可靠性对安全攸关软件的开发有着重要影响.传统检测编译器错误的方法是进行大量的测试,但测试存在局限性且难以达到完全覆盖.近年来,形式化验证方法在编译器的验证中得到了广泛的关注,但当前的形式验证方法却存在证明复杂度高、验证能力弱、自动化程序低等问题.本文提出了一种基于安全C子集形式文法的编译器验证方法,通过形式文法对应的下推自动机识别出源程序中的C文法单元,把对编译器的形式验证转化为了对有限的C文法单元的验证.文中引入了一阶逻辑的公理系统和专用公理,在此公理系统上通过定理证明的方式,完成了C文法单元和目标码模式的语义一致性验证,从而完成了对编译器的形式验证的过程.

摘要： 本文针对石油石化行业安全技术研究中的故障预报技术进行了讨论,提出了一种基于混杂形式验证进行故障预报的新技术,该方法将故障预报技术转化为混杂系统形式验证研究,利用MPT软件实现了故障预报,并根据预报结果制定维修计划,与常规维修计划相结合,可以保证设备的最大效率运行,减少不必要的成本浪费.该方法简单可靠,为石化行业故障预报技术提供了一种新方法.

摘要： 本文主要讲述了在使用Formality作形式验证时发现了综合前后仿真失配的各种问题,并对其中由于不良的代码风格所引起的问题进行了举例分析,而且对如何修改程序提出了自己的建议。

摘要： 混杂系统的形式验证中，确定近似商迁移系统的迁移关系，需要根据初始状态集计算系统可达集的流管道近似。本文针对线性定常系统的特点，结合凸多面体的性质，给出了当初始状态区域为凸多面体且不变集内连续状态方程为线性定常时，系统可达集的演化规律并加以证明。依据这些结论对混杂系统形式验证中迁移关系的计算方法进行了简化，提出了通过顶点仿真与流管道近似相结合的迁移关系计算方法。最后结合常压炉温度控制系统的例子，说明了采用顶点仿真与流管道近似相结合方法获得商迁移关系的过程，并与流管道近似的方法进行了对比。

摘要： 基于可满足性(SAT)的模型检验技术已逐渐成为主流的形式验证技术.在RTL,SAT问题的复杂性表现在位(bit)和字(word)数据类型并存和多样化的约束关系。其中,对数据通路的约束求解尤为关键.本文提出采用二元CSP来求解RTL数据通路的可满足性问题,并给出了算法的流程以及流程中每个步骤的实现方法。我们初步实现了算法,并对实验进行了设计.实验结果表明,即使是在没有采取很多优化策略的条件下,基于CSP的方法仍有较好的性能.这说明了本文方法的可行性和进一步研究的价值.

摘要： 在SOC芯片的开发中,功能覆盖率与代码覆盖率是检查验证完备性的标准.在大规模的模拟验证之后剩余的未覆盖点,如果继续使用伪随机环境进行验证往往步履维艰.随着Formal验证技术的逐渐成熟,采用Formal验证的思想和工具找到未覆盖点中的不可达点,对加速芯片验证后期的覆盖率收敛有着事半功倍的效果.

摘要： 在SOC芯片的开发中,功能覆盖率与代码覆盖率是检查验证完备性的标准.在大规模的模拟验证之后剩余的未覆盖点,如果继续使用伪随机环境进行验证往往步履维艰.随着Formal验证技术的逐渐成熟,采用Formal验证的思想和工具找到未覆盖点中的不可达点,对加速芯片验证后期的覆盖率收敛有着事半功倍的效果.

摘要： 在SOC芯片的开发中,功能覆盖率与代码覆盖率是检查验证完备性的标准.在大规模的模拟验证之后剩余的未覆盖点,如果继续使用伪随机环境进行验证往往步履维艰.随着Formal验证技术的逐渐成熟,采用Formal验证的思想和工具找到未覆盖点中的不可达点,对加速芯片验证后期的覆盖率收敛有着事半功倍的效果.

摘要： 在SOC芯片的开发中,功能覆盖率与代码覆盖率是检查验证完备性的标准.在大规模的模拟验证之后剩余的未覆盖点,如果继续使用伪随机环境进行验证往往步履维艰.随着Formal验证技术的逐渐成熟,采用Formal验证的思想和工具找到未覆盖点中的不可达点,对加速芯片验证后期的覆盖率收敛有着事半功倍的效果.

摘要： 本发明公开了一种基于形式化的FPGA软件安全性验证方法及验证平台，属于可编程逻辑器件软件测试技术领域。其方法包括，获取FPGA软件通用安全性设计要求信息，根据FPGA软件通用设计要求信息生成SVA断言模板；提取拟验证的安全性设计准则及待测FPGA软件信息，并从待测FPGA软件中提取待测信号信息；将拟验证的安全性设计准则与SVA断言模板进行映射，从SVA断言模板选取目标SVA断言并生成待执行SVA断言；将待执行SVA断言以及待测FPGA软件的源代码输入形式化验证工具完成形式化验证并输出安全性验证报告。本发明通过上述方法和执行该方法的验证平台解决了通过人工编写测试用例，并进行仿真验证所带来的开发周期长、通用化程度低等诸多问题和不足。

摘要： 本发明公开了一种应用于针对源代码的运行时形式化验证方法中的验证系统，所述系统包括：切面类文件及监视器文件自动生成工具，用户可定义描述程序性质的LTL线性时态逻辑公式以及配置文件，通过该工具自动生成监测程序性质的切面类以及监测程序状态的检测器；通过将修改后的SystemC的仿真内核与运用切面类形式的插桩源代码，以及检测器联合编译，形成可运行目标文件，运行该文件，以检测程序的动态执行，实时验证系统的性质。本发明可以应用到嵌入式系统及大型软件系统的形式化验证中，能够提高软件的安全性、可靠性。

摘要： 本发明公开了一种基于形式化的FPGA软件安全性验证方法及验证平台，属于可编程逻辑器件软件测试技术领域。其方法包括，获取FPGA软件通用安全性设计要求信息，根据FPGA软件通用设计要求信息生成SVA断言模板；提取拟验证的安全性设计准则及待测FPGA软件信息，并从待测FPGA软件中提取待测信号信息；将拟验证的安全性设计准则与SVA断言模板进行映射，从SVA断言模板选取目标SVA断言并生成待执行SVA断言；将待执行SVA断言以及待测FPGA软件的源代码输入形式化验证工具完成形式化验证并输出安全性验证报告。本发明通过上述方法和执行该方法的验证平台解决了通过人工编写测试用例，并进行仿真验证所带来的开发周期长、通用化程度低等诸多问题和不足。

摘要： 本申请提供一种基于形式化验证快速收敛覆盖率的验证方法及装置，DUT为amba总线的协议转换模块，如AHB2APB模块、AXI2AHB模块或AXI2APB模块等。针对能够覆盖的DUT行为，利用形式化仿真器穷举输入信号的行为并生成测试激励，基于统一覆盖率的验证结果分析，如果验证结果达不到要求，将结果反馈给验证计划，使得验证平台更容易建立、覆盖率更容易收敛，通过形式化验证避免了在验证至覆盖率较高后的验证效率降低，缩短了覆盖率收敛时间，提高了验证效率。

摘要： 本申请提供了一种基于形式化验证的智能合约功能验证方法及装置，所述方法包括以下步骤：获取待验证的智能合约数据，对所述智能合约数据进行编译，判断编译是否通过，若编译通过，将所述智能合约数据转化为中间语言，根据所述中间语言，通过规则库生成测试用例，根据所述测试用例验证智能合约数据，得到验证结果。本申请通过依据solidity的行为将其抽象为模型可识别的中间验证语言，方便模型生成测试用例。根据测试用例对智能合约内的功能进行快速验证，解决了现有智能合约验证方法审计时间长、审计效率低的问题。

摘要： 本发明提供了一种基于形式化验证的软件开发模型的验证方法，将形式化验证与软件开发过程结合起来，提高软件的高可信程度，从逻辑上保障开发软件的可靠性；发挥形式化验证在软件检错领域的对于软件开发过程中开发逻辑进行验证的作用；降低程序在非正常状态运行的可能性。本发明提高软件的高可信程度，从逻辑上保障开发软件的可靠性；在需求阶段进行验证，可以避免因为软件需求分析不合理导致重新开发的严重后果；及时发挥形式化验证在软件检错领域的对于软件开发过程中函数逻辑正确性进行验证的作用；将形式化方法引入软件开发过程，并给出具体的模型，解决了测试技术在软件检错领域的局限性问题。

摘要： 本发明公开了一种用于联锁软件形式化验证的系统模型构建方法，涉及计算机联锁系统技术领域。本发明利用采用不同的编程方法和编程语言开发的两个具有相同功能的翻译器读取联锁输入数据；并通过文件比较工具对两个具有相同功能的翻译器输出的特点格式的数据文件进行一致性校验；采用编程方法开发一个系统模型构建工具，利用该系统模型构建工具读入S1步骤中经翻译器数据转换后且通过一致性校验的特定格式文件，依据特定格式文件构建系统模型。本发明从信号人员视角出发，重点描述联锁数据层面的系统模型构建，及其与对象模型的映射关系。本发明描述的系统模型构建方法为信号人员如何依据现有联锁数据构建系统模型提供了一种思路。

摘要： 本发明公开了一种形式验证方法、装置、形式验证平台及可读存储介质，该形式验证方法包括如下步骤：获取输入待测模型的待验证源操作数；判断待验证源操作数是否属于必要验证源操作数；如果待验证源操作数不属于必要验证源操作数，则确定将待验证源操作数作为输入时，待测模型与参考模型的输出结果相等；如果待验证源操作数属于必要验证源操作数，则启动形式验证工具，将验证待验证源操作数作为输入，根据待测模型的输出结果与参考模型的输出结果进行验证。通过在启用形式验证工具验证待测模型和参考模型的输出结果是否相等之前，判断待验证源操作数是否属于待测模型的必须要验证源操作数，降低了形式验证方法出现空间爆炸问题的风险。

摘要： 本发明公开了一种基于形式化验证的芯片IO复用验证方法，包括如下步骤：S1、根据芯片规定定义，提炼芯片IO复用关系文件；S2、根据芯片IO复用关系文件，自动形成IO描述文件；S3、开启形式验证，同时导入芯片文件和IO描述文件到验证工具；S4、启动形式化验证，输出验证结果；S5、分析结果，判断是否为设计BUG。优点，本发明验证方法，相比传统的Uvm验证,基于形式化验证的IO复用验证技术使用简单，步骤简洁，大幅降低了工作量；该方法无需芯片系统级仿真运行，因而运行时间短，大幅提升了验证效率。

摘要： 本申请实施例提供一种基于形式验证对仲裁器验证的装置以及方法，所述装置包括：激励约束模块，被配置为对输入待验证仲裁器的激励信号进行约束，得到合法激励信号；辅助代码模块，被配置为基于所述合法激励信号，得到参考响应信号；断言检查模块，被配置为比较所述参考响应信号和实际响应信号，以完成对所述待验证仲裁器的逻辑验证，其中，所述实际响应信号是将所述合法激励信号输入所述待验证仲裁器得到的。本申请的一些实施例基于形式验证搭建验证仲裁器模型的速度更快，验证效率更高。