《国外电子与通信教材系列:硬件设计验证·基于模拟与形式的方法》全面介绍硬件系统设计验证的技术和方法,主要涉及基于模拟和形式验证的方法,内容涵盖静态检验、模拟器体系结构、测试基准设计、模拟规划与策略、调试进程与验证周期、形式验证背景知识、判定图与SAT问题、符号计算与模型检验。书中汇集大量设计验证的基本概念与技术,内容深入浅出,叙述详尽,既讨论一般的测试原则又展示具体的实践方法,包含作者多年实践经验,实用性强。每章最后还配有各类习题,读者可用来巩固所学的知识。
无线传感器网络(WSN)已经引起了那些和物理世界具有紧密关联的、范围广泛的学科领域的兴趣。分布式的环境感知能力,基于无线通信技术的简单灵活的部署方式,使得WSN成为影响我们日常生活的重要因素。通过提供分布式的实时的环境感知信息,WSN将现代通信技术基础建设拓展到了物理世界中。WSN由微小的传感器节点组成,这些节点既具有获取信息数据的功能也承担着网络中继的功能。每个传感器节点都由若干传感器、微处理器和无线收发机组成,这些有效的传感器节点紧密相联获取物理现象的数据。传感器节点通过片上微处理器可以完成复杂的任务而不是仅仅传输它们感知到的信息,通过无线收发机可以实现相互联接以传输这些数据。传感器节点一般都是静止的并由能量有限的电池提供能源,所以即使节点位置没有变化,网络拓扑结构也会由于传感器节点的能量管理操作而发生动态变化。例如,为了节省能量,节点会关闭它们的收发机,但这样就使得它们与网络断开,从而导致网络拓扑的变化。在这种复杂环境中,如何使传感器节点功耗最小并保持联网是最主要的挑战。具有高能效机制的WSN相对于其他任何依赖电池的系统将具有更长的网络生存期。
2002年3月,我们的调查报告“Wireless sensor networks: A survey”发表在EI检索期刊Computer Networks上。接着,2002年8月,“Wireless sensor networks: A survey”的精简版发表在 IEEE Communications Magazine上。这些年来,以上两篇文章在超过8000个检索索引的检索库Elsevier和IEEECommunication Society(ComSoc)中高居文章被下载次数排名前十①。此后,挑战WSN特性的研究得到了迅速发展。最近十年来,WSN技术的研究获得了可喜的成果,高技术含量的产品得以制造和改进,由此开创了一个由WSN技术推动的崭新市场。经过这些年的努力,WSN的部署已经成为现实,诸多研究机构也从中获得了宝贵的经验。此外,许多专家正致力于对现有WSN能效解决方案的改进研究,并着眼于新型的WSN技术,例如水下和地下传感器网络。这些年来,我们也一直致力于WSN的研究,在近十年里发表了大量的论文并作了四个分别关于无线传感器与执行器网络、水下无线传感器网络、地下无线传感器网络和多媒体无线传感器网络的综述性的报告。
2003年夏,随着WSN技术的研究开始明朗化,我们开始第二轮撰写WSN综述性报告以研究最新的解决方案。大量的研究成果以及学术界和工业界的兴趣激励我们对WSN展开了进一步的研究并且撰写了本书。本书既可以作为研究生的教材以激发他们的创新思想,也可以为科研人员和工程师提供有关WSN技术的概况,并通过对WSN最新技术的深度剖析和对怎样优化现有技术继而应用到新兴应用和服务中的介绍引起读者更有深度的思考。本书涵盖了现有的WSN技术研究、应用以及众多应用领域中对这些技术的改进。本书凝聚了作者自己的研究成果以及由标准委员会做出的相关共识。由于近十年来对WSN的研究众多,本书不可能涵盖每一种解决方案,如有疏漏纯属无意。本书的内容主要遵循TCP/IP协议栈的分层架构,从物理层开始详细介绍了每一层的技术,并且深入分析了诸如同步、定位和拓扑控制的跨层解决方案和服务策略以及WSN的其他特性。本书深入地阐释了网络架构每一层的功能、协议和算法,旨在向读者介绍现有技术并且在本书最后一章中指出了WSN所需面对的巨大的研究挑战,以此来启发读者对现有方案进行改进和优化。第1章是对WSN的概述,概要地介绍了传感器平台和网络结构。第2章对WSN现有的应用进行了总结,包括军用和民用。第3章综述了WSN的特性、关键设计因素和限制条件。第4章致力于WSN物理层的研究,包括物理层的技术、无线通信的特点和物理层的标准。
第5章主要介绍了WSN的MAC协议,重点介绍了应用广泛的最基础的载波侦听多点访问/冲突避免(CSMA/CA)技术、由CSMA/CA改进而来的截然不同的解决方案:基于时分多点接入(TDMA)的MAC以及二者的混合方案。第6章重点介绍了WSN中的差错控制技术并且分析了它们对高能效通信的影响。第5章和第6章介绍的都是数据链路层的技术。第7章致力于WSN的路由协议研究。将网络层的路由协议分为四类:以数据为中心的路由协议、分层路由协议、地理路由协议和基于服务质量(QoS)的路由协议。第8章首先指出了传输层解决方案的挑战然后阐述了传输层的协议。第9章介绍了每层之间的跨层相互作用以及对通信表现的影响。此外,详细阐述了跨层通信方法。第10章指出了时间同步的挑战并且介绍了几种针对这些挑战的解决方法。第11章描述了定位技术的挑战并将定位技术分为三类:测距技术、基于测距的定位协议和无需测距的定位协议。第12章介绍了WSN中的拓扑管理方案。具体而言,解释了部署、能量控制、活动状态、调度和分簇方法。第13章介绍了无线传感器与执行器网络(WSAN)的概念和特点。特别强调了传感器和执行器之间以及不同执行器之间协同问题的解决方案。此外,还讨论了WSAN中的通信问题。第14章介绍了无线多媒体传感网(WMSN)的挑战和多种网络拓扑。还介绍了现有的多媒体传感器平台并遵循TCP/IP协议栈结构描述了各层的协议。第15章致力于水下无线传感网(UWSN),主要分析了水下环境对通信的影响。研究了水下声波传播的基础,总结了协议栈各层的解决方案。第16章描述了无线地下传感网(WUSN)的特点和应用。特别地,详细介绍了WUSN在土壤、矿井和隧道环境中的应用及特点。同时研究了在上述情况下的信道特点,并指出了给通信带来的挑战。最后,第17章讨论了WSN发展面临的巨大挑战。撰写一本教科书肩负有很大的责任和挑战。
第1章 设计验证的缘由
1.1 什么是设计验证
1.2 验证的基本原理
1.3 验证方法学
1.4 基于模拟的验证与形式验证的比较
1.5 形式验证的局限性
1.6 Verilog语言调度和执行语义简介
1.7 本章小结
第2章 编写验证的代码
2.1 功能正确性
2.2 时序正确性
2.3 模拟的性能
2.4 可移植性与可维护性
2.5 可综合性、可调试性与通用工具兼容性
2.6 基于周期的模拟
2.7 硬件模拟/仿真
2.8 2状态与4状态模拟
2.9 linter程序的设计与使用
2.10 本章小结
2.11 习题
第3章 模拟器体系结构与操作
3.1 编译器
3.2 模拟器
3.3 模拟器的分类与比较
3.4 模拟器的操作与应用
3.5 增量式编译
3.6 模拟器控制台
3.7 本章小结
3.8 习题
第4章 测试基准组成与设计
4.1 测试基准的分类与测试环境
4.2 初始化机制
4.3 时钟生成与同步
4.4 激励生成
4.5 响应评估
4.6 验证实用程序
4.7 测试基准至系统设计接口
4.8 常见的实际技术与方法
4.9 本章小结
4.10 习题
第5章 测试构想、断言与覆盖
5.1 分层验证
5.2 测试规划
5.3 伪随机测试生成程序
5.4 断言
5.5 SystemVerilog断言
5.6 验证覆盖
5.7 本章小结
5.8 习题
第6章 调试进程与验证周期
6.1 故障捕获、范围压缩与错误跟踪
6.2 模拟数据转储
6.3 潜在故障原因的隔离
6.4 系统设计更新与维护:修改控制
6.5 回归、发布机制与流片标准
6.6 本章小结
6.7 习题
第7章 形式验证初步
7.1 集合与运算
7.2 关系、划分、偏序集与格
7.3 布尔函数与表示
7.4 布尔函数运算符
7.5 有限状态自动机与语言
7.6 本章小结
7.7 习题
第8章 判定图、等价检验与符号模拟
8.1 二叉判定图
8.2 判定图的变异
8.3 基于判定图的等价检验
8.4 布尔可满足性
8.5 符号模拟
8.6 本章小结
8.7 习题
第9章 模型检验与符号计算
9.1 性质、规范与逻辑
9.2 性质检验
9.3 符号计算与模型检验
9.4 符号CTL模型检验
9.5 计算改进
9.6 模型检验工具的使用
9.7 本章小结
9.8 习题
参考文献
缩写词汇表