相關主題
商品描述
本書聚焦RTL層面對ASIC和FPGA的建模與驗證，旨在通過系統化的理論講解、豐富的工程實例與工具驗證案例，幫助讀者掌握基於斷言的驗證方法，解決傳統驗證中需求模糊、設計意圖難監控、驗證完整性難衡量等核心痛點。
本書由SystemVerilog領域權威專家編寫，先通過大量示例展示基礎概念，然後專註於序列和屬性的細節，接著通過更多示例探討高級主題，隨後討論了在設計和驗證周期的各個階段（包括需求、設計和驗證階段）使用斷言的過程，通過兩個完整模型展示了形式化驗證的應用，最後增加了SVA方面的論文，同時回答了用戶在論壇中提出的問題。書中所呈現的編碼和使用指南源自作者多年的設計與驗證工作經驗，以及對硬件描述語言、斷言語言和框架庫的使用與教學經驗。
目錄大綱
第1章 驗證方法中的斷言 1
1.1 設計驗證方法學 2
1.2 項目使用哪種語言/方法？ 3
1.3 為什麼選擇SVA？ 8
1.4 屬性、斷言和嘗試的概述 12
1.5 基於斷言的驗證 21
第2章 理解序列 25
2.1 序列語法 26
2.2 序列操作符和內置函數 28
2.3 重覆操作符 31
2.4 序列組合操作符 45
2.5 序列支持的方法 55
2.6 序列和屬性中可用的形參類型 66
2.7 形參、序列和屬性聲明中的局部變量 76
第3章 理解屬性 99
3.1 斷言、屬性、術語與語法 100
3.2 屬性開頭聲明 105
3.3 屬性標識符 106
3.4 形參及其用法 106
3.5 屬性變量聲明 109
3.6 屬性語句的主體 109
3.7 時鐘事件 109
3.8 禁用條件 113
3.9 屬性表達式和操作符 118
3.10 應用場景 128
3.1 1 屬性中的局部變量 150
練習題（答案參見附錄A） 157
第4章 屬性和序列高級主題 161
4.1 斷言在SystemVerilog中的調度 162
4.2 基於斷言的系統函數 164
4.3 時鐘序列、屬性和多時鐘 186
4.4 接口中的屬性 198
4.5 斷言語句 199
4.6 立即斷言 213
4.7 斷言綁定至作用域或實例 219
4.8 靜態/自動變量和斷言 223
第5章 檢查器 231
5.1 checker的優勢 232
5.2 checker結構的語法 234
5.3 checker內容 235
5.4 檢查器使用的模型 238
5.5 上下文推斷 249
5.6 檢查器變量 250
第6章 設計流程中的SVA 257
6.1 傳統設計流程 258
6.2 采用SVA的設計流程 258
6.3 需求 260
6.4 架構規劃 263
6.5 驗證和測試計劃 263
6.6 RTL設計 264
6.7 測試平臺設計 264
6.8 功能覆蓋率在驗證中的重要性 265
6.9 案例研究——同步FIFO 269
6.10 仿真 285
第7章 基於斷言的形式化驗證 287
7.1 形式化屬性驗證 288
7.2 全局時鐘塊以及過去和將來采樣值函數 290
7.3 案例研究——信號燈控制器的FV 299
第8章 SVA規範指南 309
8.1 命名規範指南 310
8.2 風格 314
8.3 模型使用指南 324
8.4 方法學指南 334
8.5 SVA與UVM的結合 341
第9章 斷言驗證 343
9.1 驅動端口 346
9.2 激勵向量 351
9.3 測試平臺構建方法 360
9.4 測試模塊中簡單的不受約束的隨機測試向量 362
第10章 斷言字典 373
10.1 在en信號上升跳變時總線遞增 374
10.2 若COND1成立，則必須滿足COND2 376
10.3 若COND1成立，則當下次COND2發生時必須滿足COND3 376
10.4 若COND1成立，則在第N次COND2後必須滿足COND3 377
10.5 若滿足COND1且首次滿足COND2，則保持COND3直至出現COND4為止 378
10.6 若滿足COND1且首次滿足COND2，則觸發序列 379
10.7 在COND1和COND2之間，信號1必須保持有效 380
10.8 若COND1成立後出現1次COND2，則觸發序列 381
10.9 若COND1成立，則在COND3成立前出現N次COND2（N為變量值） 382
10.10 若COND1成立，且在N個周期內出現y次COND2，則觸發COND3 383
10.11 若COND1成立，則COND2必須保持直到COND3成立 384
10.12 若COND1成立，則COND2必須在COND3之前發生 385
10.13 若COND1後跟隨COND2，且在COND2持續期間64個周期內未收到COND3，則觸發錯誤（COND5）；如果64個周期內收到COND3，則觸發COND4 386
10.14 若COND1發生，則COND2應在N個周期內完成，除非COND3 發生 387
10.15 內存數據完整性：從內存讀取的數據應與最後一次寫入的數據相同 389
10.16 隊列的數據完整性：接口寫入的數據必須正確傳輸至接收硬件 391
10.17 禁止對同一地址連續寫入兩次 393
10.18 連續兩次寫入地址0後，下一周期ready必須為1 394
10.19 假設覆位信號在初始N個周期內保持低電平 395
10.20 若序列啟動但未完成，則狀態寄存器必須報錯 396
10.21 PROPERTY1與PROPERTY2互斥性驗證 397
10.22 禁止未讀前重覆寫入同一地址 400
10.23 SignalA[odd_bits] |=> SignalB[odd_bits]，SignalA[even_bits] |=> SignalB[even_bits] 400
10.24 在斷言中使用類變量 401
10.25 如何覆蓋四值變量（0,1,X,Z） 401
10.26 線程唯一性問題——FIFO 案例 402
10.27 先行算子為真時排他性後續算子檢查 405
10.28 建立時間和保持時間檢查 406
10.29 時間檢查 407
10.30 在兩個脈沖之間，信號a必須為真（無固定時鐘） 408
10.31 信號a在信號b出現10個高電平周期期間保持高電平 408
10.32 並行轉串行 408
10.33 一個信號在另一個信號的兩個非連續下降沿之後保持穩定 409
10.34 測量時鐘周期 410
10.35 斷言的順序觸發 411
10.36 用於跨時鐘域數據路徑的斷言 412
10.37 總線序列 412
10.38 在時鐘邊沿（上升沿或下降沿）發生前禁用斷言 413
10.39 這個屬性有什麼問題？ 413
10.40 信號在兩個事件之間持續保持高電平至少N 個周期 414
附錄 417
附錄A 第3章練習題答案 418
附錄B 專業術語 424
附錄C 系統任務和系統函數（IEEE 2012第20章） 435
補充內容 439
補充內容1：使用Fork-join 模型理解SVA引擎 440
補充內容2：用戶使用SVA的經驗反思（第1部分） 454
補充內容3：用戶使用SVA的經驗反思（第2部分） 459
補充內容4：理解時間步內的斷言處理 464
補充內容5：理解和使用立即斷言 470
補充內容6：SVA包——動態的範圍延遲和重覆 474
補充內容7：輔助邏輯與always屬性 480
補充內容8：基於UVM類環境的SVA 485
補充內容9： 使用斷言代替FSM/邏輯實現記分板並進行驗證 492
補充內容10：理解多時鐘、triggered和matched 499
補充內容11：用戶問答 510
補充內容12：SVA退化現象 528
補充內容13：intersect與throughout、until、until_with、within的區別與聯系536
