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

dc.contributor.authorRoy, Tonmoyen
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberWang, Chaoen
dc.contributor.committeememberZeng, Haiboen
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2017-09-06T08:00:24Zen
dc.date.available2017-09-06T08:00:24Zen
dc.date.issued2017-09-05en
dc.description.abstractIn 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 the property under test to generate small-sized SMT formulas that describe the change of variable values between consecutive cycles. Variable substitution is then used on these variables to generate the formula for the subsequent cycles without traversing the abstract syntax tree of the entire design. To reduce the approximation on the induction step, an addition of signal domain constraints is proposed. Moreover, we present the technique for splitting up the property in question to get a better model of the system. The later half of the thesis is concerned with presenting a technique for doing sequential vector compaction on test set generated during simulation based ATPG. Starting with a compaction framework for storing metadata and about the test vectors during generation, this work presented to methods for findind the solution of this compaction problem. The first of these two methods generate the optimum solution by converting the problem appropriate for an optimization solver. The latter method utilizes a heuristics based approach for solving the same problem which generates a comparable but sub-optimal solution while having magnitudes better time and computational efficiency.en
dc.description.abstractgeneralElectronic circuits can be described with languages known a hardware description languages like Verilog. The first part of this thesis is concerned about automatically proving if parts of this code is actually useful or reachable when implemented on and actual circuit. The thesis builds up on a method known as bounded model checking which can automatically prove if a property holds or not for a given system. The key insight is obtained from the fact that various memory elements in a circuit is allowed to be only in a certain range of values during the design process. The later half of this thesis is gear towards generating minimum sized inputs values to a circuit required for testing it. This work uses large sized input values to circuits generated by a previously published tool and proposes a way to make them smaller. This can reduce cost immensely for testing circuits in the industry where even the smallest increase in testing time increases cost of development immensely. There are two such approaches presented, one of which gives the optimum result but takes a long time to run for larger circuits, while the other gives comparable but sub-optimal result in a much more time efficient manner.en
dc.description.degreeMaster of Scienceen
dc.format.mediumETDen
dc.identifier.othervt_gsexam:12695en
dc.identifier.urihttp://hdl.handle.net/10919/78801en
dc.publisherVirginia Techen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectRTL Verificationen
dc.subjectReachabilityen
dc.subjectk-Inductionen
dc.subjectBounded Model Checkingen
dc.subjectTest Vector Compactionen
dc.titleReachability Analysis of RTL Circuits Using k-Induction Bounded Model Checking and Test Vector Compactionen
dc.typeThesisen
thesis.degree.disciplineComputer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.levelmastersen
thesis.degree.nameMaster of Scienceen

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Roy_T_T_2017.pdf
Size:
609.18 KB
Format:
Adobe Portable Document Format

Collections