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...
Main Author: | |
---|---|
Other Authors: | |
Format: | Others |
Published: |
Virginia Tech
2017
|
Subjects: | |
Online Access: | http://hdl.handle.net/10919/78801 |