形式验证关键系统的硬件组件

文摘

硬件组件,如内存和运算单元,是每一个计算机控制系统的重要组成部分,例如,无人驾驶飞行器(无人机)。这些硬件组件的基本要求是,他们必须像期望的;否则,整个系统建立在他们可能会失败。确定组件是否充分表现,所需的组件的行为往往是在布尔代数中指定。布尔代数是一种最广泛使用的数学工具来分析硬件组件代表在门使用布尔函数的水平上。为了确保可靠的计算机控制系统设计、仿真和测试方法通常用于检测故障;然而,这样的方法不保证没有错误。关键系统的设计,如无人机、基于仿真的技术通常与数学工具和技术来增强证明强大的属性,例如,没有缺点,在早期阶段的系统设计。在本文中,我们定义一个轻量级的数学框架基于计算机的定理验证公鸡来描述和推理关于布尔代数和硬件组件(逻辑电路)模型布尔函数。为了演示框架的有效性,我们(1)定义和证明的正确性对偶原理机械地使用计算机工具和所有布尔代数的基本定理,(2)正式定义了代数操作(循序渐进的过程证明功能对等的功能)用于简化布尔函数,和(3)验证功能正确性和可靠性两个硬件组件的属性。使用机械定理验证的主要优势是,所有的定义和证明的正确性可以检查机械使用的类型检查器和证明检查器设施证明助理公鸡。

1。介绍

硬件、软件和通信网络完全使系统操作无人机(uav)等网络空间。无人机操作在一个不确定的潜在危险,遥远,和动态环境中非常重要,但挑战是可靠的,健壮的,安全的。这些飞行汽车目前正在用于关键任务(1),面向工业(2,物联网(物联网)3)应用程序,等等。以满足无人机关键任务的高标准的安全性和可靠性1)或物联网(2,3)应用程序,这样的无人机系统必须使用严格和正式的技术研究和分析。故障或非真正的使用软件和硬件系统的飞行器可以导致人类损失(4,5)和战略损失(6,7]。无人机可以操纵和控制人类环境远程攻击者使用攻击等传感器输入欺骗攻击(8]。军用无人机已经和正在攻击者获得网络力量的最喜欢的目标(9),最近领导走向无人机战争(10]。

设计容错和安全的飞行器,常规设计和测试方法必须增强更健壮和可靠的工具和技术称为正式的方法(11]。正式的方法已成功地用于验证无人机之间的冲突避免(12),保证无人机民用空域内(13,设计有弹性的无人机系统(14]。无人机的安全性和可靠性取决于单个组件的安全性和可靠性,必须确保其正确性在设计阶段。除了无人机,本文给出的正式框架也同样适用于其他任何计算机系统,如传感器网络(15- - - - - -17)和硬件组件,比如闪存,这种系统的18]。在本文中,我们解决的正式规范和验证硬件(逻辑)组件,比如内存单位和蛇,使用布尔代数在逻辑门级设计。这使得我们的正式模型非常重要的关键领域的系统设计一般,特别是在无人机。

布尔代数(19)的分析和合成的基本逻辑工具(模型)的逻辑电路。这个布尔代数和逻辑电路之间的联系建立了克劳德·香农(20.]。尽管不同的计算机工具(21- - - - - -25)和数学技术(26,27)可用于控制逻辑电路模拟作为布尔函数,它必须确保这些工具和技术不改变这些电路的目的解释(行为)。验证数字电路的行为(模仿布尔函数)分析是对称的原始行为后,布尔函数之前数学操作必须被证明是功能对称函数后操纵。这个属性的数字电路通常被称为功能对等(28]。操纵的常见例子是数学操作(29日),卡诺图(26),列表法(27)用于布尔函数。

布尔代数是一种使用最广泛的数学技术模型和分析逻辑电路。在电子设计流程,最初的电路设计经常被描述在系统级高级语言(例如,MATLAB和C)和翻译过户逻辑(RTL)表示在一个描述语言(例如,Verilog和VHDL)使用高级合成(硬件编译器)的工具。的RTL表示电路转换为使用逻辑门电路级表示(通常作为布尔函数)合成工具,这是最后的产生电路的物理布局。门电路级表示描述为布尔函数中常用的技术和框架(30.- - - - - -33),在课堂上简单的逻辑电路的设计与分析(29日]。

1.1。研究挑战

布尔函数或逻辑电路描述为布尔函数通常是通过操纵容易出错的某月方法使用布尔代数的基本定理和假设。我们所知,代数和数学操作过程都没有被正式定义在一个交互式定理验证,因此不能被机械地检查其正确性。确实没有保证的对偶原理,进行数学处理是正确的,或逻辑电路(称为布尔函数)优化大小、效率和成本效益使用K-map [26)或制表(24)方法行为对称的。

1.2。解决方案概述

为了正式原因关于布尔代数和验证数字的正确性组件门级描述为布尔函数,我们定义了一个正式的模型布尔代数定理验证使用的微积分建设公鸡。布尔代数的正式模型定义允许一个定义并证明所有的基本定理以及二元性的原则。我们扩展我们的正式模型布尔代数的表示组合电路。评估我们的正式模型的有效性,证明公鸡的设施是用来进行正确性证明门电路级组合电路对布尔代数和理性。(部分等众多优势2)的计算机辅助验证使用交互式定理验证如下:(a)中定义的所有正式的定义和证明可以电脑,和(b)的正确性证明可以由计算机自动检查34]。

布尔函数的正式方法检查正确性和数字电路描述在图1。正式的数字电路的模型验证和感兴趣的性质定理被送入一个ITP引擎(公鸡系统,在我们的例子中)和一个正式的证明(模型)电路的特性进行交互。证明工程师指导工具通过提供证据命令,使之成为证据的一部分脚本如果接受的工具。的正确性证明脚本自动检查使用该工具。公鸡的形式验证使用提出正式的模型展示部分6证明等价性、可逆性和类型安全属性的多个电路。在这种背景下,本文的主要贡献如下:(我)一个基于计算机的数学模型来描述和推理关于布尔函数定义和门电路级组合电路。是小说,因为它使我们的正式模型,除了布尔代数基本定理,定义了对偶原理和逻辑电路计算机定理验证。此外,模型和允许一个机械化的基本定理的数学操作过程,可以检查正确使用电脑。(2)的正式证明对偶原理和布尔代数基本定理。在文献中,没有计算机的证据有效性的对偶原理和基本定理证明中列出最受欢迎的书等(29日,36]。(3)正式的证明多组合电路的等价性和可逆性。减少传播延迟多位数加法器,有预见性的携带发电机电路添加使用一个循序渐进的过程;然而,没有证据证明它不改变加法器的目的的行为。我们正式证明有预见性的发电机保护的功能行为加法器。(iv)公鸡定理验证了我们的模型的性能评估。

剩下的纸是组织如下。在下一节中,交互式定理证明的意义是突出显示。公鸡定理验证工具和布尔代数中引入部分3。基于布尔代数的正式模型中定义定理验证部分4。布尔代数和逻辑电路是理性的部分5和6,分别。我们的正式模型评估和结果讨论部分7。一个关键审查相关工作的部分8和部分9总结了纸。所有的公鸡源代码可以从GitHub库https://www.github.com/wilstef/booleanalgebra。

2。为什么互动证明助理?

一个常见的方法检查两个电路(表示为布尔函数)对许多功能对等是广泛的模拟输入和比较结果。基于仿真的测试是在行业最受欢迎的方法,因为它易于使用;然而,它不能确保系统中没有错误。此外,模拟系统与大型输入不计算上可行;例如,模拟256位内存芯片需要测试2^256年可能的输入。另一种方法来检查数字电路的正确性,特别是或等价性检查,使用正式的方法是基于计算机的数学工具和技术。正式的工具和技术的优势,严谨和计算机辅助,可以用来正式证明属性的所有可能的输入。此外,正式的方法基于技术可以用来确保系统中没有错误。

依照最近的一项调查(35),大多数的形式验证方法和工具是基于模型检测和自动定理验证由著名的状态和内存限制爆炸(37,38)问题。形式验证使用模型检测在工业[很受欢迎39,40和研究社会研究领域的40- - - - - -42];然而,本文的重点是在交互式定理证明(ITP) (43- - - - - -45)的方法。ITP-based正式的方法,指导计算机证据证明工程师助理,如公鸡和伊莎贝尔/假日[45),通过提供证据在证明过程中命令。ITP-based正式验证,也称为半自动的方法,结合了手动和自动的实力证明。这种半自动ITP的方法需要专业知识和技能;然而,它已在过去使用了调查大案例研究(46]。在自动定理证明中,很难得到见解当证据的尝试失败了,而ITP迫使设计师注意小细节。这导致更精确地理解系统研究。

传统的数学证明纸和笔(非正式)容易出错并且难以管理大型和复杂的证明。计算机辅助验证,另一方面,是一种有效,高效,严谨的正式规范和验证的方法。自动化定理验证被广泛使用在工业自动创建证明不需要人类努力;然而,他们所面临的问题,如状态爆炸(37,38]。种定理验证,另一方面,需要人力支持进行数学证明。通过提供证据证明工程师指导定理验证命令和交互式地创建证明。公鸡就是这样一个流行的互动证明助理考虑定义我们的正式框架。

数学证明种定理进行验证更有组织,因为以下原因:(i)在机械化定理验证(如公鸡),证明可分为模块(简化证明处理);(2)前题/定理已经证明可以很容易地调用和应用;(3)的公鸡语言策略(Ltac)可以用来结合复杂的证明命令(战术)在一个单一的策略;(iv)的证明可以通过电脑阅读和检查使用证明检查器;(v)一个新的证据可以打开在一个现有的未完成的证明;(vi)大证明脚本可以检查未经证实的前题是通过使用一个单一的公鸡命令;等等。总的说来,证明等证明助理公鸡更比手写的证明方法和组织的正确性证明脚本可以检查电脑。

3所示。背景

数学证明布尔代数的性质使用计算机和验证数字电路的正确性,必须定义在逻辑代数的机械(计算机可读)证明公鸡等助理。这样一个正式的定义中给出了布尔代数部分4。了解正式定义,布尔代数和公鸡使用正式的工具这一节介绍。深入了解电路的建模使用布尔代数和公鸡定理验证,读者推荐参考书籍(29日,47),分别。

3.1。公鸡的助理

公鸡(44)是一个交互式定理验证微积分的基础上归纳建设。它是可用的语言规范被称为加莉娜,类型检查器和证明检查器。语言,类型检查器和证明检查器是用于创建正式的规范下的系统测试,检查规格类型错误,分别创建和检查正式证明。理解形式化和使用交互式定理证明系统验证,我们定义了一个简单的系统的数字使用证明助理公鸡然后给推理系统。

我们开始正式定义数字电感作为数据类型Nat使用公鸡关键字归纳有两个构造函数生成的元素类型Nat(1 - 3行,清单1)。的定义Nat在这个清单的州O(0)Nat如果n是Nat,Succ n也Nat。第一个构造函数没有参数,只是说明O属于类型Nat。第二个构造函数Succ有一个参数的类型Nat即年代紧随其后的是一个Nat(Nat左边的箭头)也是一个Nat(Nat右边的箭头)。这个词Succ (Succ (Succ O))例如,一个Nat对应于3号。

操作数,我们定义了一个递归函数添加(5 - 9行)添加的值类型Nat。函数返回第二个参数米如果第一个参数O;否则,它将返回Succ(添加n′m)。一个引理Add_N_O,在那里添加n O = n适用于任何的价值n声明,证明清单1(11到18门行)。这个引理的证明进行了运用归纳建设的第一个参数n。实施证明的时候,公鸡工具被给予证明的命令称为交互式地引导战术(-)。许多其他的属性添加功能,如交换和关联属性,也可以表示和证明机械使用公鸡证明助理。

3.2。布尔代数

根据乔治·布尔(19),布尔代数是一个代数结构与一组值,“+”和“两个二进制操作。“在亨廷顿的值集和证据48)假设。后来,香农(20.]介绍了两价的版本的代数表示的属性转换电路。两值的代数,价值观包括元素1和0和两个二进制操作结合(逻辑)和分离(逻辑或)。此外,有一个一元运算称为否定或补充(不)。

使用布尔函数在两值的布尔代数,逻辑电路可以模仿。这个函数模型的逻辑电路和门代表产品操作和非门代表补充操作。当逻辑电路用函数表示,他们可以操纵和合理的使用工具和技术开发的布尔代数。例如,代数操作步骤使用假设可以写下来并使用公鸡工具(参见检查5)。

香农的布尔代数的两值的版本中定义公鸡定理验证清单中描述2(47]。布尔代数的第一部分,一组两个元素,与公鸡类型表示bool使用公鸡定义的关键字归纳见清单2(第1行)。这两个值的布尔代数的定义真正的和假。

布尔代数的第二部分是定义两个二进制操作在布尔类型的值bool。第一个操作的规则+(总和)被定义为函数总和在清单3 - 7行2。使用模式匹配的函数总和两个值的类型bool并返回值假如果两个输入值假;否则,它将返回真正的。第二个二元运算的规则。(产品)中定义的函数刺激(第四行,清单2)。这个函数返回真正的只有两个输入值真正的;否则,它将返回假。一元运算。补布尔集合的元素中定义的函数不在清单15 - 19行。给定一个值作为输入,不返回其他值。在这些操作中,操作和最高+最低优先级。

4所示。形式化逻辑电路和布尔代数

节中定义的布尔代数3专门针对组合电路的扩展和定义。首先,一组符号清单3扩展与象征(清单4)xor具有相同优先级的操作。(操作刺激)。正式定义的逻辑操作总和,刺激,xor,和不模型的基本逻辑组件或,XOR,分别而不是盖茨。后正式造型这些基本逻辑组件,它们组合在一起,形成组合电路。组合电路的定义是一个布尔值(函数)(清单列表5)。

列表”F¹x y: F²x y:零”代表了一种组合电路有两个输入x和y和两个输出定义为两个布尔函数。评估每个布尔函数列表中的一个布尔值,一个评估函数eval_cir定义在清单6。函数将一个组合电路作为列表的布尔函数,并返回一个布尔值(清单列表7)。

布尔代数是形式化的最终要求六亨廷顿假设[29日,48),证明所有的基本定理。亨廷顿的正式定义的假设都包含在公鸡脚本可以从我们的仓库。此外,正式的定义操作总和,刺激,不足以推断亨廷顿假设和基本定理除了对偶原理(部分中讨论吗5)。对偶原理的推导需要操作的布尔表达式,原则不能被定义在当前设置。现有的定义表达式不区分变量和值(身份元素),这是在二元性的基本要求操作。要做到这一点,一个类型经验值布尔表达式的定义如清单所示8。前三个构造函数(2 - 4行)对应于三个逻辑操作总和,刺激,不,分别。最后构造函数将一个布尔值,变量或者表达式。

所有的假设和基本定理,除了关闭,退化,共识,有两个部分:一部分是手术+ (总和),另一个是。(刺激)。根据对偶原理假设的一部分/定理可以来自其他运营商和元素互换身份。二元性原则是重要的在证明定理使用假设和代数操作。特别是,当一部分的定理的证明,其他的可以很容易地进行了二元性的原则。推导了这种方法被认为是有效的根据对偶原理在文献和教科书29日];然而,没有正式的提供了证据。我们这个桥梁,提供一个正式的对偶原理的证明。

一个函数changeident(清单9)交换身份定义元素的布尔表达式。它被一个表达式和互换身份的元素真正的和假和树叶运营商和变量不变。关键字Fixpoint用于定义递归函数。交换的另一个操作操作符被定义为一个递归函数changeop在清单10。同样地,函数changeop得到一个表达式和互换的操作符总和和刺激。

5。布尔代数的正式证明

节的正式定义4使一个正式的原因对布尔代数和组合电路描述为布尔函数。本节包含对偶原理的证明和展示了示例,我们正式设置可以自动化非正式代数操作用于对数字逻辑设计的教科书。此外,所有的基本定理和假设已定义和证明公鸡,公鸡给脚本可以从我们的仓库。

5.1。对偶原理

对偶原理指出表达式来源于假设通过交换运算符(+)和身份元素(0,1)是有效的。布尔表达式定义交换操作之后,所述对偶原理现在可以作为一个引理如清单所示11。引理的州,如果定理成立的一部分(两个任意表达式相等),那么它意味着的第二部分定理可以通过改变身份元素和运营商。检查证明可以使用对偶性,给出的第一部分交换属性( ),的第二部分交换属性( )被证实(清单12通过应用对偶性。

5.2。机械化的代数操作

简化的逻辑电路,文字和条款的数量必须减少电路的描述。代数操作方法是最受欢迎的方法之一在教科书29日为了这个目的。这种操作是非正式的,因此容易出错。正式结构包括前面定义的假设和基本定理的应用,如非正式的代数操作,使用公鸡证明助理。机械化在证明代数操作助理的主要优势是,证明脚本可以机械地读,检查和维护。

证明我们的正式框架适合机械检查代数操作的正确性,证明的定理absorption_sum已经列在清单吗13。这个证明是由应用(使用重写策略)的假设和定理。这个脚本是一个机械化的非正式证据证明定理6 (a)的教科书(29日]。

第二部分的证明abroption_prod相同的定理被认为持有由对偶原理。这一原则已被证明在上面的部分。每一个假设或基本定理有两部分,一个是双重的。这是有趣的表明,鉴于循序渐进的一个定理的证明,证明其他的(双)部分可以由应用对偶原理/定理应用于相应的步骤。这个定理的证明abroption_prod(对偶定理absorption_sum)已经被列入清单14。假设/定理应用于5 - 9行互相证明都是双重的。

6。描述和验证组合电路

无人机无人机飞行就像电脑在Linux或Windows操作系统,飞行控制器,主板,内存单元,和成千上万的行可编程代码。正式的方法,特别是我们的框架,可以应用于无人机以不同的方式分析。正如前面提到的,它是一个复杂的计算机系统,因此正式技术可以用来验证操作系统、协议、逻辑组件,内存单元,和任何算法用于无人机系统。算术和逻辑组件(例如,加法器和比较器)和内存(如ROM)是典型的计算机的主要部件(包括无人机),我们运用我们的正式框架分析内存和一个加法器电路。在本节中,功能对等和可逆性属性的组合电路被证明。此外,它还证明,所有的描述电路的基本属性叫类型安全可靠性。

6.1。记忆电路的等价性验证

首先,一个328罗记忆体晶片与内容值得信赖的设计、存储ASCII数据第一16个位置,指定在一个真值表如表所示1(条目第一16输入和显示在表定义。其余的条目不在乎条件)。的字母E代表位输入(条线)和O- o显示内存的八位输出(数据行)。表指定了输入-输出关系:第一16位输入选择任何位置;芯片返回ASCII代码信的内容值得信赖的设计。

首先设计内存芯片,每个内存芯片的输出定义为五个输入变量的布尔函数大肠为每个输出函数是由结合(通过运营商+)小项,在相应的输出列的值是1。这将导致八布尔函数 ,中表示sum-of-minterms(29日,36)的形式,如清单所示15(产品和和每个函数给出了源代码)。328 ROM芯片(清单定义16)七布尔函数列表清单15。这是一个58组合电路有5个输入和八个输出。芯片的5个输入位标识之一内存位置和输出线给8位字符的ASCII代码存储在这个位置。

设计一个简单、高效的内存芯片的所有八个功能(输出- - - - - -)简化使用K-map方法的功能- - - - - -见清单17。简化布尔函数有更少的文字和条款(清单17(公鸡定义)相比原始功能- - - - - -在源代码),会产生一种简单而有效的电路布局(见部分7对一个电路布局的例子)。在清单的简化布尔函数17占内存芯片的输出组合在一起,形成列表简化组合电路如清单所示18。

在清单的正式模型组合电路16进行了简化后,著名的简化方法K-map电路清单吗18;然而,它并不保证电路在功能上是等同的。换句话说,没有数学保证K-map简化流程没有改变原电路的行为。最初的设计由真值表规范作为“黄金”或“参考”的设计。证明了简化电路的功能相当于“黄金”设计,各个功能都被证明是等价的定理1(此定理对应一组八个前题equiv_OO′0-equiv_OO′7在公鸡脚本)。功能对等的两个电路定理2中检查。电路定理的状态之前简化等效电路后简化,保证简化过程保存功能。

定理1(布尔函数的等价):对于任何函数 ,在哪里我= 0,1,2, ,7日,布尔函数简化操作和功能等价关系 , 。

使用案例分析证明:这个定理证明使用布尔变量。在我们列出的公鸡这个定理的证明是GitHub库https://github.com/wilstef/booleanalgebra。

定理2(电路的功能对等):清单中描述的组合电路C16和它的简化版本_年代在清单18在功能上是等价的。更正式,CC_年代,其中C_年代=(C)和是K-map简化操作。

证明:这个定理被证明是通过应用(重写)八个前题已经证明定理1。在我们列出的公鸡这个定理的证明是GitHub库https://github.com/wilstef/booleanalgebra。

6.2。进行了组合电路的等价性验证

算法组件,如加法器、不可或缺的一部分的算术和逻辑单元(处理器)的任何基于微处理器的系统。快速设计节能和组件,设计描述(通常在一个描述语言)通常是转换和数学操作。然而,它必须确保这些转换并不改变这些组件的预期行为。这种担保是更加必要的组件设计时用于关键系统、无人机等。证明我们的正式定义也可以用来证明两个组合电路的功能对等,我们描述的两个版本的二进制编码的十进制(BCD)加法器(图2)的公鸡。这样的BCD加法器设计和受欢迎的教科书中描述29日在这个问题上)数字逻辑设计;然而,没有一个正式的等价证明已经提供。

BCD加法器添加了两个小数位数和BCD数量总和的结果。4比特BCD加法器可以设计使用两个4比特二进制并行方案如图2(右)。传统的4比特二进制加法器,由四个完整的蛇,是一种串行加法器,添加了两个4比特以串行方式二进制数。每一个全加器都有两位(被加数和加数比特)和一个输入移位,给了一笔一点一点和一个输出。给出了一个完整的加法器的输出带作为输入进行到下一个的输入进行第(右)大部分加法器将逻辑0。的输出进行最后一个加法器的输出带4比特二进制加法器。

最初的携带,作为第一个加法器的输入,传播过去的加法器,结果在一个传播延迟。为了避免这种传播延迟的二进制加法器,有预见性的携带发生器(29日是用来预测的输入。先行的携带生成器是一个小规模集成电路添加前4比特加法器,让它快。转换避免传播延迟;然而,没有正式的证明加法器的功能性质被保留。在本节中,我们正式证明的两个实现BCD加法器(图2),一个有和其他没有预见性发生器电路,在功能上是等价的。

首先,我们设计一个BCD加法器使用二进制蛇没有预见性携带发电机。4比特并行加法器FA4bit被定义为一个函数在清单吗19。它应用全加器函数足总的4比特对两个4比特数和输入(输入数字-模拟、数字-模拟和e),并返回一个5位元组。第一位元组是最后的携带和接下来的四位和碎片。二进制加法器FA4bit是用来实现BCD加法器见清单吗20.。的let-expressions线2、3和4计算的结果第一二进制加法器,输出,分别和第二二进制加法器。两个二进制蛇之间的附加电路需要生成输出携带BCD的加法器和调整的和第一个二进制加法器BCD和。

生成BCD加法器与先行的发电机,我们必须首先设计二进制并行加法器与先行的发电机。4比特的正式定义二进制并行加法器被列入清单21。的定义C2- - - - - -C5(1 - 7行)计算的四个输出带有四个完整的蛇在二进制加法器。与加法器FA4bit,每个内部输出独立于前全部加法器的输出进行。这使得每一个全加器同时生成输出和无需等待携带从之前的加法器的输出。的定义S1- - - - - -S4计算四位预见性的带位C2- - - - - -C5和初始携带e。最后,4比特二进制并行加法器与先行的携带发电机被定义为一个函数FA4bitLA(17日行)。就像在BCDadder的两个实例二进制并行加法器FA4bitLA有额外的电路对输出进行组合在一起形成一个BCD加法器。4比特BCD加法器的正式定义预见性携带发电机已经显示在清单22。建议读者参考书籍(29日,36]为进一步细节BCD加法器和有预见性的发电机。

正式的定义BCDadderLA和BCDadder模型4比特BCD蛇没有预见性携带,分别。他们的功能对等在定理check_equiv_BCD_adder在清单23。这个定理指出,两条产生相同的输出等于输入。这个定理证明使用案例分析输入变量。正式的证明定理check_equiv_BCD_adder表明我们的框架可以有效地用于组合电路的等价性检验记忆回路。

6.3。可逆性的财产证明

证明我们的正式框架也可以用来验证属性除了等价,我们正式验证可逆性的一个简单的电路描述。为此,我们证明了电路电路定义在清单24是可逆的。这个定理reversible_circuit州,为所有不同(2比特)输入,输出是不同的。此外,这个定理也指出,输入和输出的数量都是一样的。在这个定理,列表[w;x]和[y;z]在清单24 4号线模型的输入。

7所示。评估和讨论

自动化工具,如模型检查,有时由于内存或状态爆炸问题[38),永远也别回来。公鸡的性能评估工具运行在我们的框架中,我们测试了公鸡证明检查器检查证明脚本功能对等的布尔函数与多个布尔变量。结果在图3表明,公鸡证明检查器需要大约12秒检查证明脚本功能对等与功能45变量输入情况下(超过十亿)。

公鸡的正式模型提供了一个正式的定义和推理的基础对布尔函数和逻辑电路使用的微积分建筑背后的公鸡定理验证。下面列出我们的正式模型的主要优势:(我)布尔函数的定义或模型逻辑电路可以自动检查(类型错误)的公鸡类型检查器。(2)中使用的数学操作的正确性分析布尔函数可以自动检查。(3)属性,如对偶原理,功能对等,和可逆性,布尔代数,逻辑电路(模型)可以证明交互地使用公鸡定理验证。(iv)所有的证明可以进行机械检查公鸡证明检查器使用电脑。

形式验证使用证明助理非常繁琐,需要专业知识;然而,许多研究人员最近使用证明助手建立正式的语言和框架对硬件验证(49- - - - - -53]。证明助理包括手动和自动定理验证和更强大和富有表现力的50]。我们的框架允许定义布尔函数和组合电路在自然风格类似于在许多流行的教材(29日,36)和大部分的证据可以轻易通过应用公鸡的进行自毁策略。

8。相关工作

最常见的可靠的数字电路设计方法是使用模拟器测试设计等风投(54和伊卡洛斯55)通过提供所有可能的输入。虽然基于仿真的验证可以显示存在错误,不能保证他们的缺席56]。基于形式验证方法(57),如模型检查(32,58,59),定理证明(49,52,53,60,61年在文献中,更受欢迎。读者建议请参考[62年)模拟的详细比较和正式基于方法的方法。基于模型检测工具可用于两个函数的等价性检验(模型);然而,他们是受欢迎的制约状态爆炸(37,38)问题。有一个身体的研究在文学作品的形式验证软件系统(63年- - - - - -65年];然而,文献综述的硬件验证和仿真工具检查布尔函数等价包含在这一节中。

8.1。正式的硬件验证

如前所述,工具和技术的基础上正式的方法可以用来证明没有故障硬件组件。奥斯曼et al。51)定义了一个正式的框架在假日的高阶逻辑定理验证证明财产组合电路的可靠性。而他们的工作是专门针对检查可靠性的主要属性,我们的框架促进了功能对等检查逻辑演算归纳建筑强大和富有表现力的公鸡定理验证(50]。卡巴特et al。66年)提倡使用自动化定理验证组合逻辑的合成。他们用解调的重写逻辑简化规范电路结构。在工业自动化定理验证更受欢迎;然而,他们不是一样强大和富有表现力的助手的证据。助理证据,另一方面,结合自动和手动定理验证的好处和目前研究和鼓励对硬件验证(50,51]。工作(50)强调了交互式定理验证的有效性和权力公鸡在硬件验证,进一步支持我们的框架嵌入公鸡逻辑电路验证。而他们的工作是更关注于合成基于公鸡的代码提取功能,我们的工作嵌入布尔代数作为电路的门电路级描述语言的描述。我们的门电路级描述语言描述组合电路提供了一个通用的框架。此外,我们构建超理论表达和证明对偶原理并执行布尔代数基本定理的证明。

梅瑞迪斯et al。67年)定义可执行语义Verilog通过嵌入在工具莫德(68年与重写逻辑作为底层逻辑)。灵感来自[67年),原来受et al。49,69年]介绍了一个正式的语言,VeriFormal:数学基础的硬件描述语言。VeriFormal是描述语言的正式副本Verilog深深植根于伊莎贝尔/假日定理验证。VeriFormal和正式的可用模拟器使用后证明功能对等的多个逻辑电路(70年]。Braibant et al。71年)定义Fe-Si深深嵌入简化版本的功能硬件描述语言Bluespec定理验证公鸡。建筑proof-carrying代码背后的概念,爱et al。72年)实现一个框架通过形式化synthesizable子集的Verilog助理公鸡的证据。一些研究人员(52,60)有针对性的可编程逻辑控制器通过形式化的语义中使用的编程语言控制器,而其他指定电路作为向量的操作。卖弄风情的女人(53)是一个高级的规范电路使用深嵌入;然而,这种级别的抽象是通过先进的类型,如参数类型,使得电路的正式定义短但增加了复杂性。所有这些研究贡献添加形式验证在更高层次的抽象,而我们的工作分析电路门级。上级正式的验证,如过户的层面上,也同样重要,但本文的重点是针对电路门级。此外,除了对数字电路推理,我们的公鸡框架可以有效地用于推断布尔代数。

8.2。布尔等价性检查工具

有许多其他工具开发了专门为布尔函数的操作。Ronjom et al。23)开发了一个在线数据库的布尔函数。他们的工具可以用来检查布尔函数的不同属性和不同表示形式之间进行转换。WolframAlpha的计算引擎[21)翻译逻辑函数作为输入一个真值表和不同的最小形式。此外,该工具生成一个维恩图和逻辑电路的输入函数。WolframAlpha引擎被包括为布尔代数计算器TutorVista的公司。另一个工具(22使用卡诺图地图)是减少开发的布尔函数(26]。可以输入的函数作为一个符号序列或真值表(六个变量)。

在最近的工具是32×8 [25已建立逻辑电路简化。它接受一个函数(8个变量)的真值表并返回一个卡诺图,布尔函数(如产品或产品的金额之和)、真值表、逻辑电路的输入。精益和Marxel开发了一种解算器,QMSolver [24),基于Quine-McCluskey算法简化布尔函数。求解得到的小项指数(用空格分开),并返回一个简化的函数。所有这些工具操纵电路门级;然而,没有一个正式的基础,因此电路设计的操作不能被证明是正确的。

9。结论

当(模型)逻辑电路转换或数学操作(通常为优化目的),必须保证转换并不改变所需的电路的行为。在本文中,一个正式的框架来描述和验证布尔函数和逻辑电路门级定义的公鸡定理验证。为了演示框架的重要性,布尔代数的基本定理和对偶原理证明。此外,多个基本硬件组件被描述在正式的符号和功能对等和可逆性性能验证。我们正式的发展可以用来描述其他关键系统中使用的逻辑组件,可以正式证明正确使用公鸡定理验证工具。

作为一个未来的工作,我们计划建立一个翻译自动转换电路设计在自然风格中布尔函数的形式化(公鸡)布尔代数。此外,完成正式的电子设计流程,我们打算建立一个逻辑综合工具翻译从正式过户的水平表示电路(如在VeriFormal, [49,69年])门电路级表示布尔函数。

缩写

罗:	只读存储器
RTL:	过户逻辑
国际旅游业伙伴关系:	交互式定理证明
假日:	高阶逻辑
ASCII码:	美国信息交换标准代码
高密度脂蛋白:	硬件描述语言
BCD:	二-十进制计数法
史:	K-map简化操作
:	函数的等价关系。

数据可用性

公鸡脚本数据用于支持这项研究的结果已经沉积在GitHub库https://github.com/wilstef/booleanalgebra。

的利益冲突

作者宣称没有利益冲突有关这篇文章的出版。

确认

作者想扩展他们的真诚感谢在沙特国王大学科研院长以来,沙特阿拉伯,部分通过研究小组资助这个研究项目。以序列- 214。

引用

1. f . Al-Turjman”无人机定位在关键任务应用程序的新方法,”交易新兴电信技术,2019年p . e3603。视图:出版商的网站|谷歌学术搜索
2. f . Al-Turjman和美国Alturjman 5 g / IoT-enabled多媒体交割的无人机在面向工业应用中,“多媒体工具和应用程序卷。78年,22页,2018页。视图:谷歌学术搜索
3. f . Al-Turjman m . Abujubbeh a . Malekloo l .芥茉,“无人机评估软件定义的物联网网络:概述,“计算机通信卷,150年,第536 - 519页,2020年。视图:出版商的网站|谷歌学术搜索
4. 诉Arumugham,疫苗安全:学习从波音737 MAX灾害CERN欧洲核研究组织,2019年瑞士,日内瓦。
5. p•罗宾逊波音737 Max软件外包给美元9-an-hour工程师,《卫报》,布隆伯格,伦敦,英国,2019年。
6. d·p·谢泼德,j·a·巴蒂,t·e·汉弗莱斯”无人机攻击:欺骗攻击民用无人机演示,“全球定位系统(GPS)的世界,23卷,不。8日,30-33,2012页。视图:谷歌学术搜索
7. s . m . Giray”无人机劫持解剖与信号欺骗,”学报2013年第六届国际会议在空间技术最新进展(拉斯特)IEEE,页795 - 800年,伊斯坦布尔,土耳其,2013年6月。视图:谷歌学术搜索
8. r·d·戴维森h . Wu Jellinek,诉辛格(manmohan Singh)和t . Ristenpart“控制无人机传感器输入欺骗攻击,”学报第十届USENIX攻击技术研讨会(即使16)2016年8月美国奥斯汀,TX。视图:谷歌学术搜索
9. k·哈特曼和k·贾尔斯,“无人机开发:新域网络的力量,”学报》2016年第八届国际会议上网络冲突(CyCon)IEEE,页205 - 221年,塔林,爱沙尼亚,2016年5月- 6月。视图:谷歌学术搜索
10. 美国中心,无人机的也门战争回顾萨那战略研究中心,萨那,也门,2019年6月。
11. j . m .翼”,说明符形式方法的介绍,“电脑,23卷,8-22,1990页。视图:谷歌学术搜索
12. e·阿德勒和j·b·Jeannin”形式验证无人机的防撞转弯的动作”张仁航空学报》2019年论坛美国德克萨斯州达拉斯,p . 2845, 2019年6月。视图:出版商的网站|谷歌学术搜索
13. m·韦伯斯特,m . Fisher:卡梅伦,m .跳”正式自主无人机系统的认证方法,”学报》国际会议计算机安全、可靠性和安全性施普林格,页228 - 242年,那不勒斯,意大利,2011年9月。视图:谷歌学术搜索
14. a . m . Madni m·w·西弗斯j . Humann e . Ordoukhanian b·波姆和产品,所的的美国Lucero”正式在弹性系统设计方法:应用multi-UAV复杂系统控制”学科融合系统工程研究施普林格,页407 - 418年,柏林,德国,2018年。视图:谷歌学术搜索
15. s .乔·m·伊荣格,w . Ryu和j·金,“电动图像压缩在无线传感器网络中,“移动和无线,42卷,只愿降价,2013页。视图:谷歌学术搜索
16. s . k .乔·m·伊荣格,w . Ryu和j·金,“权力有效的无线多媒体传感器网络、集群”国际期刊的分布式传感器网络ID 148595条,卷。10日,2014年。视图:出版商的网站|谷歌学术搜索
17. m·a·h·Chowdhury伊·m·k·h·金,“安全、可生存的组通信在MANET使用CRTDH基于虚拟子网模型”学报2008年IEEE亚太服务计算会议IEEE,页638 - 643年,宜兰,台湾,2008年12月。视图:谷歌学术搜索
18. h . Redwan m·a·h·Chowdhury伊m和k·h·金”的调查信息检索索引方案基于闪存的无线传感器网络,”学报2009会议信息科学、技术和应用程序ACM,页14号至21号、科威特、2009年3月。视图:谷歌学术搜索
19. g .布尔调查法的思想美国,多佛,IL 1854。
20. c·e·香农,”一个象征性的继电器和开关电路的分析,“电气工程57卷,第723 - 713页,1938年。视图:谷歌学术搜索
21. WolframAlpha计算知识引擎”,2018年2月,https://www.wolframalpha.com/。视图:谷歌学术搜索
22. “在线布尔函数的最小化,”2018年2月,https://www.tma.main.jp/logic/index_en.html/。视图:谷歌学术搜索
23. r·森德a·默罕默德·拉尔斯,d .““布尔函数的在线数据库,”2018年2月,http://www.ii.uib.no/ mohamedaa / odbf / index . html。视图:谷歌学术搜索
24. r .精益Kryle, m . Marxel“QMSolver”, 2018年2月,http://agila.upm.edu.ph/ kmmolina /质量管理体系/ index . html。视图:谷歌学术搜索
25. “逻辑电路简化(SOP和POS)”, 2018年2月,http://www.32x8.com/。视图:谷歌学术搜索
26. m·卡诺图”的映射方法合成组合逻辑电路,”事务的美国电气工程师学会,我部分:通信和电子产品卷,72年,第599 - 593页,1953年。视图:谷歌学术搜索
27. d . s . Kushwaha t . k . Jain, a . k . Misra”优化Quine-Mccluskey方法最小化的布尔表达式,”英格尔学报2008年第四国际会议上自主和自治系统IEEE,页165 - 168年,安克雷奇,正义与发展党,美国,2008年9月。视图:谷歌学术搜索
28. a . Kuehlmann诉派鲁锡、f . Krohm和m . k . Ganai“健壮的布尔推理进行等价性检查验证和功能属性,“IEEE计算机辅助设计的集成电路和系统21卷,第1394 - 1377页,2002年。视图:谷歌学术搜索
29. m . m .马诺数字逻辑设计和计算机培生教育印度,新德里,印度,2017。
30. o . Lhotak“程序分析使用二元决策图,”麦吉尔大学蒙特利尔,加拿大,2006年,麦吉尔大学论文提交。视图:谷歌学术搜索
31. Carbin m·d·j·惠利Avots和m . s . Lam”使用datalog和二元决策图程序分析,”亚洲研讨会程序编程语言和系统施普林格,页97 - 118年,筑波,日本,2005年11月。视图:谷歌学术搜索
32. j·r·伯奇·e·m·克拉克,k·l·麦克米兰d l .莳萝和l . j .黄”符号模型检测:10^20.指出,“信息和Computation1,卷992,不。98年,页142 - 170。视图:谷歌学术搜索
33. b . l .合成“ABC:连续合成和系统验证,发布70930年”2007。视图:谷歌学术搜索
34. a . Mulhern c·费舍尔,b . Liblit”的工具支持工程证明,“电子票据在理论计算机科学卷,174年,第86 - 75页,2007年。视图:谷歌学术搜索
35. t·格林,d . Lettnin和m .大”在正式调查验证技术高安全性的systems-on-chip时,“电子产品,7卷,不。6,81年,页2018。视图:出版商的网站|谷歌学术搜索
36. m . m .马诺和m . d . Ciletti数字设计:介绍了Verilog HDL, Verilog硬件描述语言(VHDL),系统美国,皮尔森,波士顿,MA, 2018。
37. a . Valmari“状态爆炸的问题,”佩特里网专题我:基本模型施普林格,柏林,德国,1998年。视图:谷歌学术搜索
38. e·m·克拉克w . Klieber m . Novaček和p . Zuliani“模型检测和状态爆炸问题,”实用工具软件验证页中,施普林格,2012年。视图:谷歌学术搜索
39. j·l·雅工业用正式的方法:正式的验证新泽西州霍博肯市约翰·威利& Sons,美国,2013年。
40. m . Kwiatkowska g·诺曼·d·帕克,“PRISM 4.0:验证概率实时系统,”《国际会议上计算机辅助验证施普林格,页585 - 591年,雪鸟,UT,美国,2011年7月。视图:谷歌学术搜索
41. j·b·阿尔梅达m·j·弗雷德j·s·平托和s . m . de Sousa”正式的工具和技术方法,概述”严格的软件开发施普林格,页15 - 44,伦敦,英国,2011年。视图:谷歌学术搜索
42. d . Kroening和m . Tautschnig CBMC-C有界模型检验器,”Proceedongs国际会议工具和算法的建设和分析系统施普林格,页389 - 391年,伦敦,英国,2014年10月。视图:谷歌学术搜索
43. y Bertot和p . Casteran交互式定理证明和程序开发:公鸡艺术品:电感结构的微积分施普林格科学与商业媒体,2013年。
44. b .彭s Boutin c .玉米et al .,”公鸡证明助理参考手册:6.1版本,”1997年,博士学位论文,法国。视图:谷歌学术搜索
45. t . Nipkow、l·c·保尔森和m .文策尔伊莎贝尔/假日:证明助理高阶逻辑卷。2283年,施普林格科学与商业媒体,柏林,德国,2002年。
46. w·阿伦特b . Beckert r . Hahnle et al .,集成自动化和交互式定理证明Kluwer学术出版商,荷兰阿姆斯特丹,1998年。
47. 公元前皮尔斯,c . Casinghino m . Gaboardi et al .,“软件基础,”2010年,http://www.cis.upenn.edu/bcpierce/sf/current/index.html。视图:谷歌学术搜索
48. e . v .亨廷顿“新组独立假设的逻辑代数与怀特海德和罗素的数学原理,“事务的美国数学学会,35卷,第304 - 274页,1933年。视图:谷歌学术搜索
49. 原来受k、t . Alwen和美国大卫,“VeriFormal:一个可执行的正式模型的硬件描述语言。网络安全的系统方法,”学报》2017年第2 SGCSC新加坡网络安全研发会议2017年2月,页19-36、新加坡、。视图:谷歌学术搜索
50. Coupet-Grimal和l . Jakubiec“公鸡和硬件验证:一个案例研究”《国际会议在高阶逻辑定理证明施普林格,页125 - 139年,图尔库,芬兰,1996年8月。视图:谷歌学术搜索
51. o·哈桑,j·帕特尔,s . Tahar”正式使用定理证明了组合电路的可靠性分析,“应用逻辑杂志卷。9日,41-60,2011页。视图:谷歌学术搜索
52. s . o . Biha”,正式的语义公鸡的PLC程序”学报2011年IEEE第35年度会议(COMPSAC)计算机软件和应用程序IEEE,页118 - 127年,慕尼黑,德国,2011年7月。视图:谷歌学术搜索
53. t . Braibant“卖弄风情:公鸡库验证硬件,”学报》国际会议认证程序和证明施普林格,页330 - 345年,垦丁,台湾,2011年12月。视图:谷歌学术搜索
54. “风投在线模拟器”,2015年12月,http://www.edaplayground.com/x/FfR。视图:谷歌学术搜索
55. “伊卡洛斯Verilog”, 2016年12月,http://www.icarus.com/eda/verilog/。视图:谷歌学术搜索
56. g . j .速度和j .他“正式的推理与verilog HDL,”《车间在正式技术硬件和与硬件相关的系统1998年6月,Marstrand,瑞典,。视图:谷歌学术搜索
57. 郑胜耀黄和k·t·t·程正式的等价性检查和设计调试》12卷,施普林格科学与商业媒体,柏林,德国,2012年。
58. e·m·克拉克,o . Grumberg和d·贝利模型检查,麻省理工学院出版社,伦敦,英国,1999年。
59. a . Biere a . Cimatti e·m·克拉克o . Strichman y朱,“有界模型检验,”电脑的发展58卷,第148 - 117页,2003年。视图:谷歌学术搜索
60. l . Xiaoa m·李·m·顾,j .太阳“PLC程序的建模和验证基于交互式定理证明工具,公鸡,”《计算机科学和信息技术国际会议(ICCSIT)2012年12月,香港,中国,。视图:谷歌学术搜索
61. l . Arditi和s Antipolis”形式验证微处理器:公鸡的第一个实验证明助理,“技术。代表,大学德Nice-Sophia Antipolis,不错,法国,1996年,技术报告,研究报告,i3。视图:谷歌学术搜索
62. w·k·林,硬件设计验证:模拟和正式基于方法的方法(Prentice Hall现代半导体设计系列),普伦蒂斯霍尔PTR上台北,美国,2005年。
63. w·汗·m·Kamran a·艾哈迈德·f·a·汗和a . Derhab”正式android安全使用定理证明方法,分析基于语言”IEEE访问7卷,第16560 - 16550页,2019年。视图:出版商的网站|谷歌学术搜索
64. w·汗h . Ullah a Ahmad et al .,“CrashSafe:一个正式的模型证明碰撞安全性的android应用程序,”以人为中心的计算和信息科学,8卷,不。1,p。27日,2018。视图:出版商的网站|谷歌学术搜索
65. m . Bugliesi s Calzavara、r . Focardi和w·汗”CookiExt:修补浏览器会话劫持攻击,”《计算机安全,23卷,不。4、509 - 537年,2015页。视图:出版商的网站|谷歌学术搜索
66. w·c·卡巴特和a . s . Wojcik”自动合成使用定理证明的技术组合逻辑,”IEEE计算机,C-34卷,不。7,610 - 632年,1985页。视图:出版商的网站|谷歌学术搜索
67. p .梅雷迪思,m . Katelman j . Meseguer, g . Roşu“正式的执行语义的Verilog,”学报》2010年第八届IEEE / ACM国际会议上正式合作设计方法和模型(MEMOCODE)IEEE,页179 - 188年,2010年7月,法国格勒诺布尔。视图:谷歌学术搜索
68. m . Clavel f·杜兰,j·亨德里克斯,卢卡斯,j . Meseguer p . Olveczky,“莫德正式工具环境,”代数的国际会议上,给出在计算机科学施普林格,页173 - 178年,卑尔根,挪威,2007年8月。视图:谷歌学术搜索
69. w·汗·d·Sanan、z侯和l .杨”嵌入硬件描述语言在伊莎贝尔/假日”为嵌入式系统设计自动化,23卷,不。3 - 4、123 - 151年,2019页。视图:出版商的网站|谷歌学术搜索
70. w·汗,a . Basim诺曼,k .阿卜杜勒·莫伊和s . Ahtisham”正式验证数字电路使用模拟器和数学基础,”应用力学和材料卷,892年,第142 - 134页,2019年。视图:出版商的网站|谷歌学术搜索
71. t . Braibant和a . Chlipala”形式验证硬件的合成、”《国际会议上计算机辅助验证施普林格,页213 - 228年,圣彼得堡,俄罗斯,2013年7月。视图:谷歌学术搜索
72. e .爱,y, y Makris,“Proof-carrying硬件知识产权:可信模块获取的途径,”IEEE取证和安全信息,7卷,不。1、批准,2012页。视图:出版商的网站|谷歌学术搜索

版权

版权©2020原来受汗等。这是一个开放分布式下文章知识共享归属许可,它允许无限制的使用、分配和复制在任何媒介,提供最初的工作是正确引用。