Thesis
Precise abstract interpretation of hardware designs
- Abstract:
-
This dissertation shows that the bounded property verification of hardware Register Transfer Level (RTL) designs can be efficiently performed by precise abstract interpretation of a software representation of the RTL.
The first part of this dissertation presents a novel framework for RTL verification using native software analyzers. To this end, we first present a translation of the hardware circuit expressed in Verilog RTL into the software in C called the software netlist
Expand abstract
Actions
Authors
Contributors
+ Kroening, D
Department:
University of Oxford
Role:
Supervisor
+ Melham, T
Department:
University of Oxford
Role:
Supervisor
Funding
Bibliographic Details
- Type of award:
- DPhil
- Level of award:
- Doctoral
- Awarding institution:
- University of Oxford
Item Description
- Keywords:
- Subjects:
- UUID:
-
uuid:680f0093-0405-4a0b-88dc-c4d7177d840f
- Deposit date:
-
2018-06-18
Related Items
Terms of use
- Copyright holder:
- Mukherjee, R
- Copyright date:
- 2018
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record