Title page for ETD etd-05092011-150110


Type of Document Master's Thesis
Author Hanle, Donald
Author's Email Address dhanle@vt.edu
URN etd-05092011-150110
Title Fast Discovery of Illegal State Cubes for Sequential Equivalence Checking
Degree Master of Science
Department Electrical and Computer Engineering
Advisory Committee
Advisor Name Title
Hsiao, Michael S. Committee Chair
Martin, Thomas L. Committee Member
Schaumont, Patrick Robert Committee Member
Keywords
  • BDD
  • Illegal States
  • SEC
Date of Defense 2011-05-06
Availability unrestricted
Abstract
Sequential Equivalence checking has been and still is a challenging problem. Verifying two circuits that are structurally different but logically the same is very important and has many applications. Critical to the success of sequential equivalence checking is the determination of a sufficient portion of illegal states such that the two designs are equivalent outside of the illegal states. This work proposes a low-cost method to discover a subset of the illegal state space of a circuit by simulating and grouping some state variables to determine if any missing patterns are present. This thesis discusses the selection of simulated inputs, the grouping of flip-flops and what the missing patterns represent. Then all missing patterns are considered which are illegal state cubes and represent and compact them using BDDs. A BDD implementation was created to compact these illegal states more efficiently. Discussion is then done on the parameters of the BDD implementation design which can be used more efficiently given the situation. These illegal state cubes are considered to be implications which can be used to constrain a SAT solver. Results are then presented which show how effective these constraints are to proving equivalency using the SAT solver. Finally, the future work is discussed of discovering the illegal state space either faster or more completely.
Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  Hanle_DG_T_2011.pdf 841.24 Kb 00:03:53 00:02:00 00:01:45 00:00:52 00:00:04

Browse All Available ETDs by ( Author | Department )

dla home
etds imagebase journals news ereserve special collections
virgnia tech home contact dla university libraries

If you have questions or technical problems, please Contact DLA.