第39卷第5期2019年9月
核电子学与探测技术
Nuclear Electronics&Detection Technology
Vol.39No.5
Sep.2019
钱一名，刘志凯，梁成华，王冬
（中核控制系统工程有限公司，北京100176）
摘要：提出了一种基于形式化技术的功能验证方法，对可编程逻辑模块级/子系统级进行功能验证。通过实例逻辑验证表明，依据功能验证平台，按照验证步骤对设计程序进行缺陷检查，测试用例能保证RTL代码结构和功能覆盖达到100%，并提供验证报告方便快速定位并进行缺陷修复，大大地降低了仪控系统在核电厂实际使用过程中出现问题的概率，保证核电安全级仪控系统稳定性、可靠性和安全性的要求，为仪控系统提供更充分更有力的依据。 关键词：可编程逻辑技术；核安全级；形式化技术：功能验证
中图分类号：TM623文献标志码：B
随着可编程逻辑技术的日益成熟，在核电厂安全级系统中使用越来越广泛，但随之带来的测试与验证问题也越来越突出。目前，基于传统仿真的验证技术能在一定程度上提高可编程逻辑模块级/子系统级设计的验证质量，但仿真验证技术存在需要相当多的测试人员花大量精力去解决的难题，如进行测试用例开发、测试环境的搭建和调试等。基于断言的验证方法（ABV）是业界广泛使用成熟的验证方法学⑴，其采用的System Verilog语言⑵，易掌握，使用专业的硬件逻辑功能验证语言如SVA.PSL来精确描述各设计模块的高级/低级功能/时序需求,SVA/PSL功能需求可以插入在RTL代码中也可以单独存放在文件中。ABV方法学期望后端的验证手段能够精确全面判定在各种设计允许的数据场景下RTL代码都是否正确实现 收稿日期：2018-06-21
作者简介：钱一名（1986—），女，湖北天门人，工程师，主要从事核电站安全级数字化仪控系统技术研究。文章编号：0258-0934（2019）5-0621-05
了全部SVA/PSL功能需求，若未正确实现某个需求，后端的验证手段也能自动产生一个能表明代码是 如何违反这个需求的预期行为的输入信号数据序列波形（反例），这个反例方便设计/测试验证人员更加容易到问题所在。
本课题提出的基于ABV的功能验证方法学的形式化验证解决了上述问题。所提验证方案不需要设计测试用例序列和搭建测试环境，只需要编写各模块的SVA/PSL功能需求集，验证平台能自动验证RTL代码是否完整、正确地实现了各设计模块的所有功能需求；能自动分析、生成不满足特定功能/时序需求的具体测试用例序列的波形图，结合RTL代码来理解和修正RTL模块设计；对于已通过验证的模块提供灵活的集成方式合成更大的模块进行验证；提供精确到RTL代码行的详细验证报告表明功能验证的覆盖程度。
1形式化验证简介
形式化验证⑶是基于已建立的形式化需求规格，对实现需求规格的系统相关特性进行
621
分析和验证，以此评判系统是否满足需求期望的功能特性，可以最大限度地理解和分析系统，并尽可能地发现需求与代码的不一致性、模糊性、不完备性等错误，主要技术包括模型检查和定理证明。
1.1模型检查
模型检查⑶是一种基于有限模型并检验该模型的期望行为特性的一种技术。即对状态空间的蛮力搜索，而模型的有限性确保了搜索的终止性。它有两种主要方法。一种是时态模型检查，以时态逻辑形式表述需求规格，系统模拟为有限状态迁移的系统。有限的搜索过程用来检验给定的有限状态迁移系统是否满足需求规格的模型。另一种方法，以自动机方式给出需求规格，系统模拟为自动机模型，与需求规格进行比较，确定其行为是否与需求规格的自动机模型一致。
目前，模型检查技术已在硬件电路、协议的验证中得到了大量成功的工业级应用。贝尔实验室利用模型检查对高级数据链路控制器进行功能验证,6个功能需求规格中5个验证无误，只有1个失败，并进一步发现了影响其失败的Bug。基于SMV输入语言建立的IEEE Futurebus+896.1-1991标准下cache一致协议的精确模型，验证了迁移系统模型满足cache 一致性需求规格，从验证中发现了此前并未到的潜在的协议设计的错误。这项工作也是第一次从IEEE标准中发现错误。
1.2定理证明
定理证明⑶是以数学逻辑公式表示系统及其特性的形式化技术。逻辑公式由具有公理和推理规则的形式化系统给出。即从系统公理中寻特性证明的过程。不同于模型检查，定理证明适合于处理无限状态空间问题。定理证明系统分为自动式和交互式两种类型。前者是通用搜索过程，适用于解决各种组合问题；后者适合于系统的开发形式化和机械形式化，对使用人员的数理逻辑能力要求较高，易用性不好。
定理证明主要在硬件和软件设计的安全特性验证中得到了应用。如基于符号代数运算的自动定理证明用于证明Pentium中SRT算法的正确性，检查出了一个由商数字选择表引起的错误；PowerPC和System/390中寄存器传输级、门级、晶体管级的硬件设计模拟为布尔状态迁移函数，基于OBDD的算法用来检验不同设计级上状态迁移函数的等价性。
2功能验证平台
2.1功能验证平台技术架构
采用由上海迪真计算机公司提供的技术支持和其代理的德国ONESPIN公司的可编程逻辑功能验证产品Design Verification Suite（简称DV）的软件功能验证平台。DV中实现了形式化验证技术与ABV的功能验证方法学的结合，拥有专利的、成熟的、丰富的先进形式化验证引擎技术，这些引擎包含模型检查引擎类以及自动理论证明类。其功能验证平台技术架构示于图l o
设计读入：
Verilog System Verilog,
VHDL
MIX.
断•言约束
SVA PSL C
设计代码
Verilog.SysVlog.
VHDL SystemC
启发式引擎控制器
k
F
Observation
Coverage
可观测性强的
功能覆盖统计
Debug
Environment
提供Debuger环境
对问题进行深度剖析Multilingual In p ut
支持多种RTL语背及
SVA/PSL需求语言
Formal Model Proof Engines包含
自动生矍罷鹭态空间驟探醫響
图1DV功能验证平台技术架构
622
2.2底层原理过程
功能验证平台的主要底层原理过程:①利用与可编程逻辑相关的专业验证语言SVA/ PSL来描述功能/时序需求;②然后底层的形式化前处理引擎自动理解RTL设计以及SVA/ PSL需求;③接着形式化后处理引擎去遍历整个位模型空间的所有可能的系统状态及状态迁移序列，去搜索计算是否在状态空间中存在使得检查器逻辑为假的状态迁移序列;④对需求没翻译完整、需求之间有逻辑/时序矛盾、需求本身有逻辑/时序矛盾等问题情况，进行自动检查并有效呈现给使用者进行需求集本身的完善修正。
2.3功能验证步骤流程
图2给出了基于DV的形式化功能验证的步骤流程。
图2形式化功能验证步骤流程
(1)INSPECT：精确识别出被测RTL代码中所有运行时数组越界、运行时除零、读写竞争、数值范围越界等多种典型低级缺陷，自动分析出死代码、不可达条件、不可达FSM状态、不可达FSM转移，对于可达的代码部分能自动生成测试用例序列证明其可达性，包括语句覆盖、分支覆盖、表达式覆盖、翻转覆盖、状态机覆盖。避免了在功能验证过程中才发现并由其引发的相关定位分析这些低级缺陷的无谓消耗。
(2)VERIFY：对设计的模块及子系统级别进行自动形式化功能验证，读入人工编写的被测设计模块的SVA/PSL功能/时序需求，自动分析RTL代码是否全部正确实现了预定的功能/时序需求，自动生成RTL代码违反需求的应用情况和具体的信号波形测试用例。
(3)CERTIFY：自动生成详细功能验证覆盖报告，自动检查SVA/PSL功能需求集合自身的正确性(或对于错误的功能描述则生成测试序列波形说明其错误性)，检查功能需求描述集合的完整性包括验证RTL模块的所有输入信号组合的完整性、验证所有模块可能的行为序列组合的完整性，从而多方位引导测试验证人员形成完备正确的功能需求集，保证验证的完整性。
2.4功能验证平台技术特点
功能验证平台技术特点主要包括:①支持ABV验证方法学;②具有成熟、丰富的先进形式化验证引擎技术;③能在RTL代码运行时进行缺陷检查及代码定位，包括数组越界、运行时除零、读写竞争、数值范围越界等多种典型低级缺陷；自动分析死代码、不可达FSM状态、不可达FSM转移，对于可达的代码能自动生成测试用例序列证明其可达性，包括语句、分支、表达式、翻转、状态机覆盖;④支持对设计进行模块级/子系统级功能验证;⑤支持对多种RTL设计语言的功能验证;⑥支持以SVA/PSL验证语言描述设计的高级、低级功能/时序需求，快速描述任意类型的模块行为，如算数操作、逻辑运算、关系运算、位运算、时序关系等;⑦能自动验证RTL代码是否完整、正确地实现了各设计模块所有的功能/时序需求，并提供波形图以及与RTL代码联动的动态观察方式;⑧提供精确到RTL代码行且能证明功能验证的充分性程度的详细验证报告，包括精确到RTL代码行的功能需求集的验证覆盖信息，根据信息可以删除多余的RTL代码或者将功能需求补充完整。
3实际验证案例一3选2逻辑功能验证
3.13选2逻辑的SVA形式化需求描述
测试验证人员根据REQ1使用SVA语言来形式化描述模块功能需求，一共六大功能需求。①验证三通道基本信号的选通逻辑；②验证当三个通道基本信号都参与表决时的逻辑要求;③验证当只有两个通道
基本信号都参与表决时的逻辑要求。测试验证人员在用SVA翻译原始需求的过程中，一定要注意与原始需求相匹配，不能关注代码的实现方式。
623
3.2设计代码的前端处理-缺陷检查
验证平台自动对RTL代码进行运行时的缺陷检查，包括低级缺陷、死代码、可达与不可达代码。如模块不存在任何低级缺陷，可以进入功能验证阶段。对于可达的代码部分能自动生成测试用例序列波形证明其可达性，包括语句、分支、表达式、翻转、状态机覆盖，也可以导出波形。
3.3自动功能验证
DV软件自动利用形式化验证引擎来检查RTL代码是否正确实现了ge2oo3-function-verification-vl.sva文件中所有SVA功能/时序需求，验证代码是否与需求完全一致。同时还可以对每个需求自动生成一个正向的测试波形序列，测试波形序列能自动导出作为功能验证过程的数据依据。
3.4功能覆盖分析
DV功能验证平台提供的功能覆盖分析极其重要，它表明了在验证的当前状态下，被测代码的功能域与SVA/PSL形式化功能集合域的重叠关系，譬如:①如果形式化功能域的某些需求无法匹配追踪到相应的被测代码，则说明代码还没有实现这些需求即代码小于需求，设计人员需要增加代码来实现这些需求。②如果形式化功能域的所有需求都能匹配追踪到被测代码，但还有代码与目前的任何需求都不匹
配，则说明代码大于需求。若确认需求没有遗漏，则说明代码出了多余逻辑，应该删除；若确认需求并不完善，则可以根据代码中未匹配部分增加SVA需求集。
DV功能验证平台提供两个层次的功能覆盖分析:①针对单个需求与被测RTL代码的追踪关系;②针对所有需求与被测RTL代码的追踪关系统计。测试结果表明，当所有需求验证成功后，代码中有100%的语句和100%的分支与需求集合相关。所有需求与代码完全一致，功能域完全重叠即需求等于代码。
3.5完善需求并自动回归验证
通过对代码分析可知功能域完全重叠即需求等于代码，并不需要回归测试，若出现黄显示，则需要对黄部分进行分析，增加对缺少部分的需求描述，进行回归验证，直到所有的需求等于代码验证结束。
4结论
本文研究的核电厂可编程逻辑项目以控制逻辑算法和数据协议实现为主，适合采用形式化验证技术与基于ABV的功能验证方法学相结合的方式对模块/子系统级进行功能验证，通过实例验证表明验证过程和结论清晰，能及时发现、定位、分析、修正模块/子系统级的功能缺陷，避免这些缺陷流入后续系统级的验证工作中，给其仿真、联调带来大工作量的归零过程。
参考文献：
[1]Janick Bergeron,Eduard Cemy,Alan Hunter,et al.
System Verilog验证方法学[M].北京：北京航空航天大学出版社,2007:33-84.
[2]斯皮尔.System Verilog验证[M].北京：科学出版
社,2009.
[3]古天龙.软件开发的形式化方法[M].北京：高等
教育岀版社,2005.
Formal Functional Verification for Nuclear Safety Level System
QIAN Yi-ming,LIU Zhi-kai,LIANG Cheng-hua,WANG Dong
(CNNC China Nuclear Control System Engineering Co,Ltd,Beijing100176,China)
Abstract:A formal functional verification method is proposed to verify the modules and its subsystem
s based on formal technology.The example logic verification results show that verifiers defect inspection of the design program based on functional verification platforms and by following the steps of the verification method.The test cases can guarantee that the RTL code structure covers and coverage up to100%.And 624
provide detail verification reports to help designers quickly locate and repair.Substantially reduce the probability of the problem during the process of the control system in nuclear power station,that ensure the stability^reliability and security of nuclear safety level system requirements,and provide stronger and fuller basis for the instrumentation control system.
Key words:programmable logic technology；nuclear safety level；formal technology；functional verification
625
豫公网安备41160202000603
站长QQ:729038198
关于我们
投诉建议