《國外電子與通信教材系列：硬件設(shè)計(jì)驗(yàn)證·基于模擬與形式的方法》全面介紹硬件系統(tǒng)設(shè)計(jì)驗(yàn)證的技術(shù)和方法，主要涉及基于模擬和形式驗(yàn)證的方法，內(nèi)容涵蓋靜態(tài)檢驗(yàn)、模擬器體系結(jié)構(gòu)、測試基準(zhǔn)設(shè)計(jì)、模擬規(guī)劃與策略、調(diào)試進(jìn)程與驗(yàn)證周期、形式驗(yàn)證背景知識、判定圖與SAT問題、符號計(jì)算與模型檢驗(yàn)。書中匯集大量設(shè)計(jì)驗(yàn)證的基本概念與技術(shù)，內(nèi)容深入淺出，敘述詳盡，既討論一般的測試原則又展示具體的實(shí)踐方法，包含作者多年實(shí)踐經(jīng)驗(yàn)，實(shí)用性強(qiáng)。每章最后還配有各類習(xí)題，讀者可用來鞏固所學(xué)的知識。
無線傳感器網(wǎng)絡(luò)（WSN）已經(jīng)引起了那些和物理世界具有緊密關(guān)聯(lián)的、范圍廣泛的學(xué)科領(lǐng)域的興趣。分布式的環(huán)境感知能力，基于無線通信技術(shù)的簡單靈活的部署方式，使得WSN成為影響我們?nèi)粘Ｉ畹闹匾蛩亍Ｍㄟ^提供分布式的實(shí)時(shí)的環(huán)境感知信息，WSN將現(xiàn)代通信技術(shù)基礎(chǔ)建設(shè)拓展到了物理世界中。WSN由微小的傳感器節(jié)點(diǎn)組成，這些節(jié)點(diǎn)既具有獲取信息數(shù)據(jù)的功能也承擔(dān)著網(wǎng)絡(luò)中繼的功能。每個(gè)傳感器節(jié)點(diǎn)都由若干傳感器、微處理器和無線收發(fā)機(jī)組成，這些有效的傳感器節(jié)點(diǎn)緊密相聯(lián)獲取物理現(xiàn)象的數(shù)據(jù)。傳感器節(jié)點(diǎn)通過片上微處理器可以完成復(fù)雜的任務(wù)而不是僅僅傳輸它們感知到的信息，通過無線收發(fā)機(jī)可以實(shí)現(xiàn)相互聯(lián)接以傳輸這些數(shù)據(jù)。傳感器節(jié)點(diǎn)一般都是靜止的并由能量有限的電池提供能源，所以即使節(jié)點(diǎn)位置沒有變化，網(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)也會由于傳感器節(jié)點(diǎn)的能量管理操作而發(fā)生動態(tài)變化。例如，為了節(jié)省能量，節(jié)點(diǎn)會關(guān)閉它們的收發(fā)機(jī)，但這樣就使得它們與網(wǎng)絡(luò)斷開，從而導(dǎo)致網(wǎng)絡(luò)拓?fù)涞淖兓Ｔ谶@種復(fù)雜環(huán)境中，如何使傳感器節(jié)點(diǎn)功耗最小并保持聯(lián)網(wǎng)是最主要的挑戰(zhàn)。具有高能效機(jī)制的WSN相對于其他任何依賴電池的系統(tǒng)將具有更長的網(wǎng)絡(luò)生存期。
2002年3月，我們的調(diào)查報(bào)告“Wireless sensor networks: A survey”發(fā)表在EI檢索期刊Computer Networks上。接著，2002年8月，“Wireless sensor networks: A survey”的精簡版發(fā)表在 IEEE Communications Magazine上。這些年來，以上兩篇文章在超過8000個(gè)檢索索引的檢索庫Elsevier和IEEECommunication Society（ComSoc）中高居文章被下載次數(shù)排名前十①。此后，挑戰(zhàn)WSN特性的研究得到了迅速發(fā)展。最近十年來，WSN技術(shù)的研究獲得了可喜的成果，高技術(shù)含量的產(chǎn)品得以制造和改進(jìn)，由此開創(chuàng)了一個(gè)由WSN技術(shù)推動的嶄新市場。經(jīng)過這些年的努力，WSN的部署已經(jīng)成為現(xiàn)實(shí)，諸多研究機(jī)構(gòu)也從中獲得了寶貴的經(jīng)驗(yàn)。此外，許多專家正致力于對現(xiàn)有WSN能效解決方案的改進(jìn)研究，并著眼于新型的WSN技術(shù)，例如水下和地下傳感器網(wǎng)絡(luò)。這些年來，我們也一直致力于WSN的研究，在近十年里發(fā)表了大量的論文并作了四個(gè)分別關(guān)于無線傳感器與執(zhí)行器網(wǎng)絡(luò)、水下無線傳感器網(wǎng)絡(luò)、地下無線傳感器網(wǎng)絡(luò)和多媒體無線傳感器網(wǎng)絡(luò)的綜述性的報(bào)告。
2003年夏，隨著WSN技術(shù)的研究開始明朗化，我們開始第二輪撰寫WSN綜述性報(bào)告以研究最新的解決方案。大量的研究成果以及學(xué)術(shù)界和工業(yè)界的興趣激勵(lì)我們對WSN展開了進(jìn)一步的研究并且撰寫了本書。本書既可以作為研究生的教材以激發(fā)他們的創(chuàng)新思想，也可以為科研人員和工程師提供有關(guān)WSN技術(shù)的概況，并通過對WSN最新技術(shù)的深度剖析和對怎樣優(yōu)化現(xiàn)有技術(shù)繼而應(yīng)用到新興應(yīng)用和服務(wù)中的介紹引起讀者更有深度的思考。本書涵蓋了現(xiàn)有的WSN技術(shù)研究、應(yīng)用以及眾多應(yīng)用領(lǐng)域中對這些技術(shù)的改進(jìn)。本書凝聚了作者自己的研究成果以及由標(biāo)準(zhǔn)委員會做出的相關(guān)共識。由于近十年來對WSN的研究眾多，本書不可能涵蓋每一種解決方案，如有疏漏純屬無意。本書的內(nèi)容主要遵循TCP/IP協(xié)議棧的分層架構(gòu)，從物理層開始詳細(xì)介紹了每一層的技術(shù)，并且深入分析了諸如同步、定位和拓?fù)淇刂频目鐚咏鉀Q方案和服務(wù)策略以及WSN的其他特性。本書深入地闡釋了網(wǎng)絡(luò)架構(gòu)每一層的功能、協(xié)議和算法，旨在向讀者介紹現(xiàn)有技術(shù)并且在本書最后一章中指出了WSN所需面對的巨大的研究挑戰(zhàn)，以此來啟發(fā)讀者對現(xiàn)有方案進(jìn)行改進(jìn)和優(yōu)化。第1章是對WSN的概述，概要地介紹了傳感器平臺和網(wǎng)絡(luò)結(jié)構(gòu)。第2章對WSN現(xiàn)有的應(yīng)用進(jìn)行了總結(jié)，包括軍用和民用。第3章綜述了WSN的特性、關(guān)鍵設(shè)計(jì)因素和限制條件。第4章致力于WSN物理層的研究，包括物理層的技術(shù)、無線通信的特點(diǎn)和物理層的標(biāo)準(zhǔn)。
第5章主要介紹了WSN的MAC協(xié)議，重點(diǎn)介紹了應(yīng)用廣泛的最基礎(chǔ)的載波偵聽多點(diǎn)訪問/沖突避免（CSMA/CA）技術(shù)、由CSMA/CA改進(jìn)而來的截然不同的解決方案：基于時(shí)分多點(diǎn)接入（TDMA）的MAC以及二者的混合方案。第6章重點(diǎn)介紹了WSN中的差錯(cuò)控制技術(shù)并且分析了它們對高能效通信的影響。第5章和第6章介紹的都是數(shù)據(jù)鏈路層的技術(shù)。第7章致力于WSN的路由協(xié)議研究。將網(wǎng)絡(luò)層的路由協(xié)議分為四類：以數(shù)據(jù)為中心的路由協(xié)議、分層路由協(xié)議、地理路由協(xié)議和基于服務(wù)質(zhì)量（QoS）的路由協(xié)議。第8章首先指出了傳輸層解決方案的挑戰(zhàn)然后闡述了傳輸層的協(xié)議。第9章介紹了每層之間的跨層相互作用以及對通信表現(xiàn)的影響。此外，詳細(xì)闡述了跨層通信方法。第10章指出了時(shí)間同步的挑戰(zhàn)并且介紹了幾種針對這些挑戰(zhàn)的解決方法。第11章描述了定位技術(shù)的挑戰(zhàn)并將定位技術(shù)分為三類：測距技術(shù)、基于測距的定位協(xié)議和無需測距的定位協(xié)議。第12章介紹了WSN中的拓?fù)涔芾矸桨浮＞唧w而言，解釋了部署、能量控制、活動狀態(tài)、調(diào)度和分簇方法。第13章介紹了無線傳感器與執(zhí)行器網(wǎng)絡(luò)（WSAN）的概念和特點(diǎn)。特別強(qiáng)調(diào)了傳感器和執(zhí)行器之間以及不同執(zhí)行器之間協(xié)同問題的解決方案。此外，還討論了WSAN中的通信問題。第14章介紹了無線多媒體傳感網(wǎng)（WMSN）的挑戰(zhàn)和多種網(wǎng)絡(luò)拓?fù)洹＿�介紹了現(xiàn)有的多媒體傳感器平臺并遵循TCP/IP協(xié)議棧結(jié)構(gòu)描述了各層的協(xié)議。第15章致力于水下無線傳感網(wǎng)（UWSN），主要分析了水下環(huán)境對通信的影響。研究了水下聲波傳播的基礎(chǔ)，總結(jié)了協(xié)議棧各層的解決方案。第16章描述了無線地下傳感網(wǎng)（WUSN）的特點(diǎn)和應(yīng)用。特別地，詳細(xì)介紹了WUSN在土壤、礦井和隧道環(huán)境中的應(yīng)用及特點(diǎn)。同時(shí)研究了在上述情況下的信道特點(diǎn)，并指出了給通信帶來的挑戰(zhàn)。最后，第17章討論了WSN發(fā)展面臨的巨大挑戰(zhàn)。撰寫一本教科書肩負(fù)有很大的責(zé)任和挑戰(zhàn)。
第1章 設(shè)計(jì)驗(yàn)證的緣由
1.1 什么是設(shè)計(jì)驗(yàn)證
1.2 驗(yàn)證的基本原理
1.3 驗(yàn)證方法學(xué)
1.4 基于模擬的驗(yàn)證與形式驗(yàn)證的比較
1.5 形式驗(yàn)證的局限性
1.6 Verilog語言調(diào)度和執(zhí)行語義簡介
1.7 本章小結(jié)
第2章 編寫驗(yàn)證的代碼
2.1 功能正確性
2.2 時(shí)序正確性
2.3 模擬的性能
2.4 可移植性與可維護(hù)性
2.5 可綜合性、可調(diào)試性與通用工具兼容性
2.6 基于周期的模擬
2.7 硬件模擬／仿真
2.8 2狀態(tài)與4狀態(tài)模擬
2.9 linter程序的設(shè)計(jì)與使用
2.10 本章小結(jié)
2.11 習(xí)題
第3章 模擬器體系結(jié)構(gòu)與操作
3.1 編譯器
3.2 模擬器
3.3 模擬器的分類與比較
3.4 模擬器的操作與應(yīng)用
3.5 增量式編譯
3.6 模擬器控制臺
3.7 本章小結(jié)
3.8 習(xí)題
第4章 測試基準(zhǔn)組成與設(shè)計(jì)
4.1 測試基準(zhǔn)的分類與測試環(huán)境
4.2 初始化機(jī)制
4.3 時(shí)鐘生成與同步
4.4 激勵(lì)生成
4.5 響應(yīng)評估
4.6 驗(yàn)證實(shí)用程序
4.7 測試基準(zhǔn)至系統(tǒng)設(shè)計(jì)接口
4.8 常見的實(shí)際技術(shù)與方法
4.9 本章小結(jié)
4.10 習(xí)題
第5章 測試構(gòu)想、斷言與覆蓋
5.1 分層驗(yàn)證
5.2 測試規(guī)劃
5.3 偽隨機(jī)測試生成程序
5.4 斷言
5.5 SystemVerilog斷言
5.6 驗(yàn)證覆蓋
5.7 本章小結(jié)
5.8 習(xí)題
第6章 調(diào)試進(jìn)程與驗(yàn)證周期
6.1 故障捕獲、范圍壓縮與錯(cuò)誤跟蹤
6.2 模擬數(shù)據(jù)轉(zhuǎn)儲
6.3 潛在故障原因的隔離
6.4 系統(tǒng)設(shè)計(jì)更新與維護(hù)：修改控制
6.5 回歸、發(fā)布機(jī)制與流片標(biāo)準(zhǔn)
6.6 本章小結(jié)
6.7 習(xí)題
第7章 形式驗(yàn)證初步
7.1 集合與運(yùn)算
7.2 關(guān)系、劃分、偏序集與格
7.3 布爾函數(shù)與表示
7.4 布爾函數(shù)運(yùn)算符
7.5 有限狀態(tài)自動機(jī)與語言
7.6 本章小結(jié)
7.7 習(xí)題
第8章 判定圖、等價(jià)檢驗(yàn)與符號模擬
8.1 二叉判定圖
8.2 判定圖的變異
8.3 基于判定圖的等價(jià)檢驗(yàn)
8.4 布爾可滿足性
8.5 符號模擬
8.6 本章小結(jié)
8.7 習(xí)題
第9章 模型檢驗(yàn)與符號計(jì)算
9.1 性質(zhì)、規(guī)范與邏輯
9.2 性質(zhì)檢驗(yàn)
9.3 符號計(jì)算與模型檢驗(yàn)
9.4 符號CTL模型檢驗(yàn)
9.5 計(jì)算改進(jìn)
9.6 模型檢驗(yàn)工具的使用
9.7 本章小結(jié)
9.8 習(xí)題
參考文獻(xiàn)
縮寫詞匯表
新書資訊