|
|
|
马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。
您需要 登录 才可以下载或查看,没有账号?注册
×
本帖最后由 courageheart 于 2021-4-29 11:41 编辑
Enhanced Virtual Prototyping Featuring RISC-V Case Studies by Vladimir Herdt, Da.pdf
(4.83 MB , 下载次数:
274 )
开源资料的地址:agra-uni-bremen/riscv-vp: RISC-V Virtual Prototype (github.com)
1 Introduction .................................................................. 1
1.1 Virtual Prototype-Based Design Flow ................................. 3
1.2 Book Contribution ...................................................... 5
1.3 Book Organization ...................................................... 8
2 Preliminaries ................................................................. 11
2.1 SystemC TLM........................................................... 11
2.1.1 TLM-Based Communication ................................... 12
2.1.2 Simulation Semantics........................................... 13
2.2 RISC-V .................................................................. 14
2.2.1 ISA Overview ................................................... 15
2.2.2 Atomic Instruction Set Extension .............................. 15
2.3 Coverage-Guided Fuzzing .............................................. 16
2.3.1 LibFuzzer Core ................................................. 16
2.3.2 LibFuzzer Extensions........................................... 17
2.4 Symbolic Execution..................................................... 18
2.4.1 Overview ........................................................ 18
2.4.2 Example ......................................................... 19
3 An Open-Source RISC-V Evaluation Platform........................... 21
3.1 RISC-V-Based Virtual Prototype ....................................... 23
3.1.1 RISC-V-Based VP Architecture................................ 23
3.1.2 VP Interaction with SW and Environment .................... 26
3.1.3 VP Performance Optimizations ................................ 32
3.1.4 Simulation of Multi-Core Platforms ........................... 33
3.1.5 VP Extension and Configuration ............................... 35
3.1.6 VP Evaluation................................................... 41
3.1.7 Discussion and Future Work ................................... 45
3.2 Fast and Accurate Performance Evaluation for RISC-V .............. 46
3.2.1 Background: HiFive1 Board ................................... 47
3.2.2 Core Timing Model ............................................. 48
3.2.3 Experiments..................................................... 54
3.2.4 Discussion and Future Work ................................... 57
3.3 Summary ................................................................ 58
4 Formal Verification of SystemC-Based Designs using Symbolic
Simulation .................................................................... 59
4.1 Stateful Symbolic Simulation .......................................... 60
4.1.1 SystemC Intermediate Verification Language ................. 64
4.1.2 Overview Symbolic Simulation ................................ 66
4.1.3 State Subsumption Reduction .................................. 72
4.1.4 Symbolic Subsumption Checking.............................. 80
4.1.5 Experiments..................................................... 83
4.1.6 Discussion and Future Work ................................... 88
4.2 Formal Verification of an Interrupt Controller......................... 90
4.2.1 TLM Peripheral Modeling in SystemC ........................ 91
4.2.2 Bridging the Modeling Gap .................................... 92
4.2.3 Case Study ...................................................... 94
4.3 Compiled Symbolic Simulation ........................................ 98
4.3.1 Overview ........................................................ 99
4.3.2 Optimizations ................................................... 105
4.3.3 Experiments..................................................... 108
4.3.4 Discussion and Future Work ................................... 112
4.4 Parallelized Compiled Symbolic Simulation .......................... 112
4.4.1 Implementation Details......................................... 113
4.4.2 Evaluation and Conclusion ..................................... 116
4.5 Summary ................................................................ 117
5 Coverage-Guided Testing for Scalable Virtual
Prototype Verification ....................................................... 119
5.1 Data Flow Testing for Virtual Prototypes .............................. 120
5.1.1 SystemC Running Example .................................... 121
5.1.2 Def-Use Association and Data Flow Testing .................. 121
5.1.3 Data Flow Testing for SystemC ................................ 124
5.1.4 Implementation Details......................................... 129
5.1.5 Experimental Results ........................................... 131
5.2 Verifying Instruction Set Simulators using Coverage-Guided
Fuzzing .................................................................. 132
5.2.1 Coverage-Guided Fuzzing for ISS Verification ............... 133
5.2.2 Case Study: RISC-V ISS Verification ......................... 137
5.2.3 Discussion and Future Work ................................... 140
5.3 Summary ................................................................ 142
6 Verification of Embedded Software Binaries using Virtual
Prototypes..................................................................... 143
6.1 Concolic Testing of Embedded Binaries............................... 144
6.1.1 Background on Concolic Testing of SW ...................... 146
6.1.2 Concolic Testing Engine for RISC-V Embedded Binaries ... 146
6.1.3 Experiments..................................................... 152
6.1.4 Discussion and Future Work ................................... 157
6.2 Verification of Embedded Binaries using Coverage-guided
Fuzzing .................................................................. 158
6.2.1 VP-based Coverage-Guided Fuzzing .......................... 159
6.2.2 Experiment 1: Testing Embedded Applications............... 166
6.2.3 Experiment 2: Testing the Zephyr IP Stack ................... 170
6.2.4 Discussion and Future Work ................................... 173
6.3 Summary ................................................................ 173
7 Validation of Firmware-Based Power Management using
Virtual Prototypes ........................................................... 175
7.1 A Constrained Random Approach for Workload Generation ......... 177
7.1.1 Early Validation of FW-based Power Management
Strategies ........................................................ 178
7.1.2 SoCRocket Case Study ......................................... 183
7.1.3 Results........................................................... 188
7.1.4 Discussion and Future Work ................................... 189
7.2 Maximizing Power State Cross Coverage ............................. 190
7.2.1 Maximizing Power State Cross Coverage ..................... 191
7.2.2 Case Study ...................................................... 196
7.2.3 Discussion and Future Work ................................... 202
7.3 Summary ................................................................ 202
8 Register-Transfer Level Correspondence Analysis....................... 205
8.1 Towards Fully Automated TLM-to-RTL Property Refinement ....... 206
8.1.1 UTOPIA Case Study ........................................... 208
8.1.2 Static Analysis of Transactors.................................. 210
8.1.3 Property Refinement ............................................ 212
8.1.4 Discussion and Future Work ................................... 214
8.2 Automated RTL-to-TLM Fault Correspondence Analysis............ 215
8.2.1 RTL-to-TLM Fault Correspondence Analysis ................ 217
8.2.2 Formal Fault Localization Analysis............................ 222
8.2.3 Case Study ...................................................... 227
8.3 Summary ................................................................ 229
9 Conclusion .................................................................... 231
References......................................................................... 235
Index ............................................................................... 245
|
|