IEEE 802.11 OFDM调制解调器误差分析与验证：形式化方法和定理证明

理论计算机科学电子笔记242（2009）3-30www.elsevier.com/locate/entcsIEEE标准的误差分析与验证802.11 OFDM调制解调器使用定理证明1Abu Nasser Mohammed Abdullaha，3，Behzad Akbarpourb，4和Sofi'eneTaharc，5a美国马萨诸塞州切姆斯福德Cadence设计系统公司2b英国剑桥大学计算机实验室c加拿大魁北克省蒙特利尔市康考迪亚大学电气和计算机工程系摘要IEEE 802.11是一种广泛使用的技术，它为目前正在发生的许多数字无线通信革命提供了动力。它在物理层使用OFDM（正交频分复用）技术，这是一种有效的多径处理方法，适用于相对慢时变的信道，并且对窄带干扰具有鲁棒性。在本文中，我们正式指定和验证的实现IEEE 802.11标准的物理层为基础的OFDM调制解调器使用HOL（高阶逻辑）定理证明。HOL的多功能表达能力帮助我们在所有抽象级别上对原始设计进行建模，从浮点模型到定点设计，然后在FPGA技术中进行合成和实现。 我们已经能够找到一个错误，在一个块的设计，是负责用于调制，其实现偏离IEEE标准规范中提供的星座。本文还推导出了新的表达式的舍入误差积累在理想的实到浮点和定点过渡在算法层面上，并进行了正式的误差分析的OFDM调制解调器在HOL。保留字：形式验证，定理证明，误差分析，正交频分复用，无线通信。1 这项工作的两页摘要初步版本已作为“短论文”发表CAD 2006 [A. N. M.阿卜杜拉湾Akbarpour和S. 塔哈尔：使用HOL的OFDM调制解调器设计的形式化分析和验证，在：计算机辅助设计形式化方法IEEE国际会议论文集，IEEE计算机协会出版社，圣何塞，加利福尼亚州，美国，2006年11月，pp. 189-190]。[2]这项工作是作者在康考迪亚大学时完成的3 电子邮件地址：nasser@cadence.com4 电子邮件地址：ba265@cl.cam.ac.uk5电子邮件地址：tahar@ece.concordia.ca1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.06.0204A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）31介绍IEEE 802.11 [19]指的是关于局域网和城域网无线网络的IEEE标准族。IEEE中规定的服务和协议802.11映射到较低的两层，即七层OSI（开放系统互连）网络参考模型的数据链路层（DLL）和物理层（PHY）DLL由逻辑链路控制（LLC）和媒体访问控制（MAC ）两个子层组成。IEEE 802.11的PHY 基于正交频分复用（OFDM）[28]，这是一种使用多个载波来减轻多径效应的调制技术通常，通信和其他电子设计（如OFDM调制解调器）的分析和功能验证都是通过仿真来完成的但是，仿真不足以检查设计的所有可能输入，即使是中等大小的设计，因此使设计部分验证。形式验证是一种技术，它已被证明是模拟的补充，以实现严格的验证。在已建立的形式验证技术中，定理证明对于在更高抽象层次上验证复杂系统特别强大。在本文中，我们使用Akbar-pour [2]提出的通用分层方法对DSP（数字信号处理）设计进行正式建模和验证，以使用HOL定理证明器[9]验证IEEE802.11a物理层OFDM调制解调器[25验证在所有抽象级别执行，从实数、浮点数和定点数系统到寄存器传输级（RTL）硬件实现。为了验证，设计规范和实现都在形式逻辑中建模，然后证明数学定理的正确性。我们能够在调制块中找到一个错误，其中实现中使用的星座不符合IEEE标准规范。此外，我们推导出新的表达式的舍入误差积累，而从一个数域转换到其他和进行正式的错误分析的OFDM调制解调器在HOL。本文的其余部分组织如下。第2节回顾了相关的工作。第3节描述了待验证的OFDM调制解调器实现的详细信息以及用于验证的方法。第4节描述了OFDM系统的RTL块的验证。第5节描述了OFDM调制解调器的错误分析及其形式化使用HOL。最后一节总结了本文，并为未来的工作方向提供了提示。2相关工作在IEEE 802.11a物理层的设计和实现方面有许多研究工作。虽然没有做任何关于使用定理证明来验证OFDM或部分系统的重要工作，但我们仍然提到了OFDM系统的一些重要实现在[8]中，使用TMS320C6201处理器开发了一种编码OFDM系统，用于赛车和汽车环境中的遥测 在[30]中，作者开发了一种线-A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）35较少的LAN（局域网）系统，采用TI C6x平台。在[6]中实现了针对软件定义无线电优化的OFDM调制解调器的实时软件实现。代表离散系统块的软件模块被创建，并在此实现中根据需要按顺序调用。该软件可重构系统是在基于定点处理器的TMS320C6201评估模块上开发的。这项工作还探索了定点运算的算术精度和速度的不同组合。在本文中，我们考虑[25]的设计与[8]不同，正在验证的设计未针对遥测应用进行优化，并且未使用编码OFDM技术。[30]中的OFDM设计针对特定平台，并广泛使用平台提供的高级过程语言子例程;而[25]使用Xilinx库来实现一些高性能计算块。[6]中描述的工作也设计了OFDM系统，但它是专门针对软件定义无线电进行优化的。[8]和[6]都使用相同的处理器平台，但[25]具有更通用的设计，可以适应各种应用程序。存在一对夫妇的工作有关的应用程序的IEEE 802.11的形式化方法。两者都使用概率模型检测，但没有一个从硬件的角度分析系统的设计或实现。第一个[23]使用概率时间自动机对IEEE 802.11标准的双向握手机制进行了建模，其中使用了固定的网络拓扑结构，这是一种正式的描述机制，可以表示不确定性和概率性选择。然后从概率时间自动机模型中获得有限状态马尔可夫决策过程，然后使用PRISM [22]（一种概率模型检查工具）对其进行验证。在第二项工作[29]中，确定了将概率模型检查的应用范围扩大到802.11MAC（媒体访问控制）的方法，提出了一种通过抽象技术优化的广义概率时间自动机在这里，还使用PRISM验证了结果。与这些相关的工作相比，我们专注于一个完全不同的方向。虽然第一项工作在IEEE 802.11网络设置上执行模型检查第二项工作也使用模型检查来验证MAC协议，它驻留在物理层之上。在本文中，我们只集中在物理层和它的硬件实现。此外，我们使用基于HOL的定理证明技术，而不是模型检查上述两项工作完全与协议验证相关，并解决与OSI模型上层相关的验证问题，因此与软件验证相关性更大。此外，在我们在这里提出的工作中，我们提出了物理层实现的正式错误分析，据我们所知，这是解决这个问题的第一项工作。以前关于形式验证中的错误分析的工作是由Harrison [11]完成的，他使用HOL Light定理证明器验证了诸如指数函数的迭代点算法与其抽象数学对应物。作为主要定理，他证明了临界点指数函数有一个正确的超临界行为，在没有超临界行为的情况下，6A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3结果被限制在一定量。 他还报告了一个错误的手证明主要涉及忘记一些特殊情况下的分析。这种误差分析与针对DSP算法执行的分析类型非常相似。然而，主要的区别是使用统计方法和DSP算法的均方误差分析，这在哈里森使用的数学函数的误差分析中没有涉及。在这种方法中，误差量被视为独立的随机变量，均匀分布在一个特定的区间，这取决于算术类型和舍入模式。然后进行误差分析，推导出方差和均方误差的表达式。在另一项工作中，Huhn等人 [17]提出了一种混合形式验证方法，该方法结合了不同的最新技术，以指导从算法开始到寄存器传输级的不精确工作算术电路的完整设计流程。以离散余弦变换算法为例说明了该方法的有效性。特别是，作者在[17]中已经展示了在算法水平上使用Mathematica或Maple等计算机代数系统来推理实数并确定数值运算结果的某些误差范围。数字滤波器和FFT算法实现过程中的算术误差长期以来一直使用传统数学和仿真进行分析。例如，Tran-Thong和Liu [31]详细分析了使用定点算法的各种FFT算法版本中的舍入误差。Jackson [20]分析了定点数字滤波器的级联和并行实现的圆形噪声。Liu和Kaneko [24，21]提出了一种通用方法，用于数字滤波器和FFT算法的误差分析问题，使用浮点运算，并计算了由于舍入累加和输入量化而导致的输出误差。误差分析传统上是通过比较这样的理论结果与实验模拟。与[17]相比，Akbarpour [2]开发了一个使用HOL定理证明器进行DSP系统误差分析的框架。他展示了上述错误分析，特别是Liu和Kaneko [24，21]的错误分析，可以机械地验证。 他将这种分析扩展到了浮点和定点数字滤波器以及FFT算法。Akbarpour在本文中，我们打算以与[2]相同的方式研究误差分析我们的工作证明了[2]中的方法是可扩展的。除此之外，与对FFT算法的单个结构进行误差分析的[31，21]相比，我们推导出了IFFT-FFT组合中舍入误差累积的新表达式，该组合是基为4和64点的计算，作为整个OFDM结构的计算模型在理想的情况下，调制解调器的输出信号应该等于输入信号.但是，我们表明，在实际的实现中，由于有限的精度效应，情况并非如此。A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）37数据输出信道模型解调BPSKQPSK16-QAM64-QAMFFT随机数据生成器保 护 间隔插入并串IFFT串并调制BPSKQPSK16-QAM64-QAM保 护 间隔移除并串3IEEE 802.11 OFDM调制解调器及其验证方法IEEE 802.11物理层OFDM调制解调器的标准框图实现如图1所示。第一个模块是随机数据生成器，这里显示的只是为了完成目的。下一个块是正交幅度调制块（QAM）。对于我们的具体实现，使用64-QAM。 下一个块是串行到并行（S/P）块，其也可以在框图的接收器侧中下一个块是IFFT块，OFDM最重要的块之一该设计使用来自Xilinx Coregen Library的64点复杂IFFT核心[34]。OFDM发射机串并OFDM接收机Fig. 1. [25]第二十五话IFFT使用与接收器中的FFT块相同的IP核。 并行到串行（P/S）电路构成下一个块。发送器行中的下一个块是保护间隔插入电路。在接收器侧，第一块是保护间隔移除块。我们跳到QAM解映射器（DQAM）块，因为我们之前讨论了其他块。从这个块中，数据再次被序列化，并且输出被顺序地接收。所选择的OFDM调制解调器实现的设计流程从解调点建模开始。对于这种OFDM调制解调器设计，用于解调点建模的环境是Cadence的信号处理工作系统（SPW）[5]。设计流程的第二步是定点建模和仿真。用于此目的的环境是硬件设计系统（HDS），它是来自SPW的一组库最后利用HDS软件自动生成整个系统的VHDL代码但是，对于FFT/IFFT等模块，没有HDS对应模块，这些模块是从Xilinx Coregen库导入的。一些VHDL代码是手工编写的[25]。在VHDL代码生成后，这些模块在Synopsys设计编译器中综合，以FPGA为硬件实现。最后8A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3使用“布局布线”技术将合成电路映射到FPGA中，房（转换）浅埋REAL（HOL）FP误差分析浅FPFP估值FP实际价值（转换）嵌入（HOL）FXP错误分析（HOL）FP转FXP错误分析FXP浅FXP估值FXP真实价值（综合）RTL嵌入浅（HOL）逻辑蕴涵RTL（HOL）（综合）嵌入（HOL）逻辑蕴涵网表浅网表嵌入（HOL）图二. DSP规范和验证方法[2]本文中使用的形式化规范、验证和误差分析采用了Akbarpour [2]提出的DSP验证框架。图2所示的交换图演示了该框架的基本思想。该方法提出，DSP算法的理想实规范和相应的浮点（FP）和定点（FXP）表示以及RTL（寄存器传输级）和门级实现可以基于使用HOL定理证明环境的语言浅嵌入[4对于从实数到FP和FXP电平的过渡，使用误差分析，其中将浮点和定点输出的实际值与理想实数规格的相应输出进行比较。RTL的验证使用HOL中众所周知的经典分层证明方法进行。验证可以按照类似的方式扩展到HOL中的门级网表，或使用图中所示的其他商业验证工具。本文不涉及这一分析4正式功能验证在本节中，我们将描述根据第3节中描述的方法使用HOL对OFDM的RTL块进行验证。整个设计被分割成不同的块，然后使用HOL建模。由此产生的模型反过来又针对理想规范进行设置，并交互式地使用HOL工具来证明它的正确性。在下面的章节中，我们将详细描述QAM、DQAM、串行到并行（S/P）和并行到串行（P/S）块的验证。 对于下面描述的块，对应的抽象模型、HOL模型和A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）39提供部分证明策略以全面解释验证。更多详情请参见[1]。4.1QAM和DQAM块的验证QAM（正交幅度调制）是通过改变两个载波的幅度来传送数据的调制方案。这两个波通常是正弦波，相位相差90Ω，因此称为正交波运营商-因此该计划的名称它是一种多进制信令技术其中M个可能信号s1（t），s2（t），...，sM（t）可以在持续时间T的每个信令间隔期间发送。与M进制PSK（相移键控）不同，在M进制PSK中，调制信号的同相和正交分量以包络被约束为保持恒定的方式相互关联，QAM去除了这种约束。M-aryQAM的一般形式由以下传输信号定义：si（t）=.2E0a我不是cos（2πfct）+.2E0b我不是sin（2πfc t）0≤t≤T（1）其中E0是具有最低幅度的信号的能量，并且ai和bi是根据相关消息点的位置选择的一对独立整数[14]。根据IEEE 802.11a标准，OFDM子载波将根据所请求的速率应将编码和交织的二进制串行输入数据划分为比特组，并转换为代表BPSK、QPSK、16-QAM或64-QAM星座点的复数。 转换将根据图3所示的格雷编码星座映射来执行，其中输入比特b0是流中最早的。输出值d是通过将得到的I+jQ（其中I和Q分别是星座图的x轴和y轴）值乘以归一化因子KMOD而形成的d=（I+jQ）KMOD（2）归一化因子KMOD取决于基础调制模式，如表1所示。归一化因子的目的是为所有映射实现相同的平均功率在实际实现中，可以使用归一化因子的近似值，只要设备符合[19]中IEEE 802.11a标准草案中规定的调制精度。可能会出现一个问题，即OFDM应该使用什么QAM星座？答案在于，虽然更高的星座图每个符号提供更多的比特，但如果平均能量保持不变，这些点必须更靠近在一起，因此更容易受到噪声和其他损坏的影响;这导致更高的误码率，因此高阶QAM可以提供比低阶QAM更不可靠的更多数据。10A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3调制KMODBPSK1QPSK√1216-QAM√11016-QAM√142表1KMOD归一化对于已验证的OFDM设计，在Cadence SPW中模拟了浮点和定点模型后，选择了64-QAM星座用于QAM映射的电路使用组合逻辑来实现。它将输入整数数据映射到星座点，如图3所示。Q000 100001 100011 100010 100110 100111 100101 100100 1007000 101001 101011 101010 101110 101111 101101 101100 1015000 111001 111011 111010 1113110 111111 111101 111100 111000 110001 110011 110010 110110 110111 110101 110100 1101-7-5-3-11357我000 010001 010011 010010 010-1110 010111 010101 010100 010000 011001 011011 011010 011-3110 011111 011101 011100 011000 001001 001011 001010 001-5110 001111 001101 001100 001000 000001 000011 000010 000-7110 000111 000101 000100 000图三. 64-QAM星座比特编码VHDL建模使用查找表方法[25]完成。QAM块仅采用3位作为输入，并映射到16位的输出，如图4a所示。QAM块被实例化两次，并且被设计为生成实部和虚部作为两个分离的输出。它们中的每一个都被格式化为16位2的补码，针对从每个块的六个输入中选择的3位输入。这些输出在图4b中由out qam r和out qam i示出。电路由输入连续地馈送，因此输出qam r和输出qam i作为连续流生成。输出被处理成48个符号的组，这些符号分别存储在两个独立的双端口RAM中，称为由于这种类型的RAM是使用Xilinx Coregen库自动生成的[35]，因此没有进一步讨论。A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）311∧►∀输出qam i输出qam_r(a) （b）QAM块见图4。 QAM块及其实例化QAM的建模是在HOL中使用不同的现有理论进行的。IF-THEN-ELSE构造用于嵌入VHDL代码，如以下代码所示definputqam_out.qam_imp（输入qam_out）=（WORDLEN输入= 3）（如果input=WORD[F; F; F]，则qam_out=WORD[T;F;F;T;F;F; F; F; F;F;F;F;F;F;F]其他（如果input=WORD[F; F; T]，则qam_out=WORD[T;F;T;T;F;F; F;F;F; F;F;F;F;F]其他（如果input=WORD[F; T; F]，则qam_out=WORD[T;T;T;T;F;F; F; F; F;F;F;F;F;F;F]其他（如果input=WORD[F; T; T]，则qam_out=WORD[T;T;F;T;F;F; F; F; F;F;F;F;F;F;F]其他（如果input=WORD[T; F; F]，则qam_out=WORD[F;T;T;T;F;F; F; F; F;F;F;F;F;F;F]其他（如果input=WORD[T; F; T]，则qam_out=WORD[F;T;F;T;F;F; F; F; F;F;F;F;F;F;F]其他（如果input=WORD[T; T; F]，则qam_out=WORD[F;F;F;T;F;F; F; F; F;F;F;F;F;F;F]其他qam_out=WORD[F; F; T; T; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F]）））））上述模型是基于wordTheory[33]。利用该理论可以对VHDL的数据类型进行建模。VHDL类型的BIT可以使用T和F来建模，其中T和F分别代表1和0。位矢量可以使用WORD[...] 其中点可以用如上所述的由“;”分隔的T或F作为示例，位向量上述模型使用条件WORDLEN输入= 3来约束，因为输入总是3位，因此模型不需要针对n位进行一般化。这里，WORDLEN是一个函数，它接受任何WORD作为输入，并返回上面的模型现在可以根据需要多次使用（或者在HDL术语中可以实例化）来对任何复杂的设计进行建模。在我们的例子中，它被使用两次来将端口映射组件嵌入到HOL中，并命名为qam mod 2。我们坚持使用设计师使用的术语。下面是相应的HOL建模。3比特16位QAM6比特16位QAM16位QAM12A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3►∀∧∧∧∧►∀输入位（b0，b1，b2）I−out000-7001-5011-3010-11101111310151007输入位（b3、b4、b5）Q−输出000-7001-5011-3010-11101111310151007definput out_qam_r out_qam_i。qam_mod2_imp（输入输出_qam_r输出_qam_i）=（WORDLEN输入=6）（WORDLEN输出_qam_r=16）（WORDLENout_qam_i=16）qam_imp（WSEG3 0输入）out_qam_iqam_imp（WSEG3 3输入）out_qam_r该模型具有与之前的模型相同的特性，除了输入现在被约束为6位，因为qam mod 2的输入将总是6位。现在RTL模块的建模已经完成，是时候在HOL中对QAM的规范进行建模了。之后，我们将使用工具的逻辑技术来证明实现符合规范。 以来该设计基于IEEE 802.11a，我们使用标准[19]本身作为规范，以验证QAM实现。因此，对于进入qammod2块的每六个比特，这些比特被分成三个比特，每个比特用作qam块的输入然后，如上所述，qam mod2块输出包含调制输入的实部和虚部的两个向量。表2显示了I和Q的比特编码。表264−QAM编码表[9]从这两个表中可以注意到一点，即I和Q的位编码相似，这有助于我们仅对两者的一个规范进行建模，而单独建模它们是微不足道的。在HOL中建模表可以通过使用谓词来完成，如下所示：valTABLES_QAM=defI_OUT。TABLES_QAM（ I_OUT）=（I_OUT（F，F，F）=<$7）（I_OUT（T，F，F）=<$5）（I_OUT（T，T，F）=<$3）（I_OUT（F，T，F）=<$1）（I_OUT（F，T，T）=1）（I_OUT（T，T，T）=3）（I_OUT（T，F，T）=5）（I_OUT（F，F，T）=7）在上面的模型中，I OUT是一个三元组，它将接受三个位，类似于A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）313¬►∀►∀►∀表2的左栏。对于I OUT的每一个参数，一个唯一的数字将被映射为表中给定的数字，并且在涵盖了关于实现的所有相关细节和提取规范的非常可靠的方法之后，qam规范可以按照TABLES QAM编写如下：defb0 b1 b2 I_OUT。qam_spec（ b0 b1 b2 I_OUT）=不好意思。 TABLES_QAM OUT_OUT（I_OUT b0 b1 b2=OUT（b0，b1，b2））规范qam spec是镜像的，其实现qam imp在QAMMOD2IMP中被实例化，def输入I_OUT_R I_OUT_I。qam_mod2_spec（输入I_OUT_R I_OUT_I）=qam_spec（BIT 0输入）（BIT 1输入）（BIT 2输入）I_OUT_Iqam_spec（BIT 3输入）（BIT 4输入）（BIT 5输入）I_OUT_R有了以上说明，我们已经完成了所有基础工作，为QAM RTL模块的验证接下来，我们将详细讨论验证以及为支持RTL实现的正确性而采用的证明策略总的目标是证明对于所有输入和输出，正确性定理在一定的约束下成立，可以表述为：n输入输出。constraints=（实现规范）等价性可以用蕴涵来代替，这将通过只证明系统的特定行为来为正确性定理中的某些容许留出空间但是，在某些情况下，工程师（或任何进行证明工作的人）可以排除某些情况，因为这些情况肯定不会发生。就我们的情况而言，这是由于我们在定义中所施加的约束而产生的一种含义，因为我们确信，除了这些组合之外，不可能有其他组合发生。这个正义使我们只能陈述我们的目标，除了我们需要多一个定义，如下所示：defx.TCOMP_VAL x=&（BV（））* 2功率3 +（BV（BIT 2x））* 2功率2 +（BV（BIT 1x））* 2功率1 +（BV（BIT 0x））&&&这是一个基于HOL的boolLibrary的简单定义，将bool单词转换为它的实数等价物。函数TCOMP VAL接受一个bool字并返回一个实数。“BV也是一个函数，在numTheory理论中定义，它使用另一个函数将布尔值转换为自然数。► defB. BVb=（如果b，则SUC0，否则0）函数SUC接受一个自然数并返回连续的自然数。因此，SUC 0将返回1。并且，BIT xinput从x中定义的输入中选择特定的位位置。现在，我们可以说我们的目标是-对于所有输入∧14A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3⇒⇒以及输出和约束，QAM实现意味着QAM规范n输入输出。约束=规范（实现=规范）在HOL中正式化为输入qam_out。qam_imp（input qam_out）=qam_spec（ BIT 0输入）（BIT 1输入）（BIT 2输入）（λb0 b1 b2. TCOMP_VAL（WSEG4 12 qam_out））定义WSEG m k WORD从k到k+m-1选择WORD的一部分。函数qam spec接受三个参数并给出相应的输出。一个λ抽象用于将所选择的qam输出字转换为实数。现在，阶段是应用HOL的战术来证明目标。我们已经使用了现有的wordTheory和realTheory理论，建立了许多有用的定义和引理来证明上述目标，从而正式建立了RTL块的正确性我们证明了这个定理，并将其命名为qam imp spec correct。由于文本简洁，我们不包括整个证明过程在这里逐行。但是，证明这个定理只是确保我们关于QAM块，我们还没有证明qam mod 2 imp的实现。为此，我们设定了一个目标-输入out_qam_r out_qam_i。qam_mod2_imp（输入输出_qam_r输出_qam_i）=qam_mod2_spec输入（0 b1 b2. TCOMP_VAL（WSEG4 12 out_qam_r））（λb0b1b2. TCOMP_<$VAL（WSEG412out_qam_i））我们也使用与之前相同的库来证明这一目标。下面是HOL验证步骤。然后重复GEN_TACARW_TAC [qam_mod2_spec，qam_mod2_imp]THENARW_TAC[BIT_WSEG_input]THENARW_TAC [qam_imp_spec_correct]THENARW_TAC[BIT_WSEG_input]THENARW_TAC [qam_imp_spec_correct]我们只使用内置的战术。REPEAT GEN TAC策略删除了所有的单位性和存在性量化。接下来，ARW TAC是一种使用简单集[16]arith ss的重写策略RWTAC定义的策略。这种定义策略用于重写目标，具体说明和已证明的定理如上面的代码段。我们把这个最后证明的定理命名为qam imp spec correct。利用定理证明了qam mod 2 imp和qam impremsqam imp spec correct和qam mod2 imp spec correct，则可以得出结论，QAM被正式验证。实现符合标准中给出的规范。按照类似的方法，我们已经证明了DQAM块的正确性。细节可以在[1]中找到。4.2S/P和P/S模块在本节中，我们将验证串行到并行模块，后面写为S/P，这是整个OFDM系统不可或缺的一部分。与S/P相关的大多数基础知识与并行到串行模块的基础知识相似，稍后将进行讨论，因此本节将涵盖这两个模块的几乎所有重要方面∀∀A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）315∧¬串行到并行转换的概念是微不足道的。一个长的数据流被分成几个相等或近似相等长度的块，这些块可以同时被操作。从数学的角度来看，它是一个向量到矩阵的几个列的然而，S/P转换在OFDM中是非常重要的。在S/P中产生的块的长度决定了IFFT要使用的频谱系数的数量，这在选择要使用多少频率时是必不可少的通常，块长度是2的幂，这使得IFFT和FFT算法的计算效率最高。此外，在OFDM中，数据在大量紧密间隔的载波之间划分。由于整个带宽由单个数据源填充，因此必须以并行方式传输，以便每个载波上仅携带少量数据，并且通过降低每个载波的比特率，显著降低了符号间干扰的影响。S/P电路实现起来非常简单。它存在于系统的发送器和接收器中。在发射机侧，它被放置在QAM和IFFT块之间，并且在接收机侧，在保护去除和FFT块之间。手头的设计具有与它由一个移位寄存器和一个锁存器组成，两者都以与输入数据相同的速率计时。来自输入流的六位串行移位到寄存器中。然后，它们被锁存六个时钟周期。有两个控制信号使能和清除，以同步整个过程。HOL中S/P块的建模方式与我们在4.1节中看到的不同。建模并不是精确的一对一映射，因为这里涉及到一个VHDLPROCESS。事实上，PROCESS永远不会自行终止，只能使用WAIT语句和敏感性列表来控制它。执行完最后一条语句后，PROCESS将被挂起，只有在敏感性列表中的事件发生后才能恢复。由于非终止问题，最后一种行为在HOL中建模时存在困难。高阶逻辑是一种全函数逻辑，它不允许定义任何部分函数。但是，也有例外情况，促使我们以更简单的方式定义S/P的规格，而不诉诸复杂的定义。例如，下面是一个使用HOL表达能力的全非递归函数[16]：λx。如果（？n. P（FUNPOWg nx）），则FUNPOW g（@n. P（FUNPOW g n x）（！M. mn ==> P（FUNPOWg mx）））x否则ARB函数FUNPOW是一个尾递归函数，从理论上讲，它是一个定义函数迭代的算术理论。上面的函数对函数g的迭代进行了案例分析。无限个返回P保持的第一个值，无限个被映射到一个名为ARB的常量，该常量保存所有的任意值。 ARB是HOL中将部分函数转换为全函数的一种方法。但是，使用ARB只会使我们的模型复杂化，而不会带来任何额外的好处。的VHDLPROCESS不仅仅是一个简单的循环，而且我们没有要处理的无限情况，而是我们只有有限的语句集要无限地处理。这个讨论是为了证明为什么我们没有使用HOL的某些功能来建模我们的16A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3∧►∀►∀►∀这似乎有助于这样做。该模型的另一个方面是，由于我们独立于其他模块验证该模块，因此没有使用三个信号：清零、使能和清零话虽如此，我们在HOL中介绍S/P的实施情况如下defcnt out_parallel input.串行_并行_IMP（ cnt输出_并行输入）=移位寄存器（WORDLENout_parallel=6）（shift_reg输入=SHRN_bitcnt输入输出并行）显然，这是对相应的VHDL代码的简化，但只要稍加分析就能支持其正确的功能。 从代码中可以看出，变量cnt是一个自然数，其类型定义为num;outparallel是一个bool字，input是bool类型。该实现采用三个参数，其中cnt被定义为跟踪时间或位索引，这是信号计数的模型。第二个变量与其对应的VHDL变量同名，最后一个变量也是单输入。一个函数shiftreg被定义为shiftreg：bool→bool word，以模仿相同名称的VHDL信号。 变量不平行受约束到六个使用WORDLEN功能，因为设计规定如此。由于系统一次只接收一个输入，然后锁存所有输入，直到它填满整个移位寄存器，因此我们在HOL中编写另一个定义，以操纵进入系统的每个新位，并将空位置填充为零defNMw.SHRN_bit（NMw）=WCAT（ WORD（ REPLICATE（ WORDLEN w−（ N +1）） F），WORD[ M]）此定义使用WCAT，它连接两个列表，定义在word base理论[16]作为► def12楼。WCAT（WORD l1，WORDl2）=WORD（l1++l2）符号REPLICATE的递归定义是在理论丰富的listTheory中，它重复地复制指定的任何变量。定义为► def（注：REPLICATE 0 x=[]）卢塞恩x. REPLICATE（SUCn）x=x：：REPLICATE n x在这里，REPLICATE函数根据函数传递给它的当前值，用“F”填充移位寄存器的其余位置在完成了实现的建模之后，我们描述了块的规范，以便我们可以在下一节中解释验证。我们将块的规格声明为定义输出输入。串行_并行_规格（t输出输入）=（BITt输出=输入）它只是把块的输入和输出之间的关系放在位位置上。在每个时间t，我们有一个输入进入块，∃A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）317≤ ∧ ≤⇒⇒在与输出的当前索引t相关的位位置一种更通用的方法是使用模运算来建模规范，但由于我们接下来将遵循的证明策略，这里不需要。与第4.1节中解释的QAM验证策略不同，我们采用案例分析方法来证明目标。我们可以将目标定义如下：输出输入t.（0 t t 5）=Serial_Parallel_IMP（t out input）=串行_并行_规格（t输出输入）它有一个非常通用的模式，就像任何其他目标一样，除了将t限制为0≤t≤5的约束。边界t有助于克服我们前面提到的循环问题。我们只需要一次完整的迭代就足以证明给定块的功能正确性。这就是为什么我们只绑定变量来检查从t= 0到t= 5的情况一旦我们完成与案例分析我们证明以下平凡引理不客气。（0≤tt≤5）=（t=0）（t=1）（t=2）（t=3）（t=4）（t=5）它简单地说，当t被限制在0和5之间时，正确性定理需要保持的唯一值是t= 0， 1， 2， 3， 4， 5。我们证明了目标，从而验证了上述RTL块的功能。按照类似的方法，我们已经证明了P/S块的正确性。细节可以在[1]中找到。4.3讨论以上针对OFDM RTL块完成的建模、规范和验证展示了我们已经描述了使用形式逻辑在HOL中的RTL块的实现。对于QAM块，可以直接将if-then-elseHDL代码嵌入HOL中，并且从IEEE 802.11规范中获得规范。虽然解调器模块具有类似的实现方式，并且其形式描述类似于QAM模块，但是使用IEEE标准无法找到检查设计的规范，因为该模块位于接收器侧，设计者可以自由选择任何方式来实现它。QAM和解调器的规范都基于查找表，并且实现被证明与这些规范相反。对于S/P和P/S块，在对VHDLPROCESS进行了大量考虑之后，也对规范和实现进行了形式化。所有区块的验证都是使用HOL中关于实数、自然数、布尔逻辑、列表、单词等的现有理论完成的为了辅助证明步骤，证明了许多引理。有些引理是非常琐碎的，但HOL要求每一个证明步骤都是合理和完整的，这就是为什么HOL证明中没有歧义。内置的重写策略RW TAC被大量用于强大的简化集，与所需的引理和定理。 在大多数情况下，证明策略首先用手工绘制一个粗略的证明草图，然后在HOL中形式化但是一些∀18A.N.M. Abdullah等人/理论计算机科学电子笔记242（2009）3引理和中介定理足够简单，不需要采用这种方法。使用形式验证的主要目的是发现设计中的bug。我们没有在区块中发现任何bug。但是，有些评论是有道理的。也就是说，对于QAM块，在标准中给出了64-QAM调制的输入必须遵循图3所示的星座图。星座输出在-7到7之间，但实现使用了16位2数字来表示这些数字，而3位将完成相同的工作。如果严格遵循标准，那么这个问题可能会导致设计中的错误。但是，该标准为设计人员提供了一些灵活性，以便从IFFT块获得更精确的结果，如前面第4.1节所述。由于我们在验证时已意识到这一点，因此我们使用适当的位数限制了实现。相同的注释适用于DQAM块。对于其余的块，我们没有发现任何这样的问