硬件设计的形式化验证技术 被引量：1

1

作者 杨泽民 范全润 《太原师范学院学报（自然科学版）》 2007年第2期54-56,共3页

形式化验证用数学可证明的方式来验证系统.硬件设计的形式化验证通常有三种方法:定理证明、等价性检验和模型检验.文章着重分析了这三种方法的优缺点,探讨了形式化验证技术所面临的挑战,以及目前形式化验证技术可能的一些研究方向.

关键词 硬件 形式化验证 定理证明 等价性检验 模型检验

下载PDF 职称材料

一种软硬件结合的控制流检测与恢复方法 被引量：4

2

作者 龚锐 陈微 +2 位作者 刘芳 戴葵 王志英 《计算机研究与发展》 EI CSCD 北大核心 2009年第2期345-351,共7页

控制流检测可以有效地提高微处理器容错能力.针对传统软件实现的控制流检测时空开销大的缺点,提出了一种软硬件结合的控制流检测与恢复方法.该方法通过编译自动插入签名数据,由硬件在分支/跳转指令之后自动执行检测,并且提供了硬件现场... 控制流检测可以有效地提高微处理器容错能力.针对传统软件实现的控制流检测时空开销大的缺点,提出了一种软硬件结合的控制流检测与恢复方法.该方法通过编译自动插入签名数据,由硬件在分支/跳转指令之后自动执行检测,并且提供了硬件现场保存和恢复机制,检测到控制流错误后无需复位系统即可以快速恢复正常控制流.基于8051体系结构实现了软硬件结合的控制流检测与恢复方法,实验结果表明与传统的软件控制流检测相比,该方法在保持相同的错误检测率的情况下,可以大幅减小二进制代码量和额外的性能开销,在发生控制流错误以后可以快速恢复正常控制流. 展开更多

关键词 软错误 控制流检测 编译签名 硬件检测 控制流恢复

下载PDF 职称材料

一种基于变量隐藏抽象的IC3硬件验证算法

3

作者 杨柳 范洪宇 +1 位作者 李东方 贺飞 《计算机科学》 CSCD 北大核心 2023年第S02期783-788,共6页

随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。... 随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。为了提高验证的规模和效率,硬件验证算法设计逐渐从底层的比特级向更高的抽象级别转变。研究目标是设计一个新型有效的字级IC3算法。针对研究目标,提出了一种将变量隐藏抽象和隐式抽象结合的字级IC3算法IC3VA。该方法尝试将变量隐藏抽象和IC3算法相结合,并设计了对应的泛化和精化方案。在开源社区和硬件验证大赛收集的测试集上和基于谓词抽象的方法进行对比,实验结果显示了基于变量隐藏抽象的IC3算法的有效性。 展开更多

关键词 硬件验证 IC3算法 形式化方法 模型检验 变量隐藏抽象

下载PDF 职称材料

一种基于PXE技术的计算机硬件网络检测方法 被引量：2

4

作者 郑宇 宋宝莲 +1 位作者 马蔚吟 罗建平 《计算机与现代化》 2010年第10期191-193,共3页

给出了一种基于PXE远程启动技术的计算机硬件检测方法,可用于计算机实验室中进行远程计算机硬件检测,在一定程度上提高了实验室的管理效率。

关键词 PXE 硬件检测 远程启动

下载PDF 职称材料

基于模型检测的硬件木马检测技术研究 被引量：2

5

作者 张启智 赵毅强 +1 位作者 高雅 马浩诚 《网络与信息安全学报》 2021年第2期57-63,共7页

硬件木马对原始电路的恶意篡改,已成为集成电路面临的核心安全威胁。为了保障集成电路的安全可信,研究人员提出了诸多硬件木马检测方法。其中,模型检测作为一种形式化验证方法,在设计阶段可有效检测出硬件木马。首先,阐述了模型检测的... 硬件木马对原始电路的恶意篡改,已成为集成电路面临的核心安全威胁。为了保障集成电路的安全可信,研究人员提出了诸多硬件木马检测方法。其中,模型检测作为一种形式化验证方法,在设计阶段可有效检测出硬件木马。首先,阐述了模型检测的工作原理和应用流程;其次,介绍了基于模型检测的硬件木马检测技术的研究进展;最后,指出了当前该技术所面临的瓶颈,并讨论了潜在的研究方向。 展开更多

关键词 硬件木马 模型检测 模型构建 属性声明

下载PDF 职称材料

一种基于约束求解的Verilog语言静态分析方法 被引量：1

6

作者 黄赛杰 陈铭松 金乃咏 《计算机应用与软件》 CSCD 2015年第12期1-3,87,共4页

由于硬件描述语言Verilog中存在赋值语句的并发行为,对其验证一直是静态分析技术的一大挑战。针对Verilog程序的正确性问题,提出一种基于布尔约束求解的Verilog验证方法。通过分析Verilog语义特点,采用分步编码的方式对Verilog并发赋值... 由于硬件描述语言Verilog中存在赋值语句的并发行为,对其验证一直是静态分析技术的一大挑战。针对Verilog程序的正确性问题,提出一种基于布尔约束求解的Verilog验证方法。通过分析Verilog语义特点,采用分步编码的方式对Verilog并发赋值语句进行处理。实验结果显示,该方法能有效地检测Verilog程序中设计的缺陷,并给出错误发生时程序的状态。 展开更多

关键词 硬件设计 静态分析 模型检验 符号执行 约束求解

下载PDF 职称材料

脉冲功率放大链相位噪声检定系统中的信号处理系统

7

作者 张长革 唐申生 《宇航计测技术》 CSCD 北大核心 1996年第1期9-16,共8页

详细介绍了在脉冲功率放大链相位噪声检定系统中的信号处理系统的设计方案、工作原理及功能。本系统是整个检定系统的重要组成部分，在整个系统中担负着将放大器链的噪声信号进行转换、采集、存储、传输、处理和显示等任务，它由硬件电... 详细介绍了在脉冲功率放大链相位噪声检定系统中的信号处理系统的设计方案、工作原理及功能。本系统是整个检定系统的重要组成部分，在整个系统中担负着将放大器链的噪声信号进行转换、采集、存储、传输、处理和显示等任务，它由硬件电路和系统软件两大部分组成。硬件电路主要由采集单元、存储单元、控制单元、时钟单元及计算机接口等几个模块组成，其功能是：将模拟信号转换为数字信号，暂存采集到的信号数据，并将数据送人计算机内存中。电路中设有自检功能，从而增加了调试的透明度，也提高了系统工作的可靠性。系统软件由控制软件和分析处理软件组成，前者负责控制硬件进行自检，以及谐调各部件间按一定的时序工作；后者负责将噪声数据进行各种数据处理（时域、频域分析），并根据检定系统的测试指标要求（噪底、起伏特性等）给出正确的测量结果。软件设计采用多层菜单式动态显示技术，图文并茂，显示醒目直观。整个检定系统经多次联试试验后，结果表明，本信号处理系统方案设计合理，工作稳定可靠，功能强，维护方便。将本系统的设计思想应用于雷达发射机稳定性测试系统中也取得了很好的效果。 展开更多

关键词 数据传输 脉冲功率放大链 相位噪声

下载PDF 职称材料

ANSI-C语言的有界模型检测及其在硬件验证中的应用

8

作者 潘志鹤 李祥 《电脑与信息技术》 2005年第4期19-21,40,共4页

对软件进行检测和验证是保证软件可靠性的关键步骤,一个近来在国外颇受重视的验证标准C程序的工具——标准C语言的有界模型检测工具CBMC,它可以对用Verilog语言建好的硬件电路进行检测。文章介绍了CBMC的基本功能、基本用法和它在Window... 对软件进行检测和验证是保证软件可靠性的关键步骤,一个近来在国外颇受重视的验证标准C程序的工具——标准C语言的有界模型检测工具CBMC,它可以对用Verilog语言建好的硬件电路进行检测。文章介绍了CBMC的基本功能、基本用法和它在Windows平台下的安装使用;然后用CBMC检测了一个Verilog语言设计的电路,结果表明,使用CBMC进行硬件验证是一个值得重视的方向。 展开更多

关键词 CBMC VERILOG CYGWIN 硬件验证 有界模型检测

下载PDF 职称材料

微机保护装置的容错功能

9

作者 董津敏 李成军 王淑其 《冶金动力》 2007年第6期75-76,79,共3页

微机保护装置内部元件损坏时,从可靠性的角度希望任一元件损坏时保护不应误动,同时能自动检测出故障元件并报警,以便得到及时处理,防止设备或线路故障时由于元件损坏未被及时处理造成保护拒动。

关键词 硬件故障 自动检测 容错设计和多重化

下载PDF 职称材料

汇编级软硬结合的控制流检测方法 被引量：3

10

作者 吴艳霞 顾国昌 +2 位作者 戴葵 刘海波 沈晶 《计算机研究与发展》 EI CSCD 北大核心 2010年第8期1481-1489,共9页

控制流检测技术是防止由于瞬时故障造成程序错误运行的有效手段之一,在ARGOS卫星上测试过的基于汇编语言的软件控制流检测算法CFCSS具有较高的错误检测能力和较低的冗余指令开销,实用性较强,但此算法存在检测混淆和检测出错现象.为此,... 控制流检测技术是防止由于瞬时故障造成程序错误运行的有效手段之一,在ARGOS卫星上测试过的基于汇编语言的软件控制流检测算法CFCSS具有较高的错误检测能力和较低的冗余指令开销,实用性较强,但此算法存在检测混淆和检测出错现象.为此,首先阐述了CFCSS算法中存在的检测混淆和检测出错现象;接下来根据汇编语言特点,修改了基础基本块的选择方法和多调整签名值赋值语句的插入位置,提出了改进的ICFCSS控制流检测算法;为了在ICFCSS算法基础上进一步提高错误检测能力、降低故障延迟时间和冗余指令开销,提出了软硬结合的ICFCSSHS控制流检测方法,此方法在编译程序时只增加了和签名有关的信息,在程序运行时通过译码阶段判指令类型来触发相应的硬件完成控制流检测.实验表明,此方法的冗余代码空间开销比CFCSS算法减少了21.5%,平均未检测出错误率仅为1.5%,具有一定的使用价值. 展开更多

关键词 可靠性 硬件故障容错 控制流检测技术 控制流图 基本块

下载PDF 职称材料

改进的CFCSS控制流检测算法 被引量：1

11

作者 李静梅 吴艳霞 +1 位作者 沈晶 张健沛 《哈尔滨工程大学学报》 EI CAS CSCD 北大核心 2011年第6期814-819,共6页

针对软件控制流检测算法(CFCSS)存在的检测混淆和检测出错问题,分析了造成可靠性差的根本原因,并根据汇编语言结构特点,通过修改基础基本块的选择方法和多调整签名值赋值语句的插入位置,提出了改进的软件控制流检测算法(ICFCSS),弥补了... 针对软件控制流检测算法(CFCSS)存在的检测混淆和检测出错问题,分析了造成可靠性差的根本原因,并根据汇编语言结构特点,通过修改基础基本块的选择方法和多调整签名值赋值语句的插入位置,提出了改进的软件控制流检测算法(ICFCSS),弥补了硬件故障容错性能上的不足,改进算法克服了出错问题的发生.实验表明:此检测算法的平均未检测出错误率仅为2.9%. 展开更多

关键词 可靠性 硬件故障容错 控制流检测技术 基本块

下载PDF 职称材料

一种基于就地模块的硬件自诊断系统设计

12

作者 朱长银 刘东超 +2 位作者 夏勇军 黎恒烜 蔡敏 《电气技术》 2020年第7期35-41,共7页

针对新一代智慧变电站二次系统对就地设备硬件可靠性的要求和硬件全面自检的方法以及内存测试难点,本文提出一种新的检测方法,以提高内存纠错能力,及时获取硬件设备运行状态。新设计的就地模块具备异常主动预警功能,自动识别二次设备隐... 针对新一代智慧变电站二次系统对就地设备硬件可靠性的要求和硬件全面自检的方法以及内存测试难点,本文提出一种新的检测方法,以提高内存纠错能力,及时获取硬件设备运行状态。新设计的就地模块具备异常主动预警功能,自动识别二次设备隐性故障,通过通信协议的扩展,把硬件自检信息上送到硬件自检监控系统,实现了变电站二次设备状态的全面感知,为状态检修提供了技术支撑,提高了设备的运行可靠性。该检测方法已在工程中得到实际应用。 展开更多

关键词 智能变电站 就地模块 硬件自检 监控系统

下载PDF 职称材料

基于签名的控制流错误检测算法检测能力的验证模型

13

作者 吴艳霞 顾国昌 +2 位作者 戴葵 沈晶 刘海波 《宇航学报》 EI CAS CSCD 北大核心 2010年第12期2776-2783,共8页

目前主要采用实验测试的方法对基于签名的控制流错误检测算法进行评价,但由于控制流错误模型的不确定性,而导致测试结果存在一定的偏差,本文尝试采用模型验证的方法评价控制流检测算法的错误检测能力。本文首先简述了基于签名的控制流... 目前主要采用实验测试的方法对基于签名的控制流错误检测算法进行评价,但由于控制流错误模型的不确定性,而导致测试结果存在一定的偏差,本文尝试采用模型验证的方法评价控制流检测算法的错误检测能力。本文首先简述了基于签名的控制流错误检测算法的基本原理,其次,提出了控制流错误跳转关系表示方法和指出了传统的控制流错误检测能力分析方法中未考虑的影响检测能力的因素,接下来,结合这些因素提出了基于签名的控制流错误检测能力验证模型,最后给出实例,通过验证模型分析了目前典型的基于签名的控制流错误检测能力。 展开更多

关键词 可靠性 软件实现的硬件故障容错 控制流错误检测算法 验证模型

下载PDF 职称材料