{"id":{"repo_id":"vt","oai_identifier":"oai:vtechworks.lib.vt.edu:10919/32461"},"canonical_url":"https://search.dev.ndltd.org/etd/vt/oai:vtechworks.lib.vt.edu:10919/32461","repository":{"repo_id":"vt","name":"Virginia Tech","base_url":"https://vtechworks.lib.vt.edu/oai/request"},"display":{"title":"Fast Discovery of Illegal State Cubes for Sequential Equivalence Checking","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Hanle, Donald"],"institution":"Virginia Tech","degree_name":"Master of Science","degree_level":"masters","degree_discipline":"Electrical and Computer Engineering","degree_department":"Electrical and Computer Engineering","school":null,"contributors":[],"advisors":[],"committee_chairs":["Hsiao, Michael S."],"committee_members":["Martin, Thomas L.","Schaumont, Patrick R."],"year":2011,"date_issued":"2011-05-06","date_published":"2011-05-06","updated_at":"2026-07-22T22:19:47Z","subjects":["BDD","Illegal States","SEC"],"languages":[],"rights":["In Copyright"],"rights_urls":["http://rightsstatements.org/vocab/InC/1.0/"],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["etd-05092011-150110"],"render_values":[{"text":"etd-05092011-150110","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/10919/32461","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeechair","label":"Committee Chair","values":["Hsiao, Michael S."]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Martin, Thomas L.","Schaumont, Patrick R."]},{"key":"dc:contributor.department","label":"Department","values":["Electrical and Computer Engineering"]},{"key":"dc:creator","label":"Author","values":["Hanle, Donald"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2014-03-14T20:35:55Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2014-03-14T20:35:55Z","2011-05-12"]},{"key":"dc:date.issued","label":"Date","values":["2011-05-06"]},{"key":"dc:publisher","label":"Institution","values":["Virginia Tech"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical and Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Virginia Polytechnic Institute and State University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["BDD","Illegal States","SEC"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/vocab/InC/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["etd-05092011-150110"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10919/32461"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Master of Science"]},{"key":"dc:title","label":"Title","values":["Fast Discovery of Illegal State Cubes for Sequential Equivalence Checking"]}]}],"canonical_facts":{"dc:contributor.committeechair":["Hsiao, Michael S."],"dc:contributor.committeemember":["Martin, Thomas L.","Schaumont, Patrick R."],"dc:contributor.department":["Electrical and Computer Engineering"],"dc:creator":["Hanle, Donald"],"dc:date.accessioned":["2014-03-14T20:35:55Z"],"dc:date.available":["2014-03-14T20:35:55Z","2011-05-12"],"dc:date.issued":["2011-05-06"],"dc:description.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."],"dc:description.degree":["Master of Science"],"dc:identifier.other":["etd-05092011-150110"],"dc:identifier.uri":["http://hdl.handle.net/10919/32461"],"dc:publisher":["Virginia Tech"],"dc:rights":["In Copyright"],"dc:rights.uri":["http://rightsstatements.org/vocab/InC/1.0/"],"dc:subject":["BDD","Illegal States","SEC"],"dc:title":["Fast Discovery of Illegal State Cubes for Sequential Equivalence Checking"],"dc:type":["Thesis"],"thesis:degree_discipline":["Electrical and Computer Engineering"],"thesis:degree_level":["masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Virginia Polytechnic Institute and State University"]},"updated_at":"2026-07-22T22:19:47Z"}