Fast Discovery of Illegal State Cubes for Sequential Equivalence Checking

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.

Name thesis:degree_name

Master of Science

Level thesis:degree_level

masters

Discipline thesis:degree_discipline

Electrical and Computer Engineering

Department dc:contributor.department

Electrical and Computer Engineering

Grantor dc:publisher

Virginia Tech

Year dc:date.issued

2011

Author dc:creator

• Hanle, Donald

Chair dc:contributor.committeechair

• Hsiao, Michael S.

Committee members dc:contributor.committeemember

• Martin, Thomas L.
• Schaumont, Patrick R.

• BDD
• Illegal States
• SEC

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Dc Identifier Other

etd-05092011-150110

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/32461