（电子科学与技术专业论文）软、硬件协同验证研究.pdf

软、 硬件协同验证研究第一章序言 第一章序言 软、硬件协同验证技术是近年来一项新兴的验证技术.针对一个特定系统， 其目 的在于在系 统设计中 尽可能多的发现系统与软、 硬件都相关的错误或因其中 一方面设计不当而引起的系统错误， 以避免系统设计后期因对系统进行大的改动 而引 起的人力、物力时间上的巨大浪费. 在实际应用中， 软、 硬件协同 验证技术贯穿于系统设计的各个阶段. 尤其是 在系统设计早期， 应用软、 硬件协同验证技术， 可以极大的缩短开发周期， 尽可 能早、 尽可能多地发现错误. 结合软、 硬件各自 的验证技术和测试技术， 使我们 的系统设计尽可能安全稳定. m o d e l c h e c k i n g 技术的 提出 始于上世纪7 0 年代末期， 作为一种成熟的 验证技 术，已经被成功地使用到软件验证和硬件验证中. 这种基于状态迁移、 遇历的技 术， 虽然使用有些复杂， 但对于一个系统， 尤其是一个特定系 统而言， 事实 证明 它是非常有效的， 甚至可以说是必不可少的。因 此， 作者提出 将其运用到软、 硬 件协同验证中. 本章将分验证与测试、 软、 硬件协同 验证和形式化验证等几个部分进行介绍 与讨论. 南开欠学电 子科学与 技术系2 0 0 2 年 s 月 s4a a. u 软、 硬件协同 脸证研究第一章序言 芬 1 . 1 验证与测试 1 . 1 . 1 测试 ( t e s t i n g ) 从系统生存周期淆， 测试是卡住系统质1， 尤其是卡住系 统可靠性的欢后一道关口. 但 系 统测试并不仅仅 局限于这个阶 段， 而 应贯穿于系统开 发的全过程. 应解决这样一个认识问 题一一 对于 任何一类的复杂系 统，自 认为没有错误的 想法是不切合实际的. 因 此， 浏试的 主 要 目的是: 1 ) 对系 统的 质1或可 接受 性作出 ，1 .1 断. 2 ) 发现问 题. 会产生 错误的阶 段主要在雷求说明、 设计和编程过程中 . 这些4 翻 误若不排除， 均会遗传到测 试阶 段， 甚至会遗传到 使用阶段. 系 统测试要求在测试过程中， 采集系 统可靠 性数据， 并利用系统可扣性 模型进行可靠 性 评估. 分析其是否达到了 预期的可金 性要求. 并 据此作出 该系 统能否放行的决断. 若不满 足 要求，需继续进行测试，直到满足要求为止.可见这是一项十分花精力的事情. 1 . 1 . 2 验证 ( v e r i f i c a t i o n ) 验证关心的是确保系统模块或功能内在的正确性. 验证是贯穿于系 统开发过程中 十分细致的 检验活动. 每个开发阶 段的结果可认为是下一 开发阶 段的一个规格文件， 但要进入下一阶 段之前必须时该结果作出确认. 通常的 验证的 主 要方法 有: 走查、 审查、 正确性证明等. 走查就 是对文档进行书面检查， 人工 模拟执行过程， 检查 设计的 正确性. 人工模拟也像实际系 统执行那 样， 可以 仔细 推敲、 校验和核实 每一步的 执行结果， 进而确定其执行逻辑、 撞制模型、算法和 使用参数与数据的正确性. 审查 走验证中的一个主要方法，可弥补其他方法的一些不足之处.它是一种用形式的、 有效的 和经 济的方法查 找设计和编 程中 的 4 价 误. 审查 的 主 要目 的 是 d 找出系 统中 的 缺fa ; 2 ) 核实 是否 符合需求; 3 ) 早期生产 评价; 4 ) 过程 评 价等 .由 第三方 进行评测工 作是十分重 要 的， 其评测工具软件对系统进行铮态的和动态的评测， 能发现系统设计的缺陷、 瓶颈和多余 物等. 值得 指出 的是， 用于测试的 各种方法、 技术、 工具和 措施等， 时 提高 软件的 可靠 性都 是必要的， 但不是充分的.这就表明，其中 任 何一个手段，均不能绝对保障系统的可和 但只要能 发现系 统中 任何一个徽小的错误， 就起到了 它的 作用. 1 . 1 . 3 验证与测试的联系与区别 在一个系 统的开发过程中， 脸证与测试是相辅相成， 缺一不可的. 验证主要集中在系统 设计早期， 主要关心系统的功能与性能的设计是否合理. 进免由于设计不当 造成的系统错误. 其主要是通过模拟运行及理论推导的方法来证明系 统的正确性. 测试则贯穿于系统设计的各 个阶段. 虽然测试也是要尽可能多 地找出系 统存在的 错 误， 但这些错误的根源是各不 相同的. 测试更主要的是关心系 统的质1. 其主要方法 是通过大圣的测试用例找错误， 同时采集数据 以 评价系 统的质t. 测试与验证都不能百分之百地保证系统的正确性、可盒性. 南开大 学电干科学与技术系 2 0 0 2 年 5月 软、 硬件协同脸证研究第一章序言 1 . 2 软、硬件协同验证及其重要意义 1 . 2 . 1 软、硬件协同验证 目 前， 关于软、 硬件协同 验证还没有一个标准的解释. 作者认为， 以下儿种情况都可以 看作是软、 硬件协同 验证的范畴. ( i ) 利用虚拟硬件检查软件的错误. ( z ) 利用虚拟软件检查硬件的错误. ( 3 ) 利用虚拟的软件、 硬件检查二者的兼容性，以发现在设计过程中由于考虑不周而引 起 的软硬件不兼容的 错误. 由 此可以 看出， 软、 硬件协同 验证的关 健问 题是 “ 虚拟”问 题.实际上， 虚拟问 题也就 是如何描述的问 题. 在描述语言上， 软件语言通常是 c或c + + ;硬件上，通用的语言是硬 件描述 语言 h d l 一 一 h a r d w a r e d e s c r ip t io n l a n g u a g e ) ， 但由于c / c + + 被广泛 运用于 代 码编 写中， 用c / c + + 描述硬件已 经成为一个祈的 研究领城. 在描述方法上， 直接描述系 统本身的 功能性， 可以直接生成所需的软件、 硬件， 但这种方法往往不适用于脸证系统; 相反的， 用 形式 语言 描述软件、 硬件有利于验证. 对于一个复杂的， 特定功能的系 统， 用形式 语言描述 进行功能、 性能等方面的 描述，虽然不能直 接生成产品， 但可以确保系 统的可靠 性. 往往， 一个不可幸因紊会导致整个系 统设计失败甚至使用崩清.用形式语言 描述系 统虽然非常复 杂， 但这种代价是非常有效和必要的. 1 . 2 .2 软、硬件协同 验证的意义 1 .缩短开发周期 在没有软、 硬件协同 验证枚术之前， 时于一个系 统， 尤其是嵌入式系 统， 开发者往往需 要等到真正的物理硬件完全调试好之后，才开始写软件，进行软件调试.其开发过程如图 l . l a .虽然， 仿真器 可以 解决一些问 题， 但通常是无济于事的. 这是因为仿真器的 速 度远差 于实际系 统， 代码黄大时， 仿真器 执行全过程所需的时间 是通常的 调试根本无法忍受的. 同 时， 在硬件成型后， 我们很难修改由于硬件设计不当产生的错误， 即使修改， 也要付出 相当 大的代价.系统越复杂， 这个问 题就越突出. 然而， 开发者希望尽可能缩短开发周期， 以加 快产品进入市场，节省人力、物力. 软、硬件协同 脸证技米可以使软件、 硬件开发同步进行 ( 如图 1 . 1 b ) ， 在虚拟的硬件上调试软件， 同时检查硬件是否存在问 题， 及时 修改硬件设计 中的错误. 开始 硬件设计 2 . 避免因软、硬件设计不一致 或不周产生的错误 法国航天飞机第一次升 空失败并导致爆炸， 事 后的事 故分析表明， 由于 设计者最初 时计算机的处理能力估计不 足， 导致升空 过程中 一个 浮点 到定点的转换溢出， 使航天飞 机的 计算 机系 统停止工作. 这 种错误是由于设计者在最初 硬件调试 图1 - l b 并行开发流枉 使硬件无法满足软件的需求. 结束 图 i 一 l a 串行开发流程 对软件、 硬件的处理能力佑计不足， 在串 行设计流程中， 后期 南开大学电干科学与技术系 2 0 0 2 年 5月 软、 硬件协同脸证研究第一幸序言 发现的 硬件错误通常只能 在软件中 加以弥 补， 但这种弥补通常会影响软件的性能. 而 且， 并 不是所有的 硬件错误都是可以弥 补的. 这使设计者不得不重新修改硬件设计， 软件又 要等 待 硬件.这样做不仅费时、更 会造成经济损失. 使用协同 验证技术，可以更 有效地在早期 发现由于 软件、 硬件设计不一致产生的 wk . 及时修改硬件、软件设计，进免后期或使用期间造成的严重损失. 1 . 3 形式化验证 在本节中 ， 我们主 要 介绍 两 种形 式 化 验 证 技术 ， 一 种 是 理 论证明( t h e o r e m p r o v in g ) , 一 种是 模型检验 ( m o d e l c h e c k in g ) . 本文将采 用 模型 检验的方法. 1 .3 . 1 t h e o r e m p r o v i n g t h e o r e m p r o v in g 用 公理和 定理 来证明系 统的 正 确性.以 前， 这种证明完 全是金 人手 工 完 成的 .目 前， 已 经 有非常 有效的 软 件工 具一 一 t h e o r e m p r o v e r s 来辅助证明. 这种工 具可以 确保公理、 定理使用的正确性，并为证明 提供正确的方向. t h e o r e m p r o v i n g 对于 无限状态 系 统是非常有效的. 然而， 这种方法过于复杂. 对于一个简单的电 路或协议， 需要人为地详 细证明成百上千个辅助定理.例如， a m d 5 k 8 6 的浮点教除法的分析证明需要证明1 6 0 0 个 辅助定理.即 使付一 个数学 工 作者来 讲， 这 也 是令 人难以 忍受的. t h e o r e m p r o v in g 的另 一 个缺点是，不能预见一个证明所需 要的时间和 存储空间. 1 . 3 . 2 mo d e l c h e c k i n g m o d e l c h e c k in g 可以 说是一 种验 证有限 状态系 统的自 动技术. 时于 一个严 格给定 的 有限 状态系统， 这种技术可以自 动地、 全部地选历整个系统的状态空间以检查是否符合功能需求 和是否有错误存在.同时， 这种技术可以自 动地跟踪遮历过程， 以找到错误的根源. 使用适 当 的方 法， 选历所需的时间 和 存储空间 是可以 预见的. m o d e l c h e c k in g 的 缺点 在于， 系 统 每 增加一个参数，增加的状态会以几何级数递增. 目 前，大多 数的 验证方法采用m o d e l c h e c k in g . 本文 将就m o d e l c h e c k i n g 及 应用m o d e l c h e c k i n g 进行软、 硬件协同 验证的可 行性等 有关问 题进行更深入的讨论. 1 . 4 全文总揽 本文总 体分为两部分.第一 部分 第二章) 以s e a m l e s s c v e为基础， 提出 针对特定系 统的改 进意 见;第二 部分提出 将m o d e l c h e c k in g 技术 应用到 软、 硬件协同 验证中 . 在第二章中， 介绍一款目 前占 主导地位的 软、 硬件协同 验证产品. 并通过对该产品的 技 术分 析、 提出 作者的几点想法.最后，以8 0 5 1 单片 机及其中断为例， 介绍实现方法. 在 第 三 章中 ， 将 时m o d e l c h e c k in g 技 术 进 行 具 体 介 绍 ， 并 推 导出“ 极 限 情 况 ， 下 遮 历 路 径总童公式. 在第 g 章中 ， 将介 绍m o d e l c h e c k i n g 的s y m b o l ic m o d e l c h e c k in g 技术. 并若 重 介 绍c t l 和b d d 技术 . 并分 析 将m o d e l c h e c k in g 技术 应 用于 软、 硬件 协同 验证的 可 行 性. 在第 五幸中， 我们将以8 0 5 1 的中 断系 统为 例， 对在第三、 四两 章中 提出 的想法 和问 题 进行具体的分析，实践，以分析其性能. 在第六章中，我们将对全文进行总结，并提出一些有待研p的问 0. 南开大学电子科学与技术系2 0 0 2 年 5月 软、硬件协同脸证研究第二章 软、 硬件协同脸证技术及改进 第二章软、硬件协同验证技术及改进 软、 硬件协同 验证技术从提出 到形成产品不过短短几年时间.目 前， 世界上 已 经至少 有三款软、 硬件协同 验证产品. 三种产品的 基本技术大同小异. 在本章 中 我 们以m e n t o r g r a p h i c s 的s e a m l e s s c v e 为 例进行 详细 的 介绍和分析. 目 前，用c / c + + 来描述硬件成为一个趋势，结合对s e a m l e s s c v e的分析， 作者提出了几点基于s e a m l e s s c v e技术的改进想法，以应用于对硬件的c / c + + 描述.这些方法对于特定的系 统更为有效， 可以有效地缩短时间，节省空间. 本章的第一节将介绍s e a m l e s s c v e的技术， 第二节将提出 作者基于s e a m l e s s c v e 技术的改进意见， 第三节将以8 0 5 1 为例， 对作者的想法进行更具体的阐述. 乍叼 月.，弓 南开大学电子科学与技术系 2 0 0 2 年 s 月 诬 : . jfl 乳少 翔 软、硬件协同验证研究 第二章软、硬件协同脸证技术及改进 怪 2 . 1 s e a m l e s s c v e技术 协同 验证技术通常是通过使软件工 作在一个 硬件模拟器上来检查错误一 个特殊的处理 器 模块负 责软、 硬件之间的交互工作，并且给软件开发者一个可视的调试软件的界面. s e a m le s s c v e( c o - v e r i f ic a t io n e n v ir o n m e n t ) ( 以f 简 称c v e ) 通过集 成硬件仿真工 具和 软 件调试工具为开发者提供了 一个软、 硬件协同 验证的工作环境. 2 . 1 . 1 软、硬件协同验证技术简介 c v e 包 含了 一个特殊用 途的处 理器 模块 ( 以 下简 称s p m 一一s p e c ia l p u r p o s e m o d e l ) , 该模块带有一个运行在逻辑模拟器上的嵌入式系 统模块.硬件开发者通过硬件描述语言 ( h d l ) 来 描述这个 嵌入式系 统模块一个可 执行的im a g e 可以下 载到这个 模块的 存 储器中 ， 使其与工 作在真实环境中 一样. 在c v e中， s p m提供三个主 要功能， 1 .模拟处理器执行指令的过程，最普迫的办法是用一个指令集模拟器 ( i s s 一一 i n s t r u c t i o n s e t s i m u l a t o r ) . 2 . s p m可以使软件开发者肴到并影响软、 调试工具一样工作. 3 .处理器需要与硬件设计交互. s p m中的 一个总线接 口模 块 ( b i m一一b u s i n t e r f a c e mo d e l ) 提供7这个功能. 总线 接口 模块把处理器总线周期的动作翻 译成一系列的处理器引脚变 化，以此来 模拟逻辑模拟器的总线行为.同时总线 接口模块还需要处理由硬件设计产生 的外部事件， 如复 位、中 断， 异步触发 事件等. 硬件的 状态. 即此模块可以象一个有界面的 图2 - 1 c v e的工作原理 c v e把逻拜模拟器和所有的其他模块连 接在一 起 ( 如图2 - 1 ) ， 使它们能够协调工作. 通常， 工作流程是以启动迈样模拟器和软件调试器开始， 并建立软件、 硬件之间的通信联系 . 开 发者启 动 逻挥模拟器， 把可 执行的im a g e ( 软 件) 下载 到 退辑 模拟器中， 通过软 件、 硬件 的 调试器来 跟踪软、 硬件的工作情况. 与此同 时， 开发者可以 观察到寄存器、 存储空间的内 容变化.软件和硬件调试器都保持7它们各自 在单一环境中 工作的全部功能. c v e 是一个集成产品， i s s 和逻挥 模拟器都 是集成了 现有的产品. 对于任何一款处理器， 只要c v e支 持其仿真器 ( 逻辑模拟器) 和i s s ,就可以在c v e中 使用. 作者认为， c v e的关健技术在于s p m中 一个协调软、 硬件通信和进行优化的内 核. 这 项 技术m e n t o r g r a p h ic s 是不 对外 公开的 . 这个内 核使软硬件之间同 步工作， 并 优化整个c v e 的工作效率. 2 . 1 .2 优化模拟效率 时于一个包 含全部功能 模块和存储器的完整的软、 硬件协同 验证系 统， 我们可以 把所有 的 指令按照实际 运行流程在处理器、 存储器、 总线上一一实 现. 但这样做的速度会非常 馒， 在实际的 调试中， 这种速度几 乎是不 可以 忍受的. 分析表明， 典型的协同验证系 统每秒钟平 均可以 运行5 条指令.这样， 对于一个 有1 4 4 , 0 0 0 条指令的系 统而言，完整的 模拟 运行需 要8 个小时.而 且，这是在不考虑开发者对执行过程可视的情况下做出的统计. 南开大牛电子科学与技术系 2 0 0 2 年 5 月 软、硬件协同脸证研究第二章 软、硬件协同 脸证技术及改进 所有成功的 提高 模拟效率的方法大都采用了“ 隐 藏周期， 的办法. 这种方法把一系 列的 内 存搬移的过程放到主机上直接执行， 而不是以往的通过逞辑模拟器搬移. 这样可以在不影 响模拟结果的情况下压缩掉大量的指令周期. 考虑一个取指令的过程， 一个总线周期需要通 过内 存控制逻辑和一个或多个 存储器 把指令内 容取到处理器中， 作为下一条要执行的指令. 执行这一过 程，需要逻样模拟器处理上百个模拟事 件， 这会在主机上消耗大圣的计算时间. 然而， 这一过程对于 硬件、软件的 状态根本不会产生影响，完全可以不 使用迈辑模拟器. 在c v e中， 可以建立一个数据阵列使i s s 可以直 接从主机上提取指令，而不需 要通过 逻样模拟器 访问. 这样， 我们可以在i s s 中 加一个功能模块以 利断究竟禽 要执行哪种数据搬 移. 对于 指令的读取， 可以直 接在主 机上执行， 对于外部数据的读取， 则通过指令模拟器用 相应的总线周期 读取. 分析表明， 9 9 .9 %的指今周期可以 被屏蔽 掉.直接读取数据的速度比 通过邃辑模拟器读取快1 0 ,0 0 0 倍. 假设在这种情况下， 每秒钟可执行 1 0 0 , 0 0 0 次数据搬以和 5 个i / o数据搬移周期.则执行9 9 9 此指令搬移和以i 次数据橄移所用的时间为: 0 . 2 s + 0 . 0 0 9 9 9 s -0 . 2 0 9 9 9 s 如果不用这种方法则需要: 0 . 2 s 1 0 0 0 = 2 0 0 s 二者相差 1 0 0 0 倍. 2 . 1 .3 隐藏周期的补偿 由于我们所隐藏的存储器搬移周期不会改变 我们所模拟的 硬件的状态， 所以隐藏这种周 期不会对邃择模拟器 产生影响. 但是， 如果我们的系 统有要求精确时间的部分时， 如需 要定 时器工 作， 这种方法就会产生弊瑞. 我们称这种丢失时间 周期的 现象为“ 时间陷阱” . 在c v e 技术中， 至少雷 要做两 件事来补偿这种时间陷阱. 其一， 详细的 计算每次隐藏的时间; 其二， 由c v e 更改时间寄存器，并激活相应的时间应该有的事 件. 2 .2 针对特定系 统的改进意见 2 . 2 . 1 用 c / c + + 描述硬件 在c v e中， 逻挥模拟器和i s s 都是集成的 现有的产品. 对于一个特定系统而言，尤其 是在芯片 设计中， 有时我们需要根据需求设计特殊的 硬件. 在这种情况下， 集成通用产品显 然存在局限性.同时， 由于目 前大全的软件都采用了c / c + + ， 越来越多的人都在研究如何用 c / c *来描述硬件.而且， 用c / c + + 描述硬件的工具也已 经投入市场，可以用c / c + + 直接生 成h d l 语言甚至网 表. 因此， 作者认为， 可以在硬件设计早期， 针对硬件的功能性分析， 用c / c + + 直接描述硬 件. -i e .4 k 件代码放在这种功能性描述的 “ 虚拟硬件”上运 行、 以便在设计早期发现软、 硬件 的设计是否 存在不兼容的问 题. 同时， 这样的 验证方法可以使软、 硬件都在 “ 主 机” 上 运行， 非常有效的缩短了 验证所 需的时间.“ 主机”听能 提供的存储器也是足够 使用的，而 且， 访问 “ 主 机”存储器的速度 也会远远大于迈择模拟器的存储器. 2 . 2 . 2 优化验证的运行过程 在c v e 技术中，大 t的指令读取时间已 经被节约. 这是因为这种指令读取操作不会影 响逻辑模拟器的 状态. 如果对于一个功能明确的持定系 统， 有些指令的操作也是不 会影响软、 南开大学电子科学与技术系2 0 0 2 年5 月日 软 ，硬件协 同脸证研 究第二章 软、 硬件协同 脸证技术及改进 硬件工作状态的改变的. 这种指令直接由 软件在 “ 主机，上执行，而不通过 “ 虚拟硬件 执 行也是完全可以的. 这就要求在i s s 能够利定哪些指令需要放到 “ 虚拟硬件”上执行， 哪些 不需要.这种判断功能是完全有可能加到i s s中去的. 在一个特定系 统的 验证过程中， 有时我们只关心某一部分的 验证结果. 即有些指令对软 件、 硬件状态即 使有影响， 我们也不关心. 我们只要认真、 详尽地验证我们所关心的那部分 代码或功能 模块. 例如， 在一个系 统中，目 前我们只关心计算过程中 滋出 会不会导致死机问 题， 那么， 我们只需 要把这一部分 提出 来 放到“ 虚拟硬件， 上运行， 其余的 部分则直 接运行. 在这种优化的过程中， 我们仍然禽要关心 “ 时间陷阶”的问 题. 在这个问 题上要具体问 题具体分析， 因为时钟问 题在不同的处理器上的处理方法是不一样的. 关于本节所提到的改 进意见， 作者将在下一节中 以8 0 5 1 为例进一步讲述具体实 现. 虽 2 .3 8 0 5 1 的具体实现 5 1 系列 是最基础的 单片 机， 也是在小型系 统开 发中 使用最为 普迫的. 本节将以8 0 5 1 为 例，对上一节提出的观点进行具体的讨论.需要指出的是，我们是以8 0 5 1 为例来讨论作者 的观点，而这些观点仍然是针对特定的系统，特定的处理器而言的. 2 . 3 . 1 8 0 5 1 的体系结构 8 0 5 1 体系 结构简 单， 现简述如下: 8 位c p u 2 1 个特殊功能寄 存器2 个1 6 位定时 / 计数器 片内 振荡器3 2 根1 / o线5 个中断源， 有2 个 优先级 4 k r o m可寻址6 4 k外部r a m空间一个全双工串 行l ) 1 2 8 字节r a m可寻址6 4 k程序空间有位寻址能力 2 . 3 . 2 实现 i . 关于存储器部分 片 外部分， 我们可以在存储器中 分别开辟6 4 k字节的 数据空间和6 4 k字节的 程序空间. 片内 部分， 定义一个长度为2 5 6 的整形 数组， 前1 2 8 个元素作为片内1 2 8 字节r a m， 后 1 2 8 个元素作为2 1 个特殊功能 使用. 实际上， 我们只使用后 1 2 8 个元紊中 的2 1 个 作为特殊功能 寄 存器.这样做的目 的是方便寻址. 2 . i s s部分 读取指令后，交由 i s s进行分析以判定到底哪些需 要精确地按照在硬件执行的流程执 行， 那邢分可以直 接执行. 判断的标准是 足否 会改变 硬件的状态， 是否会造成溢出、 指针越 界等错误， 是否会涉 及我们特别关心的 硬件动作. 改变硬件的状态， 是指指令错做会改变一些特珠功能寄存器的值， 使系统的 状态发生改 变.如对中断允许寄存器的写 操作可能会使系 统由中断禁止态迁移到中 断允许态. 溢出、 指针越界等惜 误， 是指由 于计算能力 的限制而导致计算结果错误， 或指针超出了 所能控制的范围，并由 此导致一系列系统状态的不可预见性.如 s p( 堆找指针) 指向了目 前正在使用的r o - r 7 工作区，会改变 一些寄存器的值， 使系 统发生错误. 禽要指出的是， 时于昨c / c + + 指令集， i s s 还熏要一个编译过程， 现有的技术是完全可 以支持由一种语言到另一种语言的编译的. 3 . 1 / o部分 对于和外 设接口 的1 / o ， 我们可以 对每个 接口 设一个 数组或一个文件， 写入预先设定的 南开大 学电子科学与技术系 2 0 0 2 年 5月 软、硬件协同脸证研究第二章软、硬件协同 脸证技术及改进 值，根据需要依次读取. 4 . 时钟一一中断问题 在本节的讨论中，我们 只考虑由于中断而 产生的中 断问题. 5 1 系列单片机是在 每个及其周期的s s p 2 对中 断 请求位采样.所以我们考虑 在 i s s中对直接执行的指 令，在指令执行后，调用中 断处理函 数i n t e r r u p t ( i n t n ) . n为执行该条指令所需的 机 器周期， 是用来为定时器/ 计 数器 使用的.在定时器方式 时，只需 将相应时间寄 存器 的 值加n ; 在计数器方式时， 只需一次读取 n次相应的 i/ o接口的数据即可.中断 处理函 数 in t e r r u p t ( ) 的流 程图知图 2 - 2 ，相应的代码 见附录a . 关于中断i n t o / i n t i 的处理函数， 定时器八 十 数器 t o /t 1的处理函数也在附录 a中. 本文没有对串口中断 做深入研究. 图2 - 2 in t e r r u p t ( ) 的主 程序流图 南开大学电子科学与技术系 2 0 0 2 年 5月 软、硬件协同脸证研究 第三章m o d e l c h e c k i n g 介绍 第三章mo d e l c h e c k i n g介绍 随着软件、 硬件系统越来越复杂， 形式化方法被广泛的使用在系统描述和验 证中 . 在形式 化 验 证方 法中 ， m o d e l c h e c k i n g 是目 前 使 用 最广 泛的， 被 认为 是 最 有效的. m o d e l c h e c k i n g 是把系 统描述成为一个有限状态空间， 使系 统在这个有 限状态空间中不停的运转.目 前， 这种方法被广泛的使用在软件验证和硬件验证 中 . 在m o d e l c h e c k in g 中 ， 有两 种 主 要方 法， 其中 一 种是t e m p o r a l m o d e l c h e c k i n g . 这 是一 种 基于 事 态 逻 辑( t e m p o r a l lo g ic ) 的 描述 方法 . m o d e l c h e c k i n g 的最主要缺点在于 存在状态 数量爆炸的问 题. 对于一个复杂 系 统的 状态空间， 往往存 在 1 0 1 0 0 个以 上 状态空间， 在 这种情况下， 每增加一个 状态参量，系统的状态数童将会成倍增长.同时， 在通历过程中， 每增加一个状 态，系统需要遍历的数童也是骤增的. 在本章中， 将给出在 “ 极限情况”下，系 统所遥历的路径总量公式. 本 章第 一节 将 对 形式 化方 法 进 行介 绍; 第 二节 将 介绍m o d e l c h e c k in g以 及 t e m p o r a l m o d e l c h e c k in g ; 在第 三节中 ， 将 给出“ 极限 情 况 ”下， 遥历 状 态空 间 路径总童的公式证明. 在本章中，部分将使用英语. 南开大学屯子科学与技术系2 0 0 2 年 5月 软、硬件协同脸证研究第三章m o d e l c h e c k i n g 介绍 3 . 1 形式化方法 ( f o r m a l me t h o d s ) 3 . 1 . 1 w h a t a r e f o r ma l me t h o d s h a r d w a r e and s o ft w a r e s y s t e m s w i l l i n e v i t a b l y g r o w i n s c a l e a n d f u n c t i o n a l i t y . b e c a u s e o f t h i s i n c r e a s e i n c o m p l e x i t y , t h e l i k e l i h o o d o f s u b t l e e r ro r s is m u c h g r e a t e r . m o r e o v e r , s o m e o f t h e s e e r r o r s m a y c a u s e c a t a s tr o p h i c l o s s o f m o n e y , t i m e , o r e v e n h u m an l i f e . a m a j o r g o a l o f s o ft w a r e e n g i n e e r i s t o e n a b l e d e v e l o p e r s t o c o n s t r u c t s y s t e m s t h a t o p e r a t e r e l i a b l y d e s p i t e t h i s c o m p l e x i t y . o n e w a y o f a c h i e v i n g t h i s g o a l i s b y u s i n g f o r m a l m e t h o d s , w h i c h a r e m a t h e m a t i c a l l y b a s e d l ang u a g e s , t e c h n i q u e s , and t o o l s f o r s p e c i f y i n g and v e r i f y i n g s u c h s y s t e m s . u s e o f f o r m a l m e t h o d s d o e s n o t a p r i o r i g u a r a n t e e c o r r e c tn e s s . h o w e v e r , t h e y c an g r e a t l y i n c r e a s e o u r u n d e r s t an d i n g o f a s y s t e m b y re v e a l i n g i n c o n s i s t e n c i e s , a m b i g u i t i e s , an d i n c o m p l e t e n e s s t h a t m i g h t o t h e r w i s e g o u n d e t e c t e d . f o r m a l m e t h o d s m e ans t h e m a t h e m a t i c s and m o d e l i n g a p p l i c a b l e t o t h e s p e c i f i c a t i o n , d e s i g n , and v e r i f i c a t i o n o f s o ft w a r e . t h e e m p h a s i s i s o n t h e c r e a t i o n o f t h e o r i e s and t o o l s t o a i d t h e s e a c t i v i t i e s . t h e m e t h o d s a r e f o r m a l i n t h e s e s e n s e t h a t t h e y a r e p r e c i s e e n o u g h t o b e i m p l e m e n t e d o n a c o m p u t e r . wi t h t h e s e t e c h n i q u e s , w e c an d e v e lo p s p e c i f i c a t i o n s and m o d e l s w h i c h d e s c r i b e a l l o r p a rt o f a s y s t e m s b e h a v i o r a t v a r i o u s l e v e l s o f a b s tr a c t i o n , and u s e t h e m a s i n p u t t o an a u t o m a t e d t h e o r e m p r o v e r . f o r re q u i re m e n t s e n g i n e e r i n g . t h e i n p u t m a y b e a c o l l e c t i o n o f p a rt i a l s p e c i f i c a t i o n s , and t h e o u t p u t m a y b e a re p o rt o n w h e re i n c o n s i s t e n c i e s l i e . f o r d e s i g n , t h e i n p u t m a y b e a s p e c i f i c a t i o n and a d e s i g n s t e p , and t h e o u t p u t i s e i t h e r y e s , t h e d e s i g n s t e p i s c o n s i s t e n t w i t h t h e s p e c i fi c a t i o n . o r n o , and h e re s w h y n o t : . . . . f o r v e r i f i c a t i o n , t h e i n p u t m a y b e a s p e c i f i c a t i o n an d a d e s i re d p r o p e r ty o f s y s t e m b e h a v i o r , and t h e o u t p u t m a y b e e it h e r y e s , t h e p r o p e r ty i s a c o n s e q u e n c e o f t h e s p e c i f i c a t i o n . , o r n o , and h e re s w h y n o t : ， 二 ” . a lt h o u g h a c o m p l e t e f o r m a l v e r i f i c a t i o n o f a la r g e c o m p l e x s y s t e m i s i m p r a c t i c a l a t t h i s t i m e , f o r m a l m e t h o d s a re a p p l i e d t o v a r i o u s a s p e c t s , o r p ro p e rt i e s , o f l a r g e s y s t e m s . m o r e c o m m o n l y , t h e y a r e a p p l i e d t o t h e d e t a i l e d s p e c i f ic a t i o n , d e s i g n , and v e r i f i c a t i o n o f c r i t i c a l p a rt s o f la r g e s y s t e m s s u c h a s mo n i t o r s . a v i o n i c s a n d a e r o s p a c e s y s t e m s , and t o s m a l l , s a f e t y - c r i t i c a l s y s t e m s s u c h a s h e a rt 3 . 1 . 2 s t a t e o f t h e ar t i n t h e p a s t , t h e u s e o f f o r m a l m e t h o d s i n p r a c t i c e s e e m e d h o p e l e s s . t h e n o t a t i o n s w e r e t o o o b s c u r e , t h e t e c h n iq u e s d i d n t s c a le , and t h e t o o l s u p p o rt w a s i n a d e q u a t e o r t o o h a r d t o u s e . t h e r e w e r e o n l y a f e w n o n t r i v i a l c a s e s t u d i e s an d t o g e t h e r t h e y s t i l l w e re n o t c o n v i n c i n g e n o u g h t o t h e p r a c t i c i n g s o ft w a r e o r h a r d w a re e n g i n e e r . f e w p e o p l e h a d t h e t r a i n i n g t o u s e t h e m e ff e c t i v e l y o n t h e j o b o n ly i n t h i s t e n y e a r s h a v e w e b e g u n t o s e e a m o re p ro m i s i n g p i c t u r e o f f o r m a l m e t h o d s . f o r s o f t w a r e s p e c i f i c a t i o n . i n d u s t r y i s o p e n t o t r y i n g o u t n o t a t i o n s s u c h a s z t o d o c u m e n t a s y s t e m s p r o p e rt ie s m o r e r i g o r o u s l y . f o r h a r d w a r e v e r i f i c a t i o n , i n d u s t ry i s a d o p t i n g t e c h n i q u e s s u c h a s m o d e l c h e c k i n g an d t h e o re m p r o v i n g t o c o m p l e m e n t t o m o r e tr a d i t i o n a l o n e o f s i m u l a t i o n . i n b o t h a r e a s , r e s e a r c h e r s and p r a c t i t i o n e r s a r e p e r f o r m i n g m o r e an d m o r e i n d u s t r i a l - s i z e d c a s e s t u d i e s , a n d t h e r e b y g a i n i n g t h e b e n e f i t s o f u s i n g f o r m a l m e t h o d s . 南开大学电 子科学与技术系2 0 0 2 年 5 月1 5 大抽肚 l翻 软、硬件协同脸证研究第三章m o d e l c h e c k i n g 介绍 1 . s p e c i fi c a t i o n s p e c i f i c a t i o n i s t h e p r o c e s s o f d e s c r i b i n g a s y s t e m a n d i t s d e s i r e d p r o p e rt i e s . f o r m a s p e c i f i c a t i o n u s e s a l a n g u a g e w i t h a m a t h e m a t i c a l l y d e f i n e d s y n t a x a n d s e m a n t i c s . t h e k i n d s o f s y s t e m p r o p e rt i e s m i g h t i n c l u d e f u n c t i o n a l b e h a v i o r , t i m i n g b e h a v i o r , p e r f o r m a n c e c h a r a c t e r i s t i c s , o r