Verifying Stacks and Queues Using Symbolic Simulation Techniques

This paper presents a formal verification method based on logic simulation. In our method, using symbolic values even circuits which include data paths can be verified without abstraction of data paths. Our verifier extracts a transition relation from the state graph (given as a specification) which is expressed using symbolic values, and verifies based on simulation using those symbolic values if the circuit behaves correctly with respect to each transition of the specification. If the verifier terminates with "correct", then we can guarantee that for any applicable input vector sequences, the circuit and the specification behaves identically. We have implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it.

基于最大半环的DP问题函数式建模与验证

针对在DP问题算法的设计和推导中缺乏对DP问题函数式建模算法与验证的细致研究,该文首先通过深入分析最大半环与DP类问题递推关系式的对应关系,找到满足最大半环性质的一类DP问题,使用最大半环对该类DP问题进行函数式建模;然后将实现的基于最大半环的函数式建模算法与Wimmer定义的递归函数结果进行等价性验证,从而保证了函数式建模算法的正确性;最后通过对lcs问题案例分析,验证了该方法的可行性和有效性.

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

场景导向的雷达系统模型设计与仿真方法研究

由于雷达系统工作过程、接口交互目前主要采用文本的形式进行描述,导致了系统的整体验证过度依赖实物,因而带来了验证周期长、设计修正成本高等问题。针对研制过程中存在的问题,采用MBSE思想,开展了以雷达场景为导向的需求分析,并根据雷达系统功能成熟度、复杂度等特点,详细阐述了适用于不同雷达的功能分析方法,重点介绍了雷达系统与分系统的架构设计和三层仿真验证方法,将系统调试阶段的部分验证环节提前到系统设计初期,解决了过度依赖实物的痛点问题,对雷达系统新研制模式的应用具有积极的意义。

民用飞机功能和可靠性试飞分析及其价值利用研究

本文根据对民用飞机功能和可靠性试飞组织模式的研究,重点阐述如何通过高效的飞行组织完成试飞任务,并通过对功能和可靠性试飞技术的研究,探索利用好研制批试飞机,开展模拟航线运营验证试飞,为客户创造价值的方法。

基于UVM的AXI4总线自验证平台设计

基于通用验证方法学(Universal Verification Methodology, UVM)搭建了可用于AXI4总线协议的验证平台,该验证环境针对基于AMBA总线的AXI4 IP功能的验证需求搭建。该验证平台结合通用功能组件设计总线功能模型,设置受约束的随机激励与定向测试,构造不同的测试用例,完成验证结果的自动校验,提高了验证效率和平台的可移植性。在AXI4多主多从的互联结构下,对乱序传输、突发传输以及混合交叉读写类型等进行充分验证。验证进度可从仿真日志、覆盖率指标以及波形图直观判断,搭建的验证平台完成了AXI4总线的验证任务。

Formal methods, statistical debugging and exploratory analysis in support of system development: Towards a verification and validation calculator tool

In this paper,we propose an approach to formally verify and rigorously validate a simulation system against the specification of the real system.We implement the approach in a verification and validation calculator tool that takes as input a set of statements that capture the requirements,internal conditions of the system and expected outputs of the real system and produces as output whether the simulation satisfies the requirements,faithfully represents the internal conditions of the system and produces the expected outputs.We provide a use case to show how subject matter experts can apply the tool.

面向航电系统任务安全性的形式化建模与验证

针对航电系统任务安全性分析缺少仿真与验证手段问题,提出了一种面向航电系统任务安全性的形式化建模与验证方法。首先,基于时间自动机理论与民航规章建立标准运行条件下航电系统任务过程的形式化模型。随后,将危险致因和安全约束分别以状态变迁的方式注入该模型,建立航电系统任务安全性验证模型。最后,通过遍历状态空间验证模型的活性、危险致因的可达性以及安全约束的充分性,实现任务安全性分析结果的自动化验证。实验结果表明,所提方法具有可行性和有效性,能够为持续进行的航电系统任务安全性分析和设计提供模型基础,确保分析结果的正确性和完整性。

基于时序逻辑的仿真系统行为验证方法

仿真系统行为可信性评估是一项复杂的任务,需要综合利用多种方法、从多个角度对仿真系统的行为进行验证。针对仿真系统行为验证既需要具有客观性又需要考虑领域专家宝贵经验的需求,借鉴形式化验证技术的思想,提出基于时序逻辑的仿真系统行为验证方法。该方法首先根据真实系统和实测数据,结合专家经验,对所关注的仿真系统行为属性进行提取;其次,利用时序逻辑语言对提取的待验证属性进行形式化描述;然后,运行仿真系统并获得相应的输出数据,利用验证算法自动检验仿真数据是否满足给定的属性,从而实现行为验证;基于对武器装备体系对抗仿真领域的验证属性分析,选取度量区间时序逻辑作为属性的形式化描述语言;最后,通过一个防空对抗仿真系统的验证示例,表明了该方法的有效性。

PHM仿真试验系统设计与应用

PHM系统是保障机载设备稳定安全运行的重要工具;通过构建PHM仿真试验系统,可以对系统架构、总线接口、数据处理、分区存储等系统功能进行仿真验证,以便尽早发现PHM系统设计初期存在的各种问题,及时对方案进行改进和优化,降低系统研制的风险;对PHM仿真试验系统的设计进行了研究,提出了一种PHM仿真试验系统设计与应用方法,从总体层次、软硬件设计等方面介绍仿真试验系统的组成和功能设计;搭建飞机级及各区域级的仿真设备,构建基于总线通讯的交联仿真网,支持数据、模型、流程等功能的仿真,并在最后给出了仿真试验的主要流程;实际应用表明,本方法能够较好地支撑仿真验证试验,从而缩短试验周期,提高研制效率,为系统设计工作提供支撑从PHM系统功能验证的角度为PHM系统研制提供支撑。

一种嵌套中断系统的建模和分析方法

在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先,提出基于投影时序逻辑(projection temporal logic,简称PTL)的定义,并将这种定义推广到包含任意多中断事件的中断系统上,从而得出嵌套中断系统基于投影时序逻辑的形式化模型;其次,使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言(modeling,simulation and verification language,简称MSVL),并扩展MSVL语言的解释器,使其可以对嵌套中断系统进行建模仿真和验证;最后,通过一个实例展现所提出方法的正确性和实用性.

微处理器功能验证方法研究

微处理器验证是微处理器设计的关键环节。该文探讨了微处理器模拟、硬件仿真、形式验证等方法的原理、特点和适用场合,提出了进行多层次微处理器功能验证的总体思路。

面向CPU芯片的验证技术研究

CPU芯片规模大、复杂度高,在芯片设计的不同阶段进行多层次的验证,保证芯片的正确性非常关键。文章探讨了模拟验证、FPGA仿真、形式验证和静态时序分析等验证方法,提出了一种多级验证体系方法,实现CPU芯片的多层次验证,并成功地验证了自行设计的微处理器的正确性和兼容性。

龙芯2号微处理器的功能验证

开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务·龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍,如何保证设计的正确性是一个重大挑战·简单的系统级测试已经不能满足设计的需要,这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误·主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法·模拟仿真是主要的验证手段,新的形式化验证方法也应用到了验证流程当中·

一种面向微处理器验证的分层随机激励方法

针对日趋复杂的微处理器功能验证,提出一种基于分层思想的受限随机激励产生方法,通过测试层、场景层、功能层和指令层的多层约束,实现随机激励在不同粒度范围的高度可控性,精炼测试空间,加快验证的收敛速度。采用可配置的功能库,将处理器功能行为单元作为随机激励的构建基础,产生逻辑功能与通信接口结合的随机激励,实现系列处理器的验证复用。CKCore处理器验证的实验结果表明,该方法与受限随机激励相比,在功能覆盖率相同的情况下,激励编写量减少60%;在仿真时间相同的情况下,功能和代码覆盖率分别改善10%和5%以上,有效提高处理器验证的质量和效率。

紫花苜蓿不同根系分布模式的土壤水分模拟和验证

根系分布影响着土壤水分养分吸收,实测根系分布费时费力,经验根系分布函数参数简单,应用方便。该研究在田间采用苜蓿栽培土柱试验,测定根系分布,并将其和不同经验根系分布函数分别应用于Hydrus-1D对土壤水分进行动态模拟,通过土壤水分实测值和模拟值比较,验证分析了经验根系分布函数的适用性以及对土壤水分动态变化的影响。结果表明:拟合的根系分布、Prasad分布、Hoffman和van Genuchten分布3种根系分布函数的根长密度模拟值与36cm以下的根长密度实测值较为吻合,Raats根系分布模拟值与实测值及其他分布函数则差别较大。不同根系分布下土壤水分模拟差别不大,平均相对均方根误差在3.5%以下。非胁迫生长条件下,Prasad根系分布、Hoffman和vanGenuchten根系分布都可描述紫花苜蓿实际根系分布状况。

OBDD变量排序的自适应选择算法

有序的二叉决策图（ＯＢＤＤ）是形式验证领域的基础技术之一．由于ＯＢＤＤ的大小对变量序非常敏感，使得变量排序问题成为最关键的一个问题．首先将ＯＢＤＤ变量排序问题分解为３ 个子问题，定义了若干启发信息，给出了上述子问题的启发式解法；然后提出了一个变量排序自适应选择算法，从若干候选变量序中选出“最佳”的变量序．最后给出了ＩＳＣＡＳ８５ 电路的实验结果．

龙腾C1微处理器的功能验证

微处理器的功能验证是一项复杂而重要的工作。文章在进行龙腾C1微处理器的功能验证时,针对其指令集的特点,将指令集分为运算类和非运算类两种。根据两种指令各自不同的特点,文章分别提出了使用嵌入汇编语言的C语言参照模型和使用基于真实处理器执行结果的TRACE文件参照模型。在参照模型基础之上,实现了仿真结果的自动检查和基于覆盖率的分析。同时,为了加速仿真验证的速度,使用了FPGA验证平台进行功能验证,可以运行操作系统级的测试程序。

微处理器功能验证程序生成

根据指令集构造的指令功能、语法格式和语义要求,建立了微处理器指令类型集合和指令操作数集合;以此为基础,为每个指令类型集合构建一个指令生成模型.根据指令生成模型、验证计划等创建微处理器功能验证程序模板,并结合微处理器流水线状态控制部件的有限状态机的基本状态转移路径,提出一种指令序列的功能验证方法.根据程序模板实现功能验证程序伪随机生成.实验结果表明:采用该方法可以高效生成功能覆盖率高、仿真时间短的RISC3200功能验证程序.

Verilog Testbench设计技巧和策略

仿真Testbench的设计是Top-Down流程中非常关键的一个环节,但是很多设计者却感到困难较大。实际上,verilogHDL有着较强的行为建模能力,可以方便地写出更加高效、简洁的行为模型。论文结合一个ATM测试平台的Testbench设计,讨论了Testbench的结构和总线功能模型(BFM),并对使用BFM模型进行Testbench设计的策略和方法进行了探讨,希望能对广大设计者有所帮助。