Reachability Analysis of RTL Circuits Using k-Induction Bounded Model Checking and Test Vector Compaction

Reachability Analysis of RTL Circuits Using k-Induction Bounded Model Checking and Test Vector Compaction

In the first half of this thesis, a novel approach for k-induction bounded model checking using signal domain constraints and property partitioning for proving unreachability of branches in Verilog RTL code is presented. To do this, it approach uses program slicing with respect to the variables of...

Full description

Bibliographic Details
Main Author: Roy, Tonmoy
Other Authors: Electrical and Computer Engineering
Format: Others
Published: Virginia Tech 2017
Subjects:
RTL Verification
Reachability
k-Induction
Bounded Model Checking
Test Vector Compaction
Online Access:http://hdl.handle.net/10919/78801

Internet

http://hdl.handle.net/10919/78801

Similar Items